Integrating external deduction tools with ACL2

DOI10.1016/J.JAL.2007.07.002MaRDI QIDQ1006728zbMATH OpenOpenAlexFDO

Authors Matt Kaufmann, Sandip Ray, Erik Reeber, J Strother Moore

Publication date 25 March 2009

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2007.07.002

zbMATH Keywords

first-order logictheorem provinginterfacesautomated reasoningdecision procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• An ACL2 Tutorial
• Milestones from the Pure Lisp Theorem Prover to ACL2
• The ACL2 Sedan theorem proving system
• ACL2s: ``the ACL2 sedan
• Structured theory development for a mechanized logic

Cites work

• scientific article; zbMATH DE number 1629957 (Why is no real title available?)
• scientific article; zbMATH DE number 3748393 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• scientific article; zbMATH DE number 1863374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Algorithms for ordinal arithmetic.
• Automated Reasoning
• Combining WS1S and HOL
• Correct Hardware Design and Verification Methods
• Formal Methods in Computer-Aided Design
• Integrating external deduction tools with ACL2
• Interpolants and Symbolic Model Checking
• Isabelle/HOL. A proof assistant for higher-order logic
• Meta Reasoning in ACL2
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Structured theory development for a mechanized logic
• Verification Condition Generation Via Theorem Proving

Cited in

(4)

• Extending ACL2 with SMT solvers
• Integrating external deduction tools with ACL2
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• An ACL2 Tutorial

Describes a project that uses

Uses Software

• HOL90
• PROSPER
• Ivy
• LISP
• Chaff
• SMT-LIB
• ACL2

This page was built for publication: Integrating external deduction tools with ACL2

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