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

Maintainers	JacksonIsaac
Categories	math
Homepage	http://www.cs.utexas.edu/users/moore/acl2/v8-3
Platforms	darwin
Variants	ccl (Use ccl as the underlying lisp) certify (Certify the included books) emacs (Include support for using acl2 under emacs) nonstd (Build the nonstandard analysis books for handling real numbers) regression (Run the regression test suite (nb: takes hours))

"acl2" depends on

lib (1)

sbcl

build (1)

clang-15

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.

acl2 (math/acl2) Add to my watchlist

"acl2" depends on

lib (1)

build (1)

Ports that depend on "acl2"

Port notes

Port Health:

Installations (30 days)

2

Requested Installations (30 days)

2

Livecheck results

acl2 (math/acl2) Add to my watchlist 1

"acl2" depends on

lib (1)

build (1)

Ports that depend on "acl2"

Port notes

Port Health:

Installations (30 days)

2

Requested Installations (30 days)

2

Livecheck results

acl2 (math/acl2) Add to my watchlist