Structured theory development for a mechanized logic

DOI10.1023/A:1026517200045MaRDI QIDQ1595929zbMATH OpenOpenAlexFDO

Authors Matt Kaufmann, J Strother Moore

Publication date 18 February 2001

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1026517200045

zbMATH Keywords

ACL2automated reasoningconstraintencapsulationfirst-order logicfunctional instantiationsoundness

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

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.

Recommendations

• Towards a mechanically checked theory of computation. The ACL2 project
• scientific article; zbMATH DE number 2101985
• Milestones from the Pure Lisp Theorem Prover to ACL2
• A theorem prover for a computational logic
• scientific article; zbMATH DE number 2079835

Cited in

(21)

• Integrating external deduction tools with ACL2
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• Formal logics of discovery and hypothesis formation by machine
• Modelling algebraic structures and morphisms in ACL2
• Formal verification of a generic framework to synthesize SAT-provers
• Theory extension in ACL2(r)
• Towards a mechanically checked theory of computation. The ACL2 project
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• ACL2s: ``the ACL2 sedan
• On definitions of constants and types in HOL
• Towards robustness analysis using PVS
• An ACL2 Tutorial
• Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
• Proof pearl: a formal proof of Higman's lemma in ACL2
• scientific article; zbMATH DE number 2079835 (Why is no real title available?)
• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• Efficient execution in an automated reasoning environment
• A theorem prover for a computational logic
• Formal verification of a deadlock detection algorithm
• A step-indexing approach to partial functions
• Rewriting with equivalence relations in ACL2

Describes a project that uses

Uses Software

• ACL2
• LISP
• NQTHM

This page was built for publication: Structured theory development for a mechanized logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1595929)