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.
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.
To install acl2, run the following command in macOS terminal (Applications->Utilities->Terminal)
sudo port install acl2
To see what files were installed by acl2, run:
port contents acl2
To later upgrade acl2, run:
sudo port selfupdate && sudo port upgrade acl2
Reporting an issue on MacPorts Trac
The MacPorts Project uses a system called Trac to file tickets to report bugs and enhancement requests.
Though anyone may search Trac for tickets, you must have a GitHub account in order to login to Trac to create tickets.