Single step tableaux for modal logics. Computational properties, complexity and methodology

DOI10.1023/A:1006155811656zbMath0951.03008OpenAlexW1601452436MaRDI QIDQ1977576

Fabio Massacci

Publication date: 17 May 2000

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1006155811656

zbMATH Keywords

modal logicdecidabilitytranslationconfluencemodularityspace complexitydecision proceduresmodal resolutionGentzen-type tableauxprefixed tableauxsingle step tableaux

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15)

Related Items (18)

Tableaux and hypersequents for justification logics ⋮ Prefixed tableaus and nested sequents ⋮ A polynomial space construction of tree-like models for logics with local chains of modal connectives ⋮ Modal interpolation via nested sequents ⋮ Implementing a relational theorem prover for modal logic ⋮ PSPACE complexity of modal logic KD45\(_{n}\) ⋮ The complexity of identifying characteristic formulae ⋮ First-Order Resolution Methods for Modal Logics ⋮ Approximations of modal logics: \(\mathbf K\) and beyond ⋮ Proofs and countermodels in non-classical logics ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Decision Procedures for a Deontic Logic Modeling Temporal Inheritance of Obligations ⋮ A new methodology for developing deduction methods ⋮ 2005 Annual Conference of the Australasian Association for Logic ⋮ Deciding regular grammar logics with converse through first-order logic ⋮ EXPtime tableaux for ALC ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube

This page was built for publication: Single step tableaux for modal logics. Computational properties, complexity and methodology