Documentation for the ACL2 Theorem Prover.
This is a parent topic for ACL2 system documentation. (We
take some liberties with the hierarchy present in the ACL2 User's Manual to
integrate certain topics into more appropriate places.)
- Sets of runes to enable/disable in concert
- Adding rules to the database
- An interactive tool for controlling ACL2's proof processes.
- Recursion and Induction
- Hash cons, function memoization, and applicative hash tables
- Functions that extend the logic
- Experimental extension for parallel execution and proofs
- Functions to display or change contents of the logical world
- Programming in ACL2
- ACL2(r) support for real numbers
- Introductory information about ACL2
- Tools for debugging failed or slow proofs, or misbehaving
- A miscellany of documented functions and concepts
(often cited in more accessible documentation)
- Methods for controlling the output produced by the ACL2 prover
- Macros allow you to extend the syntax of ACL2.
- Libraries and tools for doing basic file
i/o, using raw Common Lisp
libraries, working with the operating
system, and interfacing with other