ACL2 - A Computational Logic for Applicative Common Lisp

A-B-C- D-E-F- G-H-I- J-K-L- M-N-O- P-Q-R- S-T-U- V-W-X- Y-Z

Contents		Identification Homepage Institution Observations Publications Classifications

Identification

Homepage

Institution

Observations

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 re-implemented extension, for applicative Common Lisp, of the so-called "Boyer-Moore theorem prover" Nqthm.

Publications

Classifications

GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster