ACL2 as an Interactive Theorem Prover (cont)

Theorems, lemmas, definitions, and advice of various sorts can be stored in books .

When a theorem or definition is stored in a book, the user can specify how it should be used in the future. When viewed this way, theorems and definitions are thought of as rules.

The ACL2 theorem prover is rule driven. The rules are obtained from books.

Click here to continue.