Major Section: ACL2 Documentation
Call this up with (verify ...).
This is an interactive system for checking ACL2 theorems, or at least
exploring their proofs. One enters it using the VERIFY command
(see verify), and then invokes commands at the resulting prompt to operate
on a stack of goals, starting with the single goal that was supplied to
VERIFY. The final command (or ``instruction'') can be an exit
command, which can print out a defthm event if the goal stack is empty;
see proof-checker-commands, in particular the exit command. That
resulting defthm event includes an :instructions parameter,
which directs replay of the proof-checker commands (for example during
certification of a book containing that event; see books).
If you exit the proof-checker interactive loop, you may re-enter that session
at the same point using the command (verify), i.e., with no arguments.
The commands save and retrieve may be invoked to manage more than one
session.
The proof-checker can be invoked on a specific subgoal, and the resulting
:instructions can be given as a hint to the theorem prover for that
subgoal. See instructions.
A tutorial is available on the world-wide web:
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html.
The tutorial illustrates more than just the proof-checker. The portion
relevant to the proof-checker may be accessed directly:
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29
See set-evisc-tuple for how to arrange that output is printed in abbreviated
form. In general, the proof-checker uses the :TERM evisc-tuple
described in that documentation.
Individual proof-checker commands are documented in subsection
proof-checker-commands. When inside the interactive loop (i.e., after
executing verify), you may use the help command to get a list of
legal instructions and (help instr) to get help for the instruction
instr.
