|
|
|---|
|
|
|
|---|
How to deal with a failure to admit an event
There are many reasons why an event can fail to be admitted. Generally, an error message will explain the failure, sometimes pointing to documentation that is specific to the relevant issue. There are tools that can sometimes help: for example, to debug failures of encapsulate or progn events, as well as certify-book failures, see redo-flat.
However, proof failures are typically not as trivial to debug as, for
example, syntactic errors (such as spelling errors in the name of a function).
Fortunately, ACL2 offers a variety of techniques for dealing with proof
failures, and some are discussed below. Also see relevant subtopics of the
topic, debugging. Some frequently-used tools for proof debugging that
are discussed in those subtopics include accumulated-persistence, break-rewrite, with-brr-data, cgen, and proof-builder.
Also see nil-goal for ideas about how to proceed when the prover
generates a goal of
We turn now to the problem of dealing with proof failures.
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 pso, set-gag-mode, and proof-tree. System hackers may want to consider using the utility, checkpoint-list.
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.