ACL2 System Architecture

The user interacts with the theorem prover by giving it definitions, theorems and advice. Most often the advice is about how to store each proved theorem as a rule. Sometimes the advice is about how to prove a specific theorem.

The database consists of all the rules ACL2 ``knows.'' It is possible to
include in the database all of the rules in some certified file of other
events. Such certified files are called books

Interesting proofs are usually built on top of many books, some of which
are written especially for that problem domain and others of which are about
oft-used domains, like arithmetic or list processing. ACL2's distribution
includes many books written by users. See the ``books'' link under the
**Lemma Libraries and Utilities**