Rify is a forward chaining inference engine designed specifically for use on in-memory RDF graphs.
It accepts conjunctive rules with limited expressiveness so reasoning is bounded by O(n^k) in both memory and in computation where n is the number of nodes in the input RDF dataset.
Given premises and target statement[s], rify can generate a proof which can be used to quickly verify the result programatically.
Logical rules are defined as if-then clauses. Something like this:
```rust struct Rule { if_all: Vec<[Entity; 4]>, then: Vec<[Entity; 4]>, }
// Notice it's [Entity; 4], not [Entity; 3]. This reasoner operates on Rdf Quads, not triples.
// You can still reason over triples by binding a unique resource e.g. RdfTerm::DefaultGraph
// as the graph in all rules and all quads.
enum Entity { /// A a named variable with an unknown value. Unbound(String), /// A literal with a constant value. Bound(RdfTerm), }
// actual definitions of these types are templated but this is the gist
// You get to define this type! Here is an example definition.
enum RdfTerm {
Blank(usize),
Iri(String),
Literal {
datatype: String,
value: String,
lang_tag: Option
Rify doesn't care whether its input and output is valid rdf. For example, it will happily accept a quad whose predicate is a literal. https://www.w3.org/TR/rdf11-concepts/#section-triples
Three functions are central to this library: prove, validate, and infer.
```rust use rify::{ prove, Entity::{Unbound, Bound}, Rule, RuleApplication, };
// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome) let awesomescoreaxiom = Rule::create( vec![ // if someone is awesome [Unbound("a"), Bound("is"), Bound("awesome"), Bound("defaultgraph")], // and they have some score [Unbound("a"), Bound("score"), Unbound("s"), Bound("defaultgraph")], ], vec![ // then they must have an awesome score [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")] ], ).expect("invalid rule");
asserteq!(
prove::<&str, &str>(
// list of already known facts (premises)
&[
["you", "score", "unspecified", "defaultgraph"],
["you", "is", "awesome", "defaultgraph"]
],
// the thing we want to prove
&[["you", "score", "awesome", "defaultgraph"]],
// ordered list of logical rules
&[awesomescoreaxiom]
),
Ok(vec![
// the desired statement is proven by instantiating the awesome_score_axiom
// (you is awesome) ∧ (you score unspecified) -> (you score awesome)
RuleApplication {
rule_index: 0,
instantiations: vec!["you", "unspecified"]
}
])
);
```
```rust use rify::{ prove, validate, Valid, Rule, RuleApplication, Entity::{Bound, Unbound} };
// same as above let awesomescoreaxiom = Rule::create( vec![ [Unbound("a"), Bound("is"), Bound("awesome"), Bound("defaultgraph")], [Unbound("a"), Bound("score"), Unbound("s"), Bound("defaultgraph")], ], vec![[Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]], ).expect("invalid rule");
let proof = vec![ // (you is awesome) ∧ (you score unspecified) -> (you score awesome) RuleApplication { rule_index: 0, instantiations: vec!["you", "unspecified"] } ];
let Valid { assumed, implied } = validate::<&str, &str>( &[awesomescoreaxiom], &proof, ).expect("invalid proof");
// Now we know that under the given rules, if all quads in assumed are true, then all
// quads in implied are also true.
```
```rust use rify::{infer, Entity::{Unbound, Bound}, Rule};
// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome) let awesomescoreaxiom = Rule::create( vec![ // if someone is awesome [Unbound("a"), Bound("is"), Bound("awesome"), Bound("defaultgraph")], // and they have some score [Unbound("a"), Bound("score"), Unbound("s"), Bound("defaultgraph")], ], vec![ // then they must have an awesome score [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")] ], ).expect("invalid rule");
let mut facts = vec![ ["you", "score", "unspecified", "defaultgraph"], ["you", "is", "awesome", "defaultgraph"] ];
let newfacts = infer::<&str, &str>(&facts, &[awesomescoreaxiom]); facts.extend(newfacts);
asserteq!( &facts, &[ ["you", "score", "unspecified", "defaultgraph"], ["you", "is", "awesome", "defaultgraph"], ["you", "score", "awesome", "defaultgraph"], ], ); ```
In addition to normal cargo commands like cargo test and cargo check the ./justfile
defines some scripts which can be useful during development. For example, just js-test will
test the javascript bindings to this library. See ./justfile for more.
This project is licensed under either of Apache License, Version 2.0 or MIT license, at your option.