The light side of interval temporal logic: The Bernays-Sch\uf6nfinkel fragment of CDT

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDT_BS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Sch\uf6nfinkel class. In addition, we show that CDT_BS is in fact NP-complete (Bernays-Sch\uf6nfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Sch\uf6nfinkel class. Finally, we show that any increase in the negation depth of CDT_BS modalities immediately yields undecidability