ACL2 Version 2.6 Notes on Changes in Proof Engine
Certain optimizations are performed when converting terms to
clausal form. For example,
In earlier versions of ACL2, the conversion of a term to clausal form
Robert Krug found a soundness bug in our linear arithmetic package. The bug was caused by the derivation of an equation from two inequalities without taking adequate precautions to ensure that both sides of the inequalities were numeric. Robert also kindly provided a fix which we adopted. Thanks Robert!
We fixed a bug that could prevent the application of a metatheorem.
A bug has been fixed that had caused bogus forcing rounds (see forcing-round). The bug could occur when the hypothesis of a rule was forced (see force) before the prover decided to start over and prove the original goal by induction. Thanks to Rob Sumners for drawing our attention to this problem.
Some low-level fixes have been made that prevent certain infinite loops, based on reports by users. We thank Yunja Choi, Matt Wilding, and Pete Manolios for reporting such problems.
An obscure potential soundness hole has been fixed by redoing the way evaluation takes place in the ACL2 loop and during theorem proving. We expect that users will see no difference based on this change. (Those interested in the details can see the long comment ``Essay on Evaluation in ACL2'' in source file interface-raw.lisp.)
A small change was made in computation for a heuristic that controls backchaining. This will speed up proofs dramatically in a very few cases but should have a very small impact in general.
The simplifier has been modified to avoid eliminating hypotheses of goals that can be established by contextual (specifically, type-set) reasoning alone. We believe that this change will generally strengthen ACL2's reasoning engine, although on rare occasions a lemma that formerly was provable may require user assistance. Thanks to Robert Krug for suggesting this change and providing its implementation.
Case splits are now limited, by default. This may allow some proof attempts to provide output where previously the prover would appear to ``go out to lunch.'' For a more complete discussion, including instructions for how users can control case splitting, see set-case-split-limitations.
ACL2 may now use the built-in induction scheme for a function symbol even
if that function symbol is disabled. Formerly, if a function symbol was
disabled then its induction scheme was only considered if an explicit
induction hint was supplied, other than
We eliminated the rule-class
In earlier versions of ACL2, when the
In response to a suggestion from Robert Krug, we added
There is less delay in printing goals. In previous versions, a goal was not printed until its subgoals were created (or the goal was proved). Now, the goal is printed essentially as soon as it is created.
A small technical change has been made in the function term-order,
to give priority on the function symbol count over the weighting of constants.
So for example, while previously the term