LP, the Larch Prover -- Sample proofs: how to guide a proof

• 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 *.

• Try alternative proof strategies.
  • The cancel command lets you back up.
  • 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.