Crate rify[][src]

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.