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 result...

• Type: Conference
• Year: 2007
• Where: TABLEAUX
• Authors: Davide Bresolin, Valentin Goranko, Angelo Montanari, Pietro Sala
• Keywords: Artificial Intelligence, Dense Linear Orderings, Interval Structures, Interval Temporal Logic, TABLEAUX 2007