LP, the Larch Prover -- Forward inference

LP provides mechanisms for proving theorems using both forward and backward inference. Forward inferences produce consequences from LP's logical system. Backward inferences produce subgoals whose proof will suffice to establish a conjecture. LP provides four methods of forward inference, each of which derives consequences from the axioms in LP's logical system.

Normalization

Whenever a new rewrite rule is added to its logical system, LP automatically renormalizes all formulas, rewrite rules, and deduction rules. It discards any formula or rewrite rule that normalizes to true. If all hypotheses of a deduction rule normalize to true, LP replaces the deduction rule by the formulas in its conclusions. If all conclusions of a deduction rule normalize to true, LP discards the deduction rule.

Users can make formulas, rewrite rules, and deduction rules immune or ancestor-immune to protect them from automatic normalization, both to enhance the performance of LP and to preserve particular forms for use in a proof. Users can also deactivate rewrite rules to prevent them from being applied automatically. The normalize and rewrite commands explicitly apply rewrite rules (whether or not active) to facts (whether or not immune).

Deduction

Whenever a new deduction rule is added to its logical system, LP automatically applies that deduction rule to all formulas and rewrite rules. Likewise, whenever a formula or rewrite rule is normalized, LP automatically applies all deduction rules to the new normal form.

Inactive deduction rules are not used for automatic deduction, and immune formulas and rewrite rules are not subject to automatic deduction. Users can also apply deduction rules explicitly, for example, to immune formulas.

Critical pairs

The computation of critical-pairs and the Knuth-Bendix completion procedure produce consequences from incomplete rewriting systems. It is generally impossible or overly costly to complete a rewriting system. However, the completion procedure can be used to look for inconsistencies in a system, or to perform the final steps in some proofs.

Quantifier elimination

The instantiate command enables users to eliminate universal quantifiers, or to replace free variables by terms, in formulas, rewrite rules, and deduction rules. The fix command enables users to eliminate existential quantifiers in formulas and rewrite rulest to produce a conservative extension of LP's logical system.