Structured theory development for a mechanized logic (Q1595929)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Structured theory development for a mechanized logic
scientific article

    Statements

    Structured theory development for a mechanized logic (English)
    0 references
    0 references
    0 references
    18 February 2001
    0 references
    Several aspects concerning the structuring mechanisms for the ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover are presented in this paper. A brief overview of ACL2 is realized. Two notions of admissibility for recursive definitions are introduced. The notion of ACL2 history is introduced and this notion formalizes the result of a user's interaction with ACL2. The theorems of a chronology are consequences of its axioms.
    0 references
    first-order logic
    0 references
    automated reasoning
    0 references
    ACL2
    0 references
    constraint
    0 references
    encapsulation
    0 references
    functional instantiation
    0 references
    soundness
    0 references
    0 references
    0 references
    0 references

    Identifiers