## FAILURE

how to deal with a proof failure
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. 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, see redo-flat.

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.