acl2 (math/acl2) Add to my watchlist
Applicative Common Lisp / A Computational LogicACL2 (Applicative Common Lisp / A Computational Logic) is the successor to nqthm, the BoyerMoore theorem prover. ACL2 can be used to automatically or semiautomatically prove theorems and has been used extensively in real applications (e.g., proving the correctness of certain calculations in the floating point unit of the AMD K5 microprocessor. ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semiautomatic theorem prover. Because the metalanguage is the same as the language (a subset of Common Lisp), it is very flexible.
Version: 8.3 License: BSD GitHubMaintainers  JacksonIsaac 
Categories  math 
Homepage  http://www.cs.utexas.edu/users/moore/acl2/v83 
Platforms  darwin 
Variants 

"acl2" depends on
lib (1)
build (1)
Ports that depend on "acl2"
No ports
Port notes
Users who want to use ACL2 for serious work should
install the certify variant (sudo port install +certify),
which will certify (i.e., prove all of the theorems)
in the included examples. This can take several hours.
Port Health:
Loading Port Health
Installations (30 days)
3
Requested Installations (30 days)
3
Livecheck results
acl2 seems to have been updated (port version: 8.3, new version: 8.5)
livecheck ran: 1 day, 7 hours ago