\doc{Backward inference}
\ref{backward-inference}

The \cflink{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 \dlink{of-dr}{deduction rules}, \dlink{of-ir}{induction rules}, and
\dlink{of-ot}{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.
\p
\begin{description}
\dt Proof by \dlink{by-normalization}{normalization}
\dd
Normalization rewrites conjectures.  If a conjecture normalizes to \fq{true},
it is a theorem.  Otherwise the normalized conjecture becomes the subgoal to be
proved.
\p
\dt Proof by \dlink{by-cases}{cases}
\dd
A proof by cases divides a proof into specified cases, enabling the conjecture
to be rewritten further using the case hypotheses.
\p
\dt Proof by \dlink{by-contradiction}{contradiction}
\dd
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.
\p
\dt Proof by \dlink{by-induction}{induction} 
\dd
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.
\p
\dt Proof of \dlink{of-conditional}{conditionals}
\dd
Proofs of conditionals are simplified proofs by cases applicable to conjectures
of the form \fq{(if t1 then t2 else t3) = t4}, where \fq{t4} does not begin
with \fq{if}.
\p
\dt Proof of \dlink{of-conjunction}{conjunctions}
\dd
Proofs of conjunctions provide a way to reduce the expense of equational term
rewriting when proving conjectures of the form \fq{t1 /\ ... /\ tn}.
\p
\dt Proof of \dlink{of-implication}{implications}
\dd
Proofs of implications are simplified proofs by cases applicable to conjectures
of the form \fq{t1 => t2}.
\p
\dt Proof of \dlink{of-biconditional}{logical equivalence}
\dd
Proofs of logical equivalence are simplified proofs by cases applicable to
conjectures of the form \fq{t1 <=> t2}.
\p
\dt Proof by \dlink{by-generalization}{generalization}
\dd
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.
\p
\dt Proof by \dlink{by-specialization}{specialization}
\dd
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.
\p
\dt Proofs using deduction rules
\dd
The \clink{apply} command provides a means of establishing a conjecture that
matches the conclusion of a deduction rule.
\end{description}
The \setlink{proof-methods} setting enables users to specify which of these
methods of backward inference are applied automatically and in what order.