The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT
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.
- Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
- Interval temporal logics over finite linear orders: the complete picture
- The dark side of interval temporal logic: marking the undecidability border
- Interval temporal logics over strongly discrete linear orders: the complete picture
- Interval temporal logics over strongly discrete linear orders: expressiveness and complexity
- A Decidable Spatial Logic with Cone-Shaped Cardinal Directions
- A general tableau method for propositional interval temporal logics: theory and implementation
- A Modal Logic for Chopping Intervals
- A propositional modal logic of time intervals
- A Road Map of Interval Temporal Logics and Duration Calculi
- B and D are enough to make the Halpern-Shoham logic undecidable
- Decidability of the interval temporal logic \(\operatorname{AB\overline{B}}\) over the natural numbers
- Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification
- Definability with bounded number of bound variables
- Expressiveness and completeness of an interval tense logic
- Extending Kamp's Theorem to Model Time Granularity
- First-order logic with two variables and unary temporal logic
- scientific article; zbMATH DE number 747023 (Why is no real title available?)
- scientific article; zbMATH DE number 834561 (Why is no real title available?)
- Maintaining knowledge about temporal intervals
- Maximal decidable fragments of Halpern and Shoham's modal logic of intervals
- Metric propositional neighborhood logics: expressiveness, decidability, and undecidability
- Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
- Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders
- Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
- The classical decision problem.
- The guarded fragment with transitive guards
- Two variable first-order logic over ordered domains
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Computational complexity of hybrid interval temporal logics
- On coarser interval temporal logics
- Hybrid fragments of Halpern-Shoham logic and their expressive power
- Sub-propositional fragments of the interval temporal logic of Allen's relations
- Extracting interval temporal logic rules: a first approach
- Fuzzy Halpern and Shoham's interval temporal logics
- Decision tree learning with spatial modal logics
This page was built for publication: The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2251124)
