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.
Immunize facts that you know are irreducible.
LP will not waste time trying to reduce them.
Deactivate rewrite rules that are needed only
Make definitions passive and apply them manually.
Avoid big terms, especially with
associative-commutative operators. Seek different
axiomatizations or proof strategies if they occur.
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.