ACL2 theorem prover
ACL2 is a mechanical theorem prover
whose underlying logic is based on an applicative subset of Common Lisp
. It is also written in the same applicative subset of Common Lisp that it provides and can be run in most Common Lisp implementations. It has a high degree of automation and its specifications can be directly compiled and executed by the underlying Common Lisp implementation. ACL2 is an "industrial strength" version of the Boyer-Moore theorem prover, NQTHM.
For detailed information see: