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
Set automatic-registry off, instruct LP to order only
the offending formula, and choose one of the presented
suggestions that order the formula as desired.
Then add register commands corresponding to that suggestion to your
command file and try running the proof again.
Alternatively, rerun the proof at a trace-level (e.g., 2) that prints
out extensions to the registry; then use a text editor and the .lplog file
to locate extensions dealing with operators appearing in the offending rewrite
rule. This may suggest a set of register commands that will force the
formulas to be ordered as desired.
Alternatively, rerun the proof with automatic-registry off to
find a set of suggestions that will order things the way you want them. Then
add register commands with the appropriate suggestions to your command
file, and execute it again with automatic-registry on. This
last step is important because proof scripts with automatic-registry
off are not usually robust.