The Computational Complexity of Provability in Systems of Modal Propositional Logic

DOI10.1137/0206033zbMath0373.02025OpenAlexW2073491323MaRDI QIDQ4149442

Publication date: 1977

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/44fb82e6a7e9eb8a08d3e1c0b80171bce8e47f28

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45)

Related Items

Decidability of order-based modal logics, The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics, Conditional logics of normality: A modal approach, Complexity of interpolation and related problems in positive calculi, Axiomatization and completeness of lexicographic products of modal logics, Belief, awareness, and limited reasoning, Satisfiability in many-valued sentential logic is NP-complete, The Complexity of Satisfiability for Fragments of Hybrid Logic—Part I, Complexity of modal logics with Presburger constraints, Graph decompositions and tree automata in reasoning with uncertainty, The complexity of concept languages, Derivability in certain subsystems of the logic of proofs is \(\Pi_2^p\)-complete, Complexity of admissible rules, Uniform interpolation and propositional quantifiers in modal logics, Open answer set programming for the semantic web, Complexity of computing with extended propositional logic programs, A class of decidable information logics, Three-valued logics in modal logic, Modal logics for reasoning about infinite unions and intersections of binary relations, Modal Inclusion Logic: Being Lax is Simpler than Being Strict, Complexity results of STIT fragments, Loop-free calculus for modal logic S4. I, Computational complexity of the word problem in modal and Heyting algebras with a small number of generators, What is an inference rule?, Lower complexity bounds in justification logic, A polynomial space construction of tree-like models for logics with local chains of modal connectives, Symmetric blocking, Complexity of some problems in positive and related calculi, Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction), The complexity of satisfiability for fragments of hybrid logic. I., Complexity of hybrid logics over transitive frames, Application of modal logic to programming, An NP-complete fragment of fibring logic, Classifying the computational complexity of problems, Deciding the word problem in pure double Boolean algebras, Modal logic S5 in answer set programming with lazy creation of worlds, On the size of refutation Kripke models for some linear modal and tense logics, On the polynomial-space completeness of intuitionistic propositional logic, On the Decision Problem for Two-Variable First-Order Logic, Coalgebraic semantics of modal logics: an overview, Hypothetical datalog: Complexity and expressibility, Complexity results for modal dependence logic, Mathematical modal logic: A view of its evolution, The decision problem of provability logic with only one atom, On the relationship between fuzzy description logics and many-valued modal logics, Control machines: A new model of parallelism for compositional specifications and their effective compilation, On the complexity of the closed fragment of Japaridze's provability logic, Public announcement logic with distributed knowledge: expressivity, completeness and complexity, TABLEAUX: A general theorem prover for modal logics, 3-SAT = SAT for a class of normal modal logics, The fluted fragment with transitive relations, The complexity of identifying characteristic formulae, A guide to completeness and complexity for modal logics of knowledge and belief, Complexity of validity for propositional dependence logics, Hybrid logics: characterization, interpolation and complexity, Parameterized modal satisfiability, Rules with parameters in modal logic. II., The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic, A logic for reasoning about counterfactual emotions, The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions, General default logic, Generalized modal satisfiability, The NP-Completeness of Reflected Fragments of Justification Logics, Computational complexity for bounded distributive lattices with negation, Unnamed Item, How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning, Propositional dynamic logic of regular programs, SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation, On the Complexity of the Equational Theory of Residuated Boolean Algebras, Weak Kripke Structures and LTL, Complexity of the universal theory of modal algebras, The price of universality, Minimal temporal epistemic logic, An Epistemic Logic with Hypotheses, Complexity of intuitionistic propositional logic and its fragments, THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆, Domino-tiling games, Adding clauses to poor man's logic (without increasing the complexity), BDD-based decision procedures for the modal logic K ★, Dynamic logics of the region-based theory of discrete spaces, Modal Logics for Parallelism, Orthogonality, and Affine Geometries, Axiomatization and Completeness of Lexicographic Products of Modal Logics, A simple propositional \(\text{S}5\) tableau system, Deciding regular grammar logics with converse through first-order logic, On the proof complexity of logics of bounded branching, The complexity of hybrid logics over equivalence relations, Hybrid logics of separation axioms, EXPtime tableaux for ALC, The complexity of the disjunction and existential properties in intuitionistic logic, NP reasoning in the monotone \(\mu\)-calculus, Guarded fixed point logics and the monadic theory of countable trees., Combining deduction and model checking into tableaux and algorithms for converse-PDL., Tractable reasoning via approximation, The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic, Undecidability of Multi-modal Hybrid Logics, A modal perspective on the computational complexity of attribute value grammar, Generalized quantifiers and modal logic, Deciding the guarded fragments by resolution, \({\mathcal E}\)-connections of abstract description systems, Efficient SAT-based minimal model generation methods for modal logic S5, On the Decidability of Elementary Modal Logics, On Composing Finite Forests with Modal Logics, Modal Logics with Hard Diamond-Free Fragments, ON THE COMPLEXITY OF COALITIONAL REASONING, Separation logics and modalities: a survey, Frame definability in finitely valued modal logics, Mechanising Gödel-Löb provability logic in HOL light, Completing the Picture: Complexity of Graded Modal Logics with Converse, Hintikka multiplicities in matrix decision methods for some propositional modal logics, From KLM-style conditionals to defeasible modalities, and back, Lattice logic as a fragment of (2-sorted) residuated modal logic, Unnamed Item, Team semantics for the specification and verification of hyperproperties, Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic, A note on the complexity of S4.2, A simple tableau system for the logic of elsewhere, Efficient loop-check for backward proof search in some non-classical propositional logics, A logic for metric and topology, Topological modal logics satisfying finite chain conditions, Unnamed Item, LOGICS AND ALGEBRAS FOR MULTIPLE PLAYERS, On the Restraining Power of Guards, A nonstandard approach to the logical omniscience problem, THE TEMPORAL LOGIC OF TWO DIMENSIONAL MINKOWSKI SPACETIME IS DECIDABLE, A nonstandard approach to the logical omniscience problem, The Complexity of Decomposing Modal and First-Order Theories, Expressivity and Complexity of Dependence Logic, Proof Complexity of Non-classical Logics, Unnamed Item, The Fluted Fragment with Transitivity, The Complexity of Satisfiability for Fragments of CTL and CTL⋆, Hyper arrow logic with indiscernibility and complementarity, Hyper arrow logic with indiscernibility and complementarity, Model Checking and Validity in Propositional and Modal Inclusion Logics, Semiring Provenance for Guarded Logics, Modal Logic S5 Satisfiability in Answer Set Programming