## 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. Books could be written about this, but they
haven't been yet. However, see proof-tree for a utility that
may be very helpful in locating parts of the failed proof that are
of particular interest. See also 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.