LP, the Larch Prover -- Hints on using LP
There are a number of hints that beginning users of LP may find helpful. These hints fall into the following categories.
Preparing input and recording work
Formalizing axioms and conjectures
Orienting formulas into rewrite rules
Making proofs go faster