Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
DOI10.1007/3-540-61511-3_115zbMATH Open1415.03022OpenAlexW1605860778MaRDI QIDQ4647549FDOQ4647549
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
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 \(\mathbf K(m)\) satisfiability
- Modal Satisfiability via SMT Solving
- BDD-based decision procedures for the modal logic K ★
Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- The Taming of the Cut. Classical Refutations with Analytic Cut
- A machine program for theorem-proving
- Attributive concept descriptions with complements
- Multilanguage hierarchical logics, or: How we can do without modal logics
- Embedding complex decision procedures inside an interactive theorem prover.
- A guide to completeness and complexity for modal logics of knowledge and belief
- Title not available (Why is that?)
- Title not available (Why is that?)
- Strongly analytic tableaux for normal modal logics
- Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
- First-order modal tableaux
- Title not available (Why is that?)
- Title not available (Why is that?)
- Ordered binary decision diagrams and the Davis-Putnam procedure
Cited In (17)
- A new method for testing decision procedures in modal logics
- Evaluating optimized decision procedures for propositional modal \(\mathbf K(m)\) satisfiability
- Implementing tableau calculi using BDDs: BDDTab system description
- A loop-free decision procedure for modal propositional logics K4, S4 and S5
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- BDD-based decision procedures for the modal logic K ★
- EXPtime tableaux for ALC
- 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
Uses Software
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)
