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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
<html>
<head><title>PROOF-CHECKER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>PROOF-CHECKER</h1>support for low-level interaction
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
Call this up with <code>(verify ...)</code>.<p>
<p>
<ul>
<li><h3><a href="DEFINE-PC-HELP.html">DEFINE-PC-HELP</a> -- define a macro command whose purpose is to print something
</h3>
</li>
<li><h3><a href="DEFINE-PC-MACRO.html">DEFINE-PC-MACRO</a> -- define a proof-checker macro command
</h3>
</li>
<li><h3><a href="DEFINE-PC-META.html">DEFINE-PC-META</a> -- define a proof-checker meta command
</h3>
</li>
<li><h3><a href="INSTRUCTIONS.html">INSTRUCTIONS</a> -- instructions to the proof checker
</h3>
</li>
<li><h3><a href="MACRO-COMMAND.html">MACRO-COMMAND</a> -- compound command for the proof-checker
</h3>
</li>
<li><h3><a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a> -- list of commands for the proof-checker
</h3>
</li>
<li><h3><a href="RETRIEVE.html">RETRIEVE</a> -- re-enter a (specified) <a href="PROOF-CHECKER.html">proof-checker</a> state
</h3>
</li>
<li><h3><a href="TOGGLE-PC-MACRO.html">TOGGLE-PC-MACRO</a> -- change an ordinary macro command to an atomic macro, or vice-versa
</h3>
</li>
<li><h3><a href="UNSAVE.html">UNSAVE</a> -- remove a <a href="PROOF-CHECKER.html">proof-checker</a> state
</h3>
</li>
<li><h3><a href="VERIFY.html">VERIFY</a> -- enter the interactive proof checker
</h3>
</li>
</ul>
This is an interactive system for checking theorems in ACL2. One
enters it using VERIFY; see <a href="VERIFY.html">verify</a>. The result of an
interactive session is a <code><a href="DEFTHM.html">defthm</a></code> event with an <code>:</code><code><a href="INSTRUCTIONS.html">instructions</a></code>
parameter supplied; see the documentation for proof-checker command
<code>exit</code> (in package <code>"ACL2-PC"</code>). Such an event can be replayed later
in a new ACL2 session with the ``proof-checker'' loaded.<p>
A tutorial is available on the world-wide web:
<pre>
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html
</pre>
The tutorial illustrates more than just the proof-checker. The portion
relevant to the proof-checker may be accessed directly:
<pre>
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29
</pre>
<p>
Individual proof-checker commands are documented in subsection
<a href="PROOF-CHECKER-COMMANDS.html">proof-checker-commands</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>
|
