## 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** link of the ACL2 home page.