Crate rify

Source

Structs§

Rule
A human friendly-ish logical rule representation. Each rule represents an if-then statement (implication relationship). Statements in the rule may contain constants and/or variables. Constants are represented as Entity::Bound. Variables are represented as Entity::Unbound.
RuleApplication
An element of a deductive proof. Proofs can be transmitted and later validatated as long as the validator assumes the same rule list as the prover.
Valid
Given the rules which were passed, if all the claims in assumed are true then all the claims in implied are true.

Enums§

CantProve
Entity
Invalid
InvalidRule

Functions§

infer
Make all possible inferences.
prove
Locate a proof of some composite claims given the provided premises and rules.
validate
Check is a proof is well-formed according to a ruleset. Returns the set of assumptions used by the proof and the set of statements those assumptions imply. If all the assumptions are true, and then all the implied claims are true under the provided ruleset.