Tableau Systems for Logics of Subinterval Structures over Dense Orderings

摘要

We construct a sound, complete, and terminating tableau system for the interval temporal logic D interpreted in interval structures over dense linear orderings endowed with strict subinterval relation (where both endpoints of the sub-interval are strictly inside the interval). In order to prove the soundness and completeness of our tableau construction, we introduce a kind of finite pseudo-models for our logic, called D -structures, and show that every formula satisfiable in D is satisfiable in such pseudo-models, thereby proving small-model property and decidability in PSPACE of D, a result established earlier by Shapirovsky and Shehtman by means of filtration. We also show how to extend our results to the interval logic D interpreted over dense interval structures with proper (irreflexive) subinterval relation, which differs substantially from D and is generally more difficult to analyze. Up to our knowledge, no complete deductive systems and decidability results for D have been proposed in the literature so far.