A new method for bounding the complexity of modal logics

MaRDI QIDQ4364506zbMATH OpenFDO

Authors Seán Matthews, Luca Viganò, David Basin

Publication date 7 January 1998

zbMATH Keywords

contraction rulemodal logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) Complexity of proofs (03F20)

Review text

A new proof of a result due to \textit{J. Hudelmaier} [``Improved decision procedures for the modal logics K, T, and S4, Lect. Notes Comput. Sci. 1092, 320-334 (1996)] is presented: For a suitable Gentzen-type version, the modal system K does not need the contraction rule, and for T one contraction of a given formula in a branch is enough. For the entire collection see [Zbl 0870.00023].

Recommendations

• scientific article; zbMATH DE number 1670490
• On the complexity of modal separation logics
• scientific article; zbMATH DE number 1989660
• Complexity results for modal dependence logic
• Complexity Results for Modal Dependence Logic
• On the complexity of elementary modal logics
• Complexity of modal logics with Presburger constraints
• Lower bounds for modal logics
• The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics
• A modal view on resource-bounded propositional logics

Cited in

(15)

• EXPtime tableaux for ALC
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• Correction to: ``A modal view on resource-bounded propositional logics
• A subset-matching size-bounded cache for testing satisfiability in modal logics
• scientific article; zbMATH DE number 1612554 (Why is no real title available?)
• On the relative complexity of labelled modal tableaux
• Admissibility of cut in coalgebraic logics
• On the size of shortest modal descriptions
• How to optimize proof-search in modal logics
• A New Method to Obtain Termination in Backward Proof Search For Modal Logic S4
• scientific article; zbMATH DE number 4145872 (Why is no real title available?)
• Hintikka multiplicities in matrix decision methods for some propositional modal logics
• scientific article; zbMATH DE number 1418348 (Why is no real title available?)
• Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics
• Cut elimination in coalgebraic logics

This page was built for publication: A new method for bounding the complexity of modal logics

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