Integrating external deduction tools with ACL2

DOI10.1016/j.jal.2007.07.002zbMath1183.68558OpenAlexW2024791001MaRDI QIDQ1006728

Erik Reeber, Matt Kaufmann, Sandip Ray, 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

theorem provinginterfacesfirst-order logicautomated reasoningdecision procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (3)

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Integrating external deduction tools with ACL2
• Structured theory development for a mechanized logic
• Isabelle/HOL. A proof assistant for higher-order logic
• A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Automated Reasoning
• Verification Condition Generation Via Theorem Proving
• Interpolants and Symbolic Model Checking
• Meta Reasoning in ACL2
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• Automated Deduction – CADE-19

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