{"name":"acl2","portdir":"math/acl2","version":"8.3","license":"BSD","platforms":"darwin","epoch":0,"replaced_by":null,"homepage":"http://www.cs.utexas.edu/users/moore/acl2/v8-3","description":"Applicative Common Lisp / A Computational Logic","long_description":"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.","active":true,"categories":["math"],"maintainers":[{"name":"ijackson","github":"JacksonIsaac","ports_count":44}],"variants":["emacs","ccl","certify","regression","nonstd"],"dependencies":[{"type":"build","ports":["clang-15"]},{"type":"lib","ports":["sbcl"]}],"depends_on":[]}