LP, the Larch Prover -- Release 3.1a

The following bugs in Version 3.1 have been fixed in Version 3.1a.
95-001
The command register top a b only registered a at the top of the registry. LP no longer ignores b.
95-002
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.
95-003
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.
95-004
LP generated an unhandled exception when trying to simplify an if__then__else__ containing a quantifier.
95-005 (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 write-mode qualified setting to ensure that the write command supplies the required parentheses when printing such assertions.
95-006 (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 non-minimal extensions to the registry.
95-007
When the subgoal for a proof by specialization contained an ac operator, LP was not able to prove the subgoal even though the show normal-form command showed that it reduced to true.
95-008
LP failed to apply the rewrite rule P(x, x) -> true to the term P(\E i A(i), \E j A(j)).
95-009
LP did not print the correct subgoal levels in response to display proof.
95-010
LP did not treat the default proof methods as local to the current proof context.
95-011
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.
95-012
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.
95-013 (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.