@INPROCEEDINGS{SchmidtStellRydeheard14b,
AUTHOR = {Schmidt, R. A. and Stell, J. G. and Rydeheard, D.},
YEAR = {2014},
TITLE = {Axiomatic and Tableau-Based Reasoning for Kt(H,R)},
EDITOR = {Gor{\'e}, R. and Kurucz, A.},
BOOKTITLE = {Advances in Modal Logic, Volume 10},
PUBLISHER = {College Publications},
ADDRESS = {London},
PAGES = {478--497},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/SchmidtStellRydeheard14b.html}},
ABSTRACT = {
We introduce a tense logic, called Kt(H,R), arising from logics for
spatial reasoning. Kt(H,R) is a multi-modal logic with two modalities
and their converses defined with respect to a pre-order and a
relation stable over this pre-order. We show Kt(H,R) is decidable,
it has the effective finite model property and reasoning in Kt(H,R)
is PSPACE-complete. Two complete Hilbert-style axiomatisations are
given. The main focus of the paper is tableau-based reasoning. Our
aim is to gain insight into the numerous possibilities of defining
tableau calculi and their properties. We present several labelled
tableau calculi for Kt(H,R) in which the theory rules range from
accommodating correspondence properties closely, to accommodating
Hilbert axioms closely. The calculi provide the basis for decision
procedures that have been implemented and tested on modal and
intuitionistic problems.
},
}