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.)

- Theories
- Sets of runes to enable/disable in concert
- Rule-classes
- Adding rules to the database
- Proof-builder
- An interactive tool for controlling ACL2's proof processes.
- Hons-and-memoization
- Hash cons, function memoization, and applicative hash tables
- Events
- Functions that extend the logic
- History
- Functions to display or change contents of the logical world
- Parallelism
- Experimental extension for parallel execution and proofs
- Programming
- Programming in ACL2
- Real
- ACL2(r) support for real numbers
- ACL2-tutorial
- Tutorial introduction to ACL2
- Debugging
- Tools for debugging failed or slow proofs, or misbehaving functions.
- Miscellaneous
- A miscellany of documented functions and concepts (often cited in more accessible documentation)
- Output-controls
- Methods for controlling the output produced by the ACL2 prover
- Built-in-theorems
- Built-in theorems.
- Macros
- Macros allow you to extend the syntax of ACL2.
- Interfacing-tools
- Libraries and tools for doing basic
file i/o, using raw Common Lisp libraries, working with the operating system, and interfacing with other programs. - About-ACL2
- General information About ACL2