## ACL2 as an Interactive Theorem Prover (cont)

When ACL2 proves a lemma, it is converted into one or more **rules** and
stored in a **database**. The theorem prover is **rule-driven**. By proving
lemmas you can configure ACL2 to behave in certain ways when it is trying to
prove formulas in a certain problem domain. The expert user can make ACL2 do
amazingly ``smart'' looking things.

But it would be wrong to think that ACL2 *knows* the mathematical content
of a formula just because it has proved it. What ACL2 knows -- all ACL2
knows -- is what is encoded in its rules. There are many types of rules
(see rule-classes ).

Many formulas can be effectively coded as rules. But by the same token, it
is possible to encode a formula as a rule that is so ineffective it cannot
even prove itself!

The way a formula is stored as a rule is entirely up to the user. That is,
**you** determine how ACL2 should use each formula that it proves.

The most common kind of rule is the **rewrite rule**. It is so common that
if you don't tell ACL2 how to store a formula, it stores it as a rewrite
rule.