LP, the Larch Prover -- Backward inference


The prove command causes LP to initiate a proof of a conjecture by backward inference. LP provides nine methods of backward inference for proving formulas; in addition, it provides automatic methods of backward inference for proving deduction rules, induction rules, and operator theories. In each method, LP generates a set of subgoals, that is, lemmas to be proved that together are sufficient to imply the conjecture. For some methods, it also generates additional hypotheses that may be used to prove particular subgoals.

Proof by normalization
Normalization rewrites conjectures. If a conjecture normalizes to true, it is a theorem. Otherwise the normalized conjecture becomes the subgoal to be proved.

Proof by cases
A proof by cases divides a proof into specified cases, enabling the conjecture to be rewritten further using the case hypotheses.

Proof by contradiction
Proofs by contradiction provide an indirect method of proof. If LP detects an inconsistency after adding the negation of the conjecture to its logical system, then it concludes that the conjecture is a theorem.

Proof by induction
Proofs by induction are based on the induction rules associated with assertions that some sort is generated by a set of operators or that some binary relation is well founded.

Proof of conditionals
Proofs of conditionals are simplified proofs by cases applicable to conjectures of the form (if t1 then t2 else t3) = t4, where t4 does not begin with if.

Proof of conjunctions
Proofs of conjunctions provide a way to reduce the expense of equational term rewriting when proving conjectures of the form t1 /\ ... /\ tn.

Proof of implications
Proofs of implications are simplified proofs by cases applicable to conjectures of the form t1 => t2.

Proof of logical equivalence
Proofs of logical equivalence are simplified proofs by cases applicable to conjectures of the form t1 <=> t2.

Proof by generalization
Proofs by generalization provide a means of establishing a conjecture that contains a universal quantifier by proving an instance of the conjecture with the quantified variable replaced by an appropriate Skolem constant or function.

Proof by specialization
Proofs by specialization provide a means of establishing a conjecture that contains an existential quantifier by proving an instance of the conjecture with the quantified variable replaced by a particular term.

Proofs using deduction rules
The apply command provides a means of establishing a conjecture that matches the conclusion of a deduction rule.
The proof-methods setting enables users to specify which of these methods of backward inference are applied automatically and in what order.