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 Boyer-Moore theorem prover. ACL2 can be used to automatically or semi-automatically 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 semi-automatic theorem prover. Because the meta-language is the same as the language (a subset of Common Lisp), it is very flexible.
Version: 8.3 License: BSD
GitHub
| Maintainers | JacksonIsaac |
| Categories | math |
| Homepage | http://www.cs.utexas.edu/users/moore/acl2/v8-3 |
| 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)
1
Requested Installations (30 days)
1
Livecheck results
acl2 seems to have been updated (port version: 8.3, new version: 8.6)
livecheck ran: 7 hours ago