### 8 unstable releases (3 breaking)

0.7.1 | Apr 23, 2021 |
---|---|

0.7.0 | Apr 12, 2021 |

0.7.0-rc.1 | Mar 30, 2021 |

0.6.0 | Mar 9, 2021 |

0.1.0 | Sep 15, 2020 |

#**284** in Database implementations

**25** downloads per month

**MIT/Apache**

105KB

2K
SLoC

# rify

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

in both memory and in computation where n is the number of nodes in the input RDF dataset.`O (n^k)`

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`

, and `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`"``]``,`
`]``,`
`)``;`

# Recipes

In addition to normal cargo commands like

and `cargo`` test`

the `cargo`` check`

defines some scripts which can be useful during development. For example, `./justfile`

will
test the javascript bindings to this library. See `just js -test`

`./justfile`

for more.# License

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

#### Dependencies

~170KB