Research News
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,
Nqthm,
and its interactive enhancement,
Pc-Nqthm.
Visit the ACL2 home page for more
information including guided tours, documentation and instructions for
obtaining the latest release.
http://dirleton.csres.utexas.edu/software/acl2/index.html
This page is URL http://www.computationallogic.com/software/acl2/index.html