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.