Building decision procedures for modal logics from propositional decision procedures — The case study of modal K

DOI10.1007/3-540-61511-3_115zbMath1415.03022OpenAlexW1605860778MaRDI QIDQ4647549

Roberto Sebastiani, Fausto Giunchiglia

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_115

zbMATH Keywords

modal logicdecision procedurepropositional variabletruth assignmentmodal atom

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction), Hybrid Tableaux for the Difference Modality, A new method for testing decision procedures in modal logics, An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,׆, SAT-based explicit LTL reasoning and its application to satisfiability checking, EXPtime tableaux for ALC

Uses Software

• TPTP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Attributive concept descriptions with complements
• First-order modal tableaux
• A guide to completeness and complexity for modal logics of knowledge and belief
• The TPTP problem library. CNF release v1. 2. 1
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• 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