LP, the Larch Prover -- Release 3.1a
The following bugs in Version 3.1 have been fixed in Version 3.1a.
In addition, the following improvements have been made in Version 3.1a.
The command register top a b only registered a at the top of the
registry. LP no longer ignores b.
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.
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.
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.
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.
LP failed to apply the rewrite rule P(x, x) -> true to the term
P(\E i A(i), \E j A(j)).
LP did not print the correct subgoal levels in response to display proof.
LP did not treat the default proof methods as local to the current proof
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.
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.
A variant, freeze-current, 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.