		Search-engine friendly clone of the ACL2 documentation.

Note-2-6

Note-2-6-proofs

ACL2 Version 2.6 Notes on Changes in Proof Engine

Certain optimizations are performed when converting terms to clausal form. For example, (< 0 1) is known to be t, (HARD-ERROR ctx str alist) is known to be nil, and (INTEGERP n) is known to imply (RATIONALP n).

In earlier versions of ACL2, the conversion of a term to clausal form expanded LAMBDA applications. That may no longer occur. Some proofs may slow down (or fail) because your LAMBDA-expressions are not expanded away when you ``expected'' them to be.

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.

A bug has been fixed in the handling of :type-prescription rules by the bdd package. Thanks to Rob Sumners for discovering this bug and supplying a helpful example.

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 :induct t.

We eliminated the rule-class linear-alias. This rule class was seldom used and complicated the linear arithmetic decision procedure in ways that made it difficult to extend to handle some non-linear special cases. The only use of the rule-class that we know of was in our own Nqthm books, which were an attempt to provide an embedding of the Nqthm logic and theorem prover into ACL2. But that facility was also practically never used, as far as we know. So both linear-alias rules and the Nqthm books have been eliminated.

In earlier versions of ACL2, when the IF-form of (AND p q) was assumed true — as when rewriting the alpha expression in (IF (AND p q) alpha beta) — the assumption mechanism did not deduce that p and q are true, only that their conjunction, in its IF-form, is true. This has long been known as a deficiency in both ACL2 and the earlier Nqthm but it was tedious to do better when one considered the full range of IF-forms one might encounter in the test of another IF. Rather than code all the cases, we just waited until clausification got rid of them. Robert Krug developed a pretty nice treatment of the general case and we added it in this version. This also involved a surprising number of changes elsewhere in the system because the improved handling of assumptions caused the theorem prover often to ``erase'' hypotheses provided by :use hints because it could simplify them to t. Thank you Robert!

In response to a suggestion from Robert Krug, we added mfc-ap so that extended metafunctions can take advantage of linear arithmetic. See extended-metafunctions.

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 (f) preceded the constant 2, that is no longer the case. If this change is noticed at all, it will probably be noticed in how so-called permutative rewrite rules are applied; see loop-stopper. Thanks to Robert Krug for suggesting this improvement and providing part of the implementation.