ACL2
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.)
Subtopics
- 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
- Start-here
- Introductory information about 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
- 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.
