PROOF-CHECKER

support for low-level interaction
Major Section:  ACL2 Documentation

Call this up with (verify ...).

Some Related Topics

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.