Integrating external deduction tools with ACL2

DOI10.1016/J.JAL.2007.07.002zbMATH Open1183.68558OpenAlexW2024791001MaRDI QIDQ1006728FDOQ1006728

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

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

zbMATH Keywords

first-order logictheorem provinginterfacesautomated reasoningdecision procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

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

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

Uses Software

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

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)