Formal rules can be carried out by machine.

The ACL2 machine above interacts with the user to find formal mathematical proofs of conjectures posed by the user. In the illustration above,

• ACL2 announces that the conjecture P is a theorem and shows a proof.
• The user helps the machine by suggesting a key lemma, Q, to be proved first.

[Next] [Research] [Home]