Axiomatic and Tableau-Based Reasoning for Kt(H,R)

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 though, 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.

The paper is to appear in "Advances in Modal Logic", Volume 10, 2014.