LP, the Larch Prover  Release 3.1a
The following bugs in Version 3.1 have been fixed in Version 3.1a.
 95001

The command register top a b only registered a at the top of the
registry. LP no longer ignores b.
 95002

When LP discovered an inconsistency during an attempt to prove the subgoal
justifying a proof by cases, it did not propagate the inconsistency to the
parent context. LP now propagates the inconsistency. This action is sound,
because the subgoal did not introduce any additional hypotheses.
 95003

When using the rewrite rule n <= m > \E k (n + k = m) to reduce the term
n <= k, LP unsoundly renamed the bound variable k to n. It now
renames it to n1.
 95004

LP generated an unhandled exception when trying to simplify an
if__then__else__ containing a quantifier.
 95005 (Partially fixed)

LP interpreted commands like assert commutative(plus) and
assert ac(plus) as syntactically incorrect assertions of operator
theories, rather than as assertions of formulas. This problem has been
corrected, but assertions like assert ac + remain ambiguous. LP resolves
such ambiguities by parsing them as operator theories, rather than as formulas
consisting of a constant followed by a postfix operator. Users who want the
latter interpretation can type assert (ac+). They should also use the
default set writemode qualified setting to ensure that the write
command supplies the required parentheses when printing such assertions.
 95006 (Partially fixed)

LP had difficulty orienting some equations like a+a+b = c+d+d, which
contain operators with multiset status applied to repeated subterms, into
terminating rewrite rules. LP now correctly orients such equations, but it
does so in some cases by making nonminimal extensions to the registry.
 95007

When the subgoal for a proof by specialization contained an ac operator,
LP was not able to prove the subgoal even though the show normalform
command showed that it reduced to true.
 95008

LP failed to apply the rewrite rule P(x, x) > true to the term
P(\E i A(i), \E j A(j)).
 95009

LP did not print the correct subgoal levels in response to display proof.
 95010

LP did not treat the default proof methods as local to the current proof
context.
 95011

LP required the user to qualify an overloaded variable v in the command
instantiate v by c in *, even when the sort of v could be determined
from that of c.
 95012

LP could not prove a deduction rule that contained an ac operator in its
conclusion even though its logical system contained a rewrite rule equivalent
to that deduction rule.
 95013 (Partially fixed)

LP generated an unhandled overflow when using the polynomial ordering to orient
a long formula into a rewrite rule. LP behaves more gracefully now, but at the
expense of orienting the formula.
In addition, the following improvements have been made in Version 3.1a.

A variant, freezecurrent, of the freeze
command freezes only the current proof attempt. This variant makes it faster
to use freeze and thaw to try different strategies for the current
proof attempt. It also consumes less disk space.

The tracer now shows the accumulated CPU time at trace level 3 or higher
whenever it discovers that more than 15 seconds of CPU time have elapsed.