The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT (Q2251124)

Interval temporal logics are modal logics, propositions of which are evaluated over intervals rather than points. One of the most elaborated among such logics is Yde Venema's system CDT, which deals with the binary modalities \(C\) (for the ternary relation \textit{chop}), \(D\) (for \textit{done}), and \(T\) (\textit{to do}). Taken in full generality, the satisfiability problem in CDT turns out to be undecidable, just like in many other interval temporal systems, such as Halpern and Shoham's logic HS. In this paper, a certain fragment of CDT is considered, called CDT\(_{\mathrm{BS}}\), which consists of all and only those formulas where the modalities \(C\), \(D\), and \(T\) can occur in the scope of at most one negation. The authors introduce the so-called \textit{standard translation} (ST) of the CDT-formulas into the formulas of the first-order logic, defined as follows: \(\mathrm{ST}(\varphi)[x,y]\) = \(x\leq y \wedge\mathrm{ST}^{\prime}(\varphi)[x,y]\), where \(x\), \(y\) are two first-order variables, and \(\mathrm{ST}^{\prime}(\varphi)[x,y]\) is defined inductively for any CDT-formula. It is shown that the standard translation defined so maps CDT\(_{\mathrm{BS}}\) formulas into the so-called \textit{Bernays-Schönfinkel class}, which consists of all and only first-order formulas in prenex form with the quantifier prefix of the form \(\exists x_1 \ldots{} \exists x_n \forall y_1 \ldots{} \forall y_m\), the matrix of which may include predicate symbols of any arity (but no function symbols) and, possibly, equality. Since Bernays-Schönfinkel class is known to be decidable, the decidability of CDT\(_{\mathrm{BS}}\) immediately follows. The expressive completeness of CDT\(_{\mathrm{BS}}\) with respect to a suitable fragment of such a class is proved, and a sound, complete and terminating tableau method for CDT\(_{\mathrm{BS}}\) is formulated.