Integrating external deduction tools with ACL2
type: Item
instance of: scholarly article
title: Integrating external deduction tools with ACL2
zbMATH Open document ID: 1183.68558
author: Matt Kaufmann
author: Sandip Ray
author: Erik Reeber
author: J Strother Moore
published in: Journal of Applied Logic
publication date: 2009-03-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 5532933
zbMATH Keywords: automated reasoning
zbMATH Keywords: decision procedures
zbMATH Keywords: first-order logic
zbMATH Keywords: interfaces
zbMATH Keywords: theorem proving
describes a project that uses: SMT-LIB
describes a project that uses: LISP
describes a project that uses: Ivy
describes a project that uses: HOL90
describes a project that uses: ACL2
describes a project that uses: Chaff
describes a project that uses: PROSPER
MaRDI profile type: Publication
full work available at URL: j.jal.2007.07.002
OpenAlex ID: W2024791001
cites work: Interpolants and Symbolic Model Checking
cites work: A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
cites work: A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
cites work: Structured theory development for a mechanized logic
cites work: Q3932277
cites work: Q5573961
cites work: Automated Deduction – CADE-19
cites work: Q4016540
cites work: Formal Methods in Computer-Aided Design
cites work: Verification Condition Generation Via Theorem Proving
cites work: Q5287513
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q3997095
cites work: Meta Reasoning in ACL2
cites work: A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
cites work: Correct Hardware Design and Verification Methods
cites work: Q4790648
cites work: Combining WS1S and HOL
cites work: Q2729073
cites work: Programming Combinations of Deduction and BDD-based Symbolic Calculation
cites work: Automated Reasoning
cites work: Q4809048
DOI: 10.1016/J.JAL.2007.07.002
description: scientific article; zbMATH DE number 5532933