Building decision procedures for modal logics from propositional decision procedures: The case study of modal K(m).
DOI10.1006/INCO.1999.2850zbMATH Open1033.03509OpenAlexW2021025450MaRDI QIDQ1854375FDOQ1854375
Authors: Fausto Giunchiglia, Roberto Sebastiani 
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
Recommendations
- Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
- Evaluating optimized decision procedures for propositional modal \(\mathbf K(m)\) satisfiability
- Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability
- Modal Satisfiability via SMT Solving
- SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
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 Taming of the Cut. Classical Refutations with Analytic Cut
- A machine program for theorem-proving
- 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?)
- Strongly analytic tableaux for normal modal logics
- First-order modal tableaux
- Title not available (Why is that?)
- Exploiting the deep structure of constraint problems
- Ordered binary decision diagrams and the Davis-Putnam procedure
Cited In (24)
- Generalizing DPLL and satisfiability for equalities
- Towards an efficient library for SAT: A manifesto
- Evaluating optimized decision procedures for propositional modal \(\mathbf K(m)\) satisfiability
- SAT-based decision procedures for classical modal logics
- Title not available (Why is that?)
- SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
- The SAT-based approach to separation logic
- Implementing tableau calculi using BDDs: BDDTab system description
- BDD-based decision procedures for the modal logic K ★
- Tableau reductions: towards an optimal decision procedure for the modal necessity
- Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
- Modal Satisfiability via SMT Solving
- Optimizing terminological reasoning for expressive description logics
- Formulating the template ILP consistency problem as a constraint satisfaction problem
- Complexity analysis of propositional resolution with autarky pruning
- Evaluating optimised decision procedures for propositional modal \({\mathbf K}_{({\mathbf m})}\) satisfiability
- Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ $\mathcal{ALC}$
- Title not available (Why is that?)
- Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving
- A conflict-driven solving procedure for poly-power constraints
- Title not available (Why is that?)
- Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
- InKreSAT: modal reasoning via incremental reduction to SAT
- Automated reasoning in modal and description logics via SAT encoding: the case study of \(K_m/\mathcal{ALC}\)-satisfiability
This page was built for publication: Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1854375)
