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 proofmethods setting enables users to specify which of these
methods of backward inference are applied automatically and in what order.