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.