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.