Skip to content

RDF fact prover and proof validator operating on simple conjunctive rules.

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT
Notifications You must be signed in to change notification settings

docknetwork/rify

Repository files navigation

rify

Crates.io Docs npm

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:

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<String>,
    },
    DefaultGraph,
}

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

Use

Three functions are central to this library: prove, validate, and infer.

prove

use rify::{
    prove,
    Entity::{Unbound, Bound},
    Rule, RuleApplication,
};

// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
let awesome_score_axiom = Rule::create(
    vec![
        // if someone is awesome
        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
        // and they have some score
        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
    ],
    vec![
        // then they must have an awesome score
        [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")]
    ],
).expect("invalid rule");

assert_eq!(
    prove::<&str, &str>(
        // list of already known facts (premises)
        &[
            ["you", "score", "unspecified", "default_graph"],
            ["you", "is", "awesome", "default_graph"]
        ],
        // the thing we want to prove
        &[["you", "score", "awesome", "default_graph"]],
        // ordered list of logical rules
        &[awesome_score_axiom]
    ),
    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"]
        }
    ])
);

validate

use rify::{
    prove, validate, Valid,
    Rule, RuleApplication,
    Entity::{Bound, Unbound}
};

// same as above
let awesome_score_axiom = Rule::create(
    vec![
        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
    ],
    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>(
    &[awesome_score_axiom],
    &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.

infer

use rify::{infer, Entity::{Unbound, Bound}, Rule};

// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
let awesome_score_axiom = Rule::create(
    vec![
        // if someone is awesome
        [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")],
        // and they have some score
        [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")],
    ],
    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", "default_graph"],
    ["you", "is", "awesome", "default_graph"]
];

let new_facts = infer::<&str, &str>(&facts, &[awesome_score_axiom]);
facts.extend(new_facts);

assert_eq!(
    &facts,
    &[
        ["you", "score", "unspecified", "default_graph"],
        ["you", "is", "awesome", "default_graph"],
        ["you", "score", "awesome", "default_graph"],
    ],
);

Recipes

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.

License

This project is licensed under either of Apache License, Version 2.0 or MIT license, at your option.

About

RDF fact prover and proof validator operating on simple conjunctive rules.

Resources

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Stars

Watchers

Forks

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •