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.
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.
Given the rules which were passed, if all the claims in
Make all possible inferences.
Locate a proof of some composite claims given the provided premises and rules.
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.