Single step tableaux for modal logics. Computational properties, complexity and methodology
From MaRDI portal
Publication:1977576
DOI10.1023/A:1006155811656zbMath0951.03008OpenAlexW1601452436MaRDI QIDQ1977576
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
modal logicdecidabilitytranslationconfluencemodularityspace complexitydecision proceduresmodal resolutionGentzen-type tableauxprefixed tableauxsingle step tableaux
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
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
