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

Schmidt, R. A., Stell, J. G. and Rydeheard, D. (2014)

In Goré, R. and Kurucz, A. (eds), Advances in Modal Logic, Volume 10. College Publications, London, 478-497, BiBTeX, PDF (final version available in the proceedings).

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.

Long version with proofs.

Accompanying website with benchmark results and more detailed analysis.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 22 Sep 14
Copyright © 2014 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk