We construct a sound, complete, and terminating tableau system for the interval temporal logic ${{\rm D}_\sqsubset}$ 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 ${{\rm D}_\sqsubset}$ -structures, and show that every formula satisfiable in ${{\rm D}_\sqsubset}$ is satisfiable in such pseudo-models, thereby proving small-model property and decidability in PSPACE of ${{\rm D}_\sqsubset}$ , a result established earlier by Shapirovsky and Shehtman by means of filtration. We also show how to extend our results to the interval logic ${{\rm D}_\sqsubset}$ interpreted over dense interval structures with proper (irreflexive) subinterval relation, which differs substantially from ${{\rm D}_\sqsubset}$ and is generally more difficult to analyze. Up to our knowledge, no complete deductive systems and decidability results for ${{\rm D}_\sqsubset}$ have been proposed in the literature so far.
Tableau Systems for Logics of Subinterval Structures over Dense Orderings / Davide Bresolin; Valentin Goranko; Angelo Montanari; Pietro Sala. - STAMPA. - 4548:(2007), pp. 73-89. (Intervento presentato al convegno 16th International Conference, TABLEAUX 2007 tenutosi a Aix en Provence, France nel July 3-6, 2007) [10.1007/978-3-540-73099-6_8].
Tableau Systems for Logics of Subinterval Structures over Dense Orderings
BRESOLIN, DAVIDE;
2007
Abstract
We construct a sound, complete, and terminating tableau system for the interval temporal logic ${{\rm D}_\sqsubset}$ 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 ${{\rm D}_\sqsubset}$ -structures, and show that every formula satisfiable in ${{\rm D}_\sqsubset}$ is satisfiable in such pseudo-models, thereby proving small-model property and decidability in PSPACE of ${{\rm D}_\sqsubset}$ , a result established earlier by Shapirovsky and Shehtman by means of filtration. We also show how to extend our results to the interval logic ${{\rm D}_\sqsubset}$ interpreted over dense interval structures with proper (irreflexive) subinterval relation, which differs substantially from ${{\rm D}_\sqsubset}$ and is generally more difficult to analyze. Up to our knowledge, no complete deductive systems and decidability results for ${{\rm D}_\sqsubset}$ have been proposed in the literature so far.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.