ACL2

ACL2 Sources

ACL2 documentation (system only, not including the community books)

This is the ACL2 documentation. For the ACL2+Books Manual, which that includes both the ACL2 documentation and the ACL2 community-books, see the ACL2+Books Manual.

Subtopics

About-ACL2

General information About ACL2

ACL2-tutorial

Tutorial introduction to ACL2

Bdd

Ordered binary decision diagrams with rewriting

Books

Books are files of ACL2 events—they are the main way to split up large ACL2 developments into separate modules.

Debugging

Tools for debugging failed or slow proofs, or misbehaving functions.

Documentation

Information about options for downloading and viewing the ACL2 documentation, contributing documentation, and the available tools for documenting your own books.

Events

Functions that extend the logic

History

Functions to display or change contents of the logical world

Hons-and-memoization

Hash cons, function memoization, and applicative hash tables

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.

Macros

Macros allow you to extend the syntax of ACL2.

Miscellaneous

A miscellany of documented functions and concepts (often cited in more accessible documentation)

Parallelism

Experimental extension for parallel execution and proofs

Programming

Programming in ACL2

Proof-builder

An interactive tool for controlling ACL2’s proof processes.

Prover-output

Methods for controlling the output produced by the ACL2 prover

Real

ACL2(r) support for real numbers

Rule-classes

Adding rules to the database

Theories

Sets of runes to enable/disable in concert