LP, the Larch Prover — Release 3.1b

95-014

The normalize command now properly normalizes a rewrite rule with a reducible left side. Formerly, it failed to normalize a rewrite rule when its left side could be reduced, but no further reductions were possible.

95-015

The operation of boolean equality is now recognized as an ac operator and not just as a commutative operator. Formerly, LP incorrectly (and unsoundly) eliminated some subterms when reducing formulas such as a = (r = (b = b')) that contain multiple occurrences of equality between boolean subformulas.

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.