Embedding complex decision procedures inside an interactive theorem prover.

DOI10.1007/BF01530803zbMath1034.68541OpenAlexW2047580205MaRDI QIDQ1353946

Enrico Giunchiglia, Alessandro Armando

Publication date: 12 May 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01530803

Mathematics Subject Classification ID

Related Items

The SAT-based approach to separation logic, Structured proof procedures, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Programming for modular reconfigurable robots, Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).

Uses Software

• Nuprl
• Automath
• LCF
• GETFOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eliminating dublication with the hyper-linking strategy
• A structure-preserving clause form translation
• Seventy-five problems for testing automatic theorem provers
• Prolegomena to a theory of mechanized formal reasoning
• Completely non-clausal theorem proving
• Solving propositional satisfiability problems
• Edinburgh LCF. A mechanized logic of computation
• Nonclausal deduction in first-order temporal logic
• Algorithms for testing the satisfiability of propositional formulae
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Theorem Proving via General Matings
• Reasoning About Recursively Defined Data Structures
• A Computational Study of Satisfiability Algorithms for Propositional Logic
• A Machine-Oriented Logic Based on the Resolution Principle
• On Cores and Prime Implicants of Truth Functions
• A Computing Procedure for Quantification Theory