ACL2 is a mathematical logic and a mechanical theorem prover to help you reason in the logic (which is a subset of applicative Common Lisp). The theorem prover is an ``industrial strength version of the Boyer-Moore theorem prover, Nqthm. Users can build models of all kinds of computing systems in ACL2, just as in Nqthm, even though the formal logic is Lisp. Once you've built an ACL2 model of a system, you can run it and use ACL2 to prove theorems about the model.
DocumentationUser install guide available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-9/installation.html; User guide available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-9/The_Tours.html; User reference manual available in HTML format from http://www.cs.utexas.edu/users/moore/acl2/v2-9/acl2-doc.html#User's-Manual
released on 22 April 2005
|License||Verified by||Verified on||Notes|
|GPLv2||Janet Casey||3 June 2002|
Leaders and contributors
|J Strother Moore||Maintainer|
Resources and communication
This entry (in part or in whole) was last reviewed on 7 January 2008.