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.
