acl2 (math/acl2) Add to my watchlist

Applicative Common Lisp / A Computational Logic

ACL2 (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
Displaying statistics for 773 users who made submissions during: until

Statistics for selected duration

2023-Jan-06 to 2023-Feb-05


Total Installations 3
Requested Installations 3


macOS Versions

Loading Chart

Port Versions

Loading Chart



Xcode Versions

Loading Chart

CLT Versions

Loading Chart



Variants table

Variants Count


Monthly Statistics

Can remain cached for up to 24 hours