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)

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)