		Search-engine friendly clone of the ACL2 documentation.

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.
Recursion-and-induction: Recursion and Induction
Hons-and-memoization: Hash cons, function memoization, and applicative hash tables
Events: Functions that extend the logic
Parallelism: Experimental extension for parallel execution and proofs
History: Functions to display or change contents of the logical world
Programming: Programming in ACL2
Operational-semantics: Modeling State Machines
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.