LP, the Larch Prover -- Release 3.1b

95-014

The normalize command now properly normalizes a rewrite rule with a reducible left side.

95-015

The operation of boolean equality is now recognized as an ac operator, and not just as a commutative operator.

95-016

The experimental version of LP (invoked by the command lp -e) no longer crashes when a register command is issued during a proof.

98-001

The bound variable i1 in

f(i, j) <=> \A i1 \A j1 (i ~= i1 \/ j ~= j1 => P(i1, j1))

is no longer changed incorrectly to i2 when executing show normal-form f(i2, i1).

• LP now contains an experimental implementation of an enhanced dsmpos ordering, which can be activated by the lp -debug command and used to prove the termination of rewriting systems in the presence of ac operators. The enhanced ordering uses a variant, developed in collaboration with Deepak Kapur, of the multiset comparison.
• The command display conjectures <names> now shows only the current conjecture when no names are specified. To show all named conjectures, the user must now type display conjectures (*). The parentheses are required, lest the command be parsed as display conjectures*.
• The class expressions contains-operator(<operator>) and contains-variable(<variable>) now allow an unqualified operator or variable to be overloaded, in which case the class expression names all facts containing at least one of the overloading.
• The routines that display the precedence relation (for the write and display commands) now display a generating subset of the relation, not the entire relation.
• There is now a class expression contains-match(<term>), which matches all facts that contain a subterm matching the given term.