Minimal structures for modal tableaux: Some examples

Luis Fariñas del Cerro, Olivier Gasquet



In this paper we present some examples of decision procedures based on tableau calculus for some mono- and multimodal logics having a semantics involving properties that are not easily representable in tree-like structures (like e.g. density, confluence and persistence). We show how to handle them in our framework by generalizing usual tableaux (which are trees) to richer structures: rooted directed acyclic graphs.

Full Text:



Laurent Catach, Les logiques multi-modales, Ph.D. thesis, Universit´ e Paris VI, France, 1989.

G. De Giacomo, F. Massacci. “Tableau and algorithm for propositional dynamic logic with converse”. In M.A. McRobbie, J.K. Slaney editor, Proc. CADE-13, LNAI 1104, Springer, 1996.

S. Demri, E. Orłowska. “Every finitely reductible logic has the finite model property with respect to the class of 3-formulae”. Bulletin of the Section of Logic, to appear in Studia Logica.

H.C.M. de Swart. “Gentzen-type systems for C, K and several extensions of C and K; constructive completeness proofs and effective decision procedure for these systems”. Logique et Analyse, 1980.

Marcos A. Castilho, Luis Fari˜ nas del Cerro, Olivier Gasquet, and Andreas Herzig. “Modal tableaux with propagation rules and structural rules”. Fundamenta Informaticæ 32(3/4):281–297, 1997.

Luis Fariñas del Cerro, and Olivier Gasquet. “Tableaux based decision procedures for modal logics of confluence and density”. Fundamenta Informaticæ 41(1):1–17, 2000.

M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht, 1983.

M. Fitting. “Basic modal logic”. In D. Gabbay et al., editor, Handbook of Logic in Artificial Intelligence and Logic Programming: Logical Foundations, vol. 1, Oxford University Press, 1993.

S. Kripke. “A completeness theorem in modal logic”. Journal of Symbolic Logic 24, 1959.

S. Kripke. “Semantical analysis of modal logic I: Normal modal propositional calculi”. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9, 1963.

F. Massacci. “Strongly analytic tableaux for normal modal logics”. In Alan Bundy editor, Proc. CADE-12, LNAI 814, Springer, 1994.

E. Orłowska. “Relational formalization of non-classical logics”. In Brink, Kahl, Schmidt editor, Relational Methods in Computer Science, pp. 91–105, Springer-Verlag, 1997.

H. Sahlqvist. “Completeness and correspondence in the first and second order semantics for modal logics”. In S. Kanger editor, Proc. 3rd Scandinavian Logic Symposium 1973, Studies in Logic 82 (1975), North-Holland, 1973.

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism