ACL2 stands for A Computational Logic for Applicative Common Lisp.
It is a theorem proving system authored by Matt Kaufmann and J Moore, with very
significant contributions by Bob Boyer. Thus, it has been developed by the
authors of the Boyer-Moore system,
and its interactive enhancement,
Visit the ACL2 home page for more
information including guided tours, documentation and instructions for
obtaining the latest release.
This page is URL http://www.computationallogic.com/software/acl2/index.html