Description
Interpreter and prover for a Lisp dialect.
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".
ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.
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.
The community books are also included and certified with the make everything target.