ACL2 theorem prover

ACL2 is a mechanical theorem prover that supports automated reasoning in inductive logic theories. ACL2's object logic, i.e., the formal system in which propositions can be stated, can be viewed as an applicative subset of the programming language Common Lisp. Besides some bootstrapping code, most of the system in written in the same applicative subset of Common Lisp that it provides and can be run in most Common Lisp implementations. The system provides a high degree of automation and its specifications can be directly compiled and executed by the underlying Common Lisp implementation. ACL2 is intended to be an "industrial strength" version of the Boyer-Moore theorem prover, NQTHM .

External link

• http://www.cs.utexas.edu/users/moore/acl2/