An ACL2 Tutorial

We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to provide ideas for other interactive theorem prover projects; and to elicit feedback on how we might incorporate features of other proof tools into ACL2.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Matt Kaufmann, J. Strother Moore
• Keywords: ACL2 Theorem Prover, Artificial Intelligence, Interactive Theorem Prover, Proof Tools, TPHOL 2008