ACL2 System Architecture

The user interacts with the theorem prover by giving it definitions, theorems and advice (e.g., ``use this lemma.''), often in the form of books books .

The theorem prover uses the rules in the library of books the user has selected.

The theorem prover prints its proof attempts to the user.

When a theorem is proved it is converted to a rule under the control of the user's rule-classes .

The informed user can make ACL2 do amazing things.