Interpreter and prover for a Lisp dialect

<rendered-html><p>ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. “ACL2” denotes “A Computational Logic for Applicative Common Lisp”.</p> <p>ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.</p> <p>This package installs the main ACL2 executable acl2, as well as the build tools cert.pl and clean.pl, renamed to acl2-cert and acl2-clean.</p> <p>The community books are also included and certified with the <code>make everything</code> target.</p> </rendered-html>