Major Section: MISCELLANEOUS
When ACL2 gives up it does not mean that the submitted conjecture is invalid, even if the last formula ACL2 printed in its proof attempt is manifestly false. Since ACL2 sometimes generalizes the goal being proved, it is possible it adopted an invalid subgoal as a legitimate (but doomed) strategy for proving a valid goal. Nevertheless, conjectures submitted to ACL2 are often invalid and the proof attempt often leads the careful reader to the realization that a hypothesis has been omitted or that some special case has been forgotten. It is good practice to ask yourself, when you see a proof attempt fail, whether the conjecture submitted is actually a theorem.
If you think the conjecture is a theorem, then you must figure out from ACL2's output what you know that ACL2 doesn't about the functions in the conjecture and how to impart that knowledge to ACL2 in the form of rules. The ``key checkpoint'' information printed at the end of the summary provides a fine place to start. See the-method for a general discussion of how to prove theorems with ACL2, and see introduction-to-the-theorem-prover for a more detailed tutorial. Also see set-gag-mode for discussion of key checkpoints and an abbreviated output mode that focuses attention on them. You may find it most useful to start by focusing on key checkpoints that are not under a proof by induction, if any, both because these are more likely to suggest useful lemmas and because they are more likely to be theorems; for example, generalization may have occurred before a proof by induction has begun. If you need more information than is provided by the key checkpoints -- although this should rarely be necessary -- then you can look at the full proof, perhaps with the aid of certain utilities: see proof-tree, see set-gag-mode, and see set-saved-output.
For information on a tool to help debug failures of encapsulate and
progn events, as well as certify-book failures, see redo-flat.
Again, see the-method for a general discussion of how to prove theorems with ACL2, and see introduction-to-the-theorem-prover for a more detailed tutorial. See also the book ``Computer-Aided Reasoning: An Approach'' (Kaufmann, Manolios, Moore), as well as the discussion of how to read Nqthm proofs and how to use Nqthm rules in ``A Computational Logic Handbook'' by Boyer and Moore (Academic Press, 1988).
If the failure occurred during a forcing round, see failed-forcing.
