Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).

DOI10.1006/inco.1999.2850zbMath1033.03509OpenAlexW2021025450MaRDI QIDQ1854375

Roberto Sebastiani, Fausto Giunchiglia

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1999.2850

zbMATH Keywords

propositional modal logicsdecision procedures

Mathematics Subject Classification ID

Related Items (9)

Generalizing DPLL and satisfiability for equalities ⋮ The SAT-based approach to separation logic ⋮ Unnamed Item ⋮ Complexity analysis of propositional resolution with autarky pruning ⋮ Formulating the template ILP consistency problem as a constraint satisfaction problem ⋮ Optimizing terminological reasoning for expressive description logics ⋮ A conflict-driven solving procedure for poly-power constraints ⋮ BDD-based decision procedures for the modal logic K ★ ⋮ Modal Satisfiability via SMT Solving

Cites Work

• Unnamed Item
• Unnamed Item
• First-order modal tableaux
• A guide to completeness and complexity for modal logics of knowledge and belief
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Exploiting the deep structure of constraint problems
• Embedding complex decision procedures inside an interactive theorem prover.
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• Strongly analytic tableaux for normal modal logics
• A machine program for theorem-proving

This page was built for publication: Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).