LP, the Larch Prover -- Hints on making proofs go faster


When LP seems too slow, use the statistics command to find out which activities are consuming a lot of time. If rewriting (particularly, unsuccessful rewriting) is costly, try one of the following. If ordering is costly, put ordering constraints in the registry, particularly if you have declared many operators. It may also help to put ordering constraints in the registry prior to a proof by cases to save the cost of having LP rediscover these constraints in each of the cases.

If unification or critical pairing is costly, try to use smaller rule lists as arguments to the critical-pairs command. Also, try to avoid computing critical pairs between rewrite rules that contain subterms such as t1 /\ t2 /\ ... /\ t5, with multiple occurrences of the same associative-commutative operator.