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.