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

  • Identification
  • Homepage
  • Institution
  • Observations
  • Publications
  • Classifications
  • Identification

    ACL2 - A Computational Logic for Applicative Common Lisp



    University of Texas at Austin - USA


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


    /Kaufmann, 1997/ Industrial Strength Theorem Prover for a Logic Based on Common Lisp


    First-Order 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