给定前提和目标陈述，rify 可以生成一个证明，该证明可以用于程序化快速验证结果。

逻辑规则定义为 if-then 子句。例如：

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 不关心其输入和输出是否为有效的 RDF。例如，它会欣然接受谓词为字面量的四元组。 https://www.w3.org/TR/rdf11-concepts/#section-triples

使用

该库中有三个核心功能：prove、validate 和 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"],
    ],
);

食谱

除了正常的 cargo 命令（如 cargo test 和 cargo check）外，./justfile 定义了一些在开发期间可能有用的脚本。例如，just js-test 将测试该库的 JavaScript 绑定。更多信息请参见 ./justfile。

许可协议

该项目可根据您的选择在 Apache 许可协议版本 2.0 或 MIT 许可协议下获得许可。