Terminating tableau systems for hybrid logic with difference and converse

Journal of Logic, Language and Information 18 (4):437-464 (2009)
  Copy   BIBTEX

Abstract

This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence theorem.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,100

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-04-27

Downloads
54 (#296,486)

6 months
4 (#795,160)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Modal Logic: Graph. Darst.Patrick Blackburn, Maarten de Rijke & Yde Venema - 2001 - New York: Cambridge University Press. Edited by Maarten de Rijke & Yde Venema.
An introduction to modal logic.G. E. Hughes - 1968 - London,: Methuen. Edited by M. J. Cresswell.
Semantical Analysis of Modal Logic I. Normal Propositional Calculi.Saul A. Kripke - 1963 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9 (5‐6):67-96.
An Introduction to Modal Logic.George Edward Hughes & M. J. Cresswell - 1968 - London, England: Methuen. Edited by M. J. Cresswell.

View all 12 references / Add more references