LP, the Larch Prover -- Hints on preparing input and recording work


Use an editor to prepare a command file containing declarations and assertions. Then execute that file to check that LP can read what you have typed. If you have made any mistakes, edit the command file to fix them.

Put all the declarations you expect to need at the beginning of your command file. This allows LP to check your declarations before beginning any time consuming tasks.

Although proofs are usually constructed interactively, successful proofs should be recorded in cleaned-up command files. Structure your proofs using a sequence of execute commands.

Freeze LP's state often. This makes it easier to try different alternatives when looking for a proof.

Always set scripting and logging on at the start of an LP session. If you realize that you are not recording a session, start logging and then execute a history all command to get LP to print the commands already executed. After executing a step of a proof, enter a comment recording information that may be helpful in cleaning up the LP-produced .lpscr file. If, for example, a critical-pairs command produced no useful critical pairs, record that fact in a comment.

Keep in mind that LP automatically indents and annotates .lpscr files. It is often useful to use an editor to replace parts of human-generated .lp files with material extracted from .lpscr files.