Formal verification of a generic framework to synthesize SAT-provers

DOI10.1007/BF03177742zbMath1096.68094MaRDI QIDQ2583288

Jose Antonio Alonso, Francisco Jesús Martín-Mateos, María José Hidalgo, José Luis Ruiz-Reina

Publication date: 16 January 2006

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Mathematics Subject Classification ID

Related Items (4)

A logic-algebraic tool for reasoning with knowledge-based systems ⋮ An approach from answer set programming to decision making in a railway interlocking system ⋮ Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations ⋮ Formally verified tableau-based reasoners for a description logic

Uses Software

• ACL2

Cites Work

• Structured theory development for a mechanized logic
• Implementing the Davis-Putnam method
• Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formal verification of a generic framework to synthesize SAT-provers