Sciweavers

Share
TABLEAUX
2007
Springer

Tableau Systems for Logics of Subinterval Structures over Dense Orderings

9 years 11 months ago
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...
Davide Bresolin, Valentin Goranko, Angelo Montanar
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TABLEAUX
Authors Davide Bresolin, Valentin Goranko, Angelo Montanari, Pietro Sala
Comments (0)
books