

ACL2  A Computational Logic for Applicative Common Lisp 

ABC
DEF
GHI
JKL
MNO
PQR
STU
VWX
YZ
ACL2  A Computational Logic for Applicative Common Lisp
http://www.cs.utexas.edu/users/moore/acl2/acl2doc.html
University of Texas at Austin  USA
A sucessor of Nqthm  BoyerMoore theorem prover
ACL2 is both a mathematical logic and system of mechanical tools which can be used to construct proofs in the logic. The logic, which formalizes a subset of Common Lisp, is a high level programming language which can be executed efficiently on many host platforms. Thus, programmers can define models of computational systems and these models can be executed ("simulated") to test them on concrete data. But because the language is also a formal mathematical logic it is possible to reason about the models symbolically. Indeed, it is possible to prove theorems establishing properties of the models and to check these proofs with mechanical tools that are part of the ACL2 system. The ACL2 system is essentially a reimplemented extension, for applicative Common Lisp, of the socalled "BoyerMoore theorem prover" Nqthm.
/Kaufmann, 1997/ Industrial Strength Theorem Prover for a Logic Based on Common Lisp
FirstOrder Logic
Type Checking
Types of Systems: Sequential systems
Development Phases: Verification
Development Phases: Proof  Theorem Prover
Development Phases: Reasoning
GDPA Online
Last Updated 01.Jan.2002
Updated by Webmaster
Last Revised 01.Jan.2002
Revised by Webmaster

