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

BRESOLIN, Davide;SALA, Pietro
2007-01-01

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.
2007
9783540730989
Temporal Logic; Interval logic; decidability
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/312541
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 9
social impact