Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K

DOI10.1007/3-540-61511-3_115MaRDI QIDQ4647549zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability
• Evaluating optimized decision procedures for propositional modal K(m) satisfiability
• Modal Satisfiability via SMT Solving
• BDD-based decision procedures for the modal logic K ★

Cites work

• scientific article; zbMATH DE number 67503 (Why is no real title available?)
• scientific article; zbMATH DE number 1149402 (Why is no real title available?)
• scientific article; zbMATH DE number 1149437 (Why is no real title available?)
• scientific article; zbMATH DE number 1995157 (Why is no real title available?)
• A guide to completeness and complexity for modal logics of knowledge and belief
• A machine program for theorem-proving
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Attributive concept descriptions with complements
• Embedding complex decision procedures inside an interactive theorem prover.
• First-order modal tableaux
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Strongly analytic tableaux for normal modal logics
• The TPTP problem library. CNF release v1. 2. 1
• The Taming of the Cut. Classical Refutations with Analytic Cut

Cited in

(17)

• A new method for testing decision procedures in modal logics
• Evaluating optimized decision procedures for propositional modal K(m) satisfiability
• A loop-free decision procedure for modal propositional logics K4, S4 and S5
• Implementing tableau calculi using BDDs: BDDTab system description
• Reasoning with propositional logic: from SAT solvers to knowledge compilation
• EXPtime tableaux for ALC
• BDD-based decision procedures for the modal logic K ★
• An analysis of empirical testing for modal decision procedures
• Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
• Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• An improved set-based reasoner for the description logic \(\mathcal{DL}_\mathrm{D}^{4,\times\dagger}\)
• Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability
• Solving graded/probabilistic modal logic via linear inequalities (system description)
• Hybrid tableaux for the difference modality
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• SAT-based explicit LTL reasoning and its application to satisfiability checking

Describes a project that uses

Uses Software

• TPTP

This page was built for publication: Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647549)