LP, the Larch Prover -- Hints on orienting formulas into rewrite rules

If you put some well-selected ordering constraints in the registry, LP will orient formulas more quickly and with fewer surprises. Put the generators for a sort, such as 0 and s for Nat, at the bottom of the registry. Enter defining formulas, such as P(x) = P1(x) /\ P2(x), with the term being defined on the left side of the equality sign.

When a proof fails unexpectedly, look at the rewrite rules to see if any are oriented in surprising directions. If so, there are several potentially useful things to try.

Occasionally, LP will fail to orient a set of formulas for which a terminating set of rewrite rules does indeed exist. At this point you should consider changing the ordering to use a more powerful ordering strategy (e.g., the dsmpos ordering rather than noeq-dsmpos) or an ordering strategy that makes no attempt to check termination (e.g., left-to-right). It is also worth keeping in mind that although LP will not automatically give operators equal height when using noeq-dsmpos, the register command can be used to do so explicitly.