LP, the Larch Prover -- Sample proofs: how to guide a proof
Here are some things to try when LP and/or you get stuck trying to prove a
conjecture.
Try a proof method based on the form of the conjecture. For example, try
resume by <=> if the conjecture is a logical equivalence. Sometimes such
proof methods are useful ``no-brainers''.
Think about why you believe the conjecture.
If you've forgotten where you are in a proof, type
display proof to see the current subgoal
display *Hyp to see the current hypotheses
display to see all facts
history to see how you got where you are
Be skeptical: maybe the conjecture isn't a theorem.
Try a proof by cases, either to simplify the current subgoal or to make some
hypothesis more useful.
Look for a useful lemma to prove.
Try using the critical-pairs command to derive consequences from the
hypotheses, for example, by typing critical-pairs *Hyp with *.
The freeze and thaw commands let you save LP's state in a file and get
it back again.
Think again about why you still believe the conjecture.
Try explaining why LP must be broken to a colleague. (The colleague does not
need to understand anything about LP. He or she simply needs to appear to be
listening attentively.)
If you still believe that LP is broken, send e-mail to larch@lcs.mit.edu.