The Computational Complexity of Provability in Systems of Modal Propositional Logic

DOI10.1137/0206033zbMath0373.02025OpenAlexW2073491323MaRDI QIDQ4149442

Richard E. Ladner

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 (only showing first 100 items - show all)

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

This page was built for publication: The Computational Complexity of Provability in Systems of Modal Propositional Logic