rify 0.5.0

RDF reasoner that operates on RIF-like conjunctive rules. Outputs a machine readable proof of some claim which can be cheaply verified.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

# rify

[![Crates.io](https://img.shields.io/crates/v/rify)](https://crates.io/crates/rify)
[![Docs](https://docs.rs/rify/badge.svg)](https://docs.rs/rify)
[![npm](https://img.shields.io/npm/v/rify)](https://www.npmjs.com/package/rify)

Rify is a [forward chaining](https://en.wikipedia.org/wiki/Forward_chaining) [inference engine](https://en.wikipedia.org/wiki/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 graph.

Reasoning generates a proof which can be used to quickly verify the result pragmatically.

Logical rules are defined as if-then clauses. Something like this:

```rust
struct Rule {
    if_all: Vec<[Entity; 3]>,
    then: Vec<[Entity; 3]>,
}

enum Entity {
    /// A a named variable with an unknown value.
    Unbound(String),
    /// A literal RDF node.
    Bound(RdfNode),
}

// actual definitions of these types are templated but this is the gist
```

# Use

Two functions are central to this library: `prove` and `validate`.

```rust
// Example use of `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![
        [Unbound("a"), Bound("is"), Bound("awesome")], // if someone is awesome
        [Unbound("a"), Bound("score"), Unbound("s")],    // and they have some score
    ],
    vec![[Unbound("a"), Bound("score"), Bound("awesome")]], // then they must have an awesome score
)?;

assert_eq!(
    prove::<&str, &str>(
        &[["you", "score", "unspecified"], ["you", "is", "awesome"]],
        &[["you", "score", "awesome"]],
        &[awesome_score_axiom]
    )?,
    &[
        // (you is awesome) ∧ (you score unspecified) -> (you score awesome)
        RuleApplication {
            rule_index: 0,
            instantiations: vec!["you", "unspecified"]
        }
    ]
);
```

```rust
// Example use of `validate`

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

// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome)
let awesome_score_axiom = ...;

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,
).map_err(|e| format!("{:?}", e))?;

// Now we know that under the given rules, if all RDF triples in `assumed` are true, then all
// RDF triples in `implied` are also true.
```

# recipies

In addition to normal cargo commands like `cargo test` and `cargo check` the `./justfile`
defines some scripts which can be useful during develompent. 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.