1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
<html>
<head><title>FAILURE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>FAILURE</h2>how to deal with a proof failure
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
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 <a href="GENERALIZE.html">generalize</a>s 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.
<p>
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. However, see <a href="PROOF-TREE.html">proof-tree</a> for a utility that
may be very helpful in locating parts of the failed proof that are
of particular interest. 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).<p>
If the failure occurred during a forcing round,
see <a href="FAILED-FORCING.html">failed-forcing</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
