Reasoning About Time in DatalogMTL: Course Notes

We focus on the original setting for DatalogMTL, where the timeline is dense and consists of rational numbers. However, it is worth noting that DatalogMTL was also considered over the discrete integer timeline [47]. Formally, we let the (rational) timeline be the set $\mathbb{Q}$ of rational (both positive and negative) numbers and we will call each element of the timeline a time point. An interval $\varrho$ is a non-empty subset of $\mathbb{Q}$ satisfying the following standard properties:

• $\mathrm{■}$

  for all $t_1,t_2,t_3\in \mathbb{Q}$ with and $t_1,t_3\in \varrho$, it is the case that $t_2\in \varrho$, and

• $\mathrm{■}$

  both the greatest lower bound ${\varrho }^{-}$ and the least upper bound ${\varrho }^{+}$ of $\varrho$ belong to $\mathbb{Q}\cup \{-\mathrm{\infty },\mathrm{\infty }\}$.

The bounds ${\varrho }^{-}$ and ${\varrho }^{+}$ are called the left and right endpoints of $\varrho$, respectively, and ${\varrho }^{+}-{\varrho }^{-}$ is the length of $\varrho$. An interval $\varrho$ is punctual if it contains exactly one number, it is positive if it does not contain negative numbers (i.e., $\varrho \subseteq {\mathbb{Q}}_{\ge 0}$), and it is bounded if both its left and right endpoints are rational numbers.

We use the standard representation $⟨{\varrho }^{-},{\varrho }^{+}⟩$ for intervals $\varrho$, where the left bracket $⟨$ is either $[$ or $($, the right bracket $⟩$ is either $]$ or $)$, and ${\varrho }^{-}$ and ${\varrho }^{+}$ are representations of the left and right endpoints of $\varrho$, respectively. For example, the following represent three different intervals: $[2⁤\frac{1}{2},4]$, $(2⁤\frac{1}{2},4]$, and $[2⁤\frac{1}{2},4)$. As usual, brackets $[$ and $]$ indicate that the corresponding endpoints are included in the interval, whereas $($ and $)$ indicate that they are not included. We abbreviate a punctual interval $[t,t]$ as $t$. For example instead of $[2⁤\frac{1}{2},2⁤\frac{1}{2}]$ we may simply write $2⁤\frac{1}{2}$.

We let a relational atom be of the form $P(𝐬)$, with $P$ an $n$-ary predicate and $𝐬$ an $n$-ary tuple of terms (i.e., constants and variables). For example $\text{Vaccinated}(\mathrm{𝖡𝖾𝗇})$ is a relational atom with a predicate Vaccinated of arity 1 and with a single constant $\mathrm{𝖡𝖾𝗇}$, whereas $\text{Vaccinated}(x)$ is a relational atom using a variable $x$ instead of a constant. We allow also for predicates of arity 0, such as Sunny, which do not require terms. A metric atom is an extension of a relational atom with metric temporal operators. In particular, a metric atom is an expression given by the following grammar, where $P(𝐬)$ ranges over relational atoms and $\varrho$ over positive non-empty intervals:

For example ${\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-02-20-19-50-15-page-1.pdf2svg.svg" id="S2.SS2.p1.m14.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="7" height="9" style="width: 14px; height: unset; max-width: 100\%"></object>}}_{(10,183]}\text{Infected}(x)$ is a metric atom. Notice that the definition allows also for arbitrary nesting of temporal operators, so ${⊞}_{[11,14]}{\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-02-20-19-50-15-page-1.pdf2svg.svg" id="S2.SS2.p1.m15.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="7" height="9" style="width: 14px; height: unset; max-width: 100\%"></object>}}_{(10,183]}\text{Infected}(x)$ is also a metric atom.

A rule is an expression built from metric atoms as follows:

where each $M_i$ is a metric atom and $M^{\prime }$ is a metric atom allowing only for “boxes” among temporal operators, namely $M^{\prime }$ is generated by the following grammar:¹¹1Notice that we disallow $\perp$ in $M^{\prime }$, which ensures that no inconsistency can occur; DatalogMTL is often considered with rules allowing for $\perp$ in $M^{\prime }$, but to simplify the setting we will not consider such rules.

The fact that we disallow some temporal operators in $M^{\prime }$ is dictated by complexity results; if we allow for $M^{\prime }$ being an arbitrary metric atom, reasoning would become undecidable. The conjunction $M_1\wedge \mathrm{\cdots }\wedge M_n$ in Expression (5) is the rule’s body, each $M_i$ is a body atom, and $M^{\prime }$ is the rule’s head. As an example of DatalogMTL rules, consider Rules (1)–(4) from ${\mathrm{\Pi }}_{\mathrm{𝖾𝗑}}$ in Example 2. A program, like ${\mathrm{\Pi }}_{\mathrm{𝖾𝗑}}$, is a finite set of rules²²2Precisely speaking we require also that rules are safe, namely each variable mentioned in the head of a rule occurs also in its body, and this occurrence is not in a left operand of $𝒮$ or $𝒰$; without this restriction we could write rules like $Q(x)\leftarrow P$, which are usually disallowed in Datalog..

An expression (e.g. a metric atom, rule, or program) is ground if it mentions no variables. Hence $\text{Vaccinated}(\mathrm{𝖡𝖾𝗇})$ is ground, but $\text{Vaccinated}(x)$ is not. A fact over an interval $\varrho$ is an expression $M\mathrm{@}\varrho$, with $M$ a ground relational atom. A dataset, for example ${𝒟}_{\mathrm{𝖾𝗑}}$ from Example 1, is a finite set of facts.

The grounding of a program $\mathrm{\Pi }$, written as $\mathrm{𝗀𝗋𝗈𝗎𝗇𝖽}(\mathrm{\Pi })$, is the ground program obtained as the set of all ground rules that can be obtained by assigning constants to variables in $\mathrm{\Pi }$. The grounding of $\mathrm{\Pi }$ with respect to a dataset $𝒟$, written as $\mathrm{𝗀𝗋𝗈𝗎𝗇𝖽}(\mathrm{\Pi },𝒟)$, is the restriction of $\mathrm{𝗀𝗋𝗈𝗎𝗇𝖽}(\mathrm{\Pi })$ rules which do mention only those constants which are present in $\mathrm{\Pi }$ or $𝒟$.

We will focus in this course on the standard continuous semantics of DatalogMTL, as opposed to the alternative pointwise semantics [36]. In the standard setting an interpretation $\Im$ is a function which specifies, for each ground relational atom $P(𝐬)$ and each time point $t$, whether $P(𝐬)$ is satisfied at $t$, in which case we write $\Im ,t\vDash P(𝐬)$. This notion extends to complex ground metric atoms as given in Table 1.

The meaning of past operators , $\boxminus$, and $𝒮$ is additionally visualised in figures below. The first figure shows that ${\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-02-20-19-50-15-page-1.pdf2svg.svg" id="S2.SS3.p2.m4.g1nest" class="ltx\_graphics ltx\_img\_portrait" width="7" height="9" style="width: 14px; height: unset; max-width: 100\%"></object>}}_{[1,2]}P$ holds at $3⁤\frac{1}{10}$ if $P$ holds at some time point located within the interval $[1⁤\frac{1}{10},2⁤\frac{1}{10}]$. The second figure indicates that ${\boxminus }_{[1,2]}P$ holds at $3⁤\frac{1}{10}$ if $P$ holds continuously in the interval $[1⁤\frac{1}{10},2⁤\frac{1}{10}]$. The third figure, in turn, shows that $Q{𝒮}_{[1,2]}P$ holds at $3⁤\frac{1}{10}$ if $P$ holds at some time point within $[1⁤\frac{1}{10},2⁤\frac{1}{10}]$ and $Q$ holds continuously from this time point up to the time point $3⁤\frac{1}{10}$. The meaning of future operators , $⊞$, and $𝒰$ is symmetric to the meaning of the corresponding past operators , $\boxminus$, and $𝒮$, respectively.

To illustrate the notion of satisfaction in an interpretation, consider the following example.

We say that an interpretation $\Im$ satisfies a fact $M\mathrm{@}\varrho$, written $\Im \vDash M\mathrm{@}\varrho$, if $\Im ,t\vDash M$ for all $t\in \varrho$. Moreover, $\Im$ satisfies a ground rule $r$ if, whenever $\Im$ satisfies each body atom of $r$ at a time point $t$, then $\Im$ also satisfies the head of $r$ at $t$. Furthermore, $\Im$ satisfies a rule $r$ if it satisfies its every ground instance, that is, each rule in $\mathrm{𝗀𝗋𝗈𝗎𝗇𝖽}(\{r\})$. We say that $\Im$ is a model of a program $\mathrm{\Pi }$ if $\Im$ satisfies each rule in $\mathrm{\Pi }$. An interpretation $\Im$ is a model of a dataset $𝒟$ if $\Im$ satisfies each fact in $𝒟$. A dataset $𝒟$ entails a fact $M\mathrm{@}\varrho$ if each model of $𝒟$ is also a model of $M\mathrm{@}\varrho$. A program $\mathrm{\Pi }$ and a dataset $𝒟$ entail a fact $M\mathrm{@}\varrho$, written $(\mathrm{\Pi },𝒟)\vDash M\mathrm{@}\varrho$, if each model of both $\mathrm{\Pi }$ and $𝒟$ is also a model of $M\mathrm{@}\varrho$.

An interpretation $\Im$ contains an interpretation ${\Im }^{\prime }$, written ${\Im }^{\prime }\subseteq \Im$, if ${\Im }^{\prime },t\vDash P(𝐬)$ implies $\Im ,t\vDash P(𝐬)$, for each ground relational atom $P(𝐬)$ and each time point $t$. We say that $\Im$ is the least interpretation in a set $X$ of interpretations if $\Im \subseteq {\Im }^{\prime }$, for every ${\Im }^{\prime }\in X$. Each dataset $𝒟$ admits the least interpretation ${\Im }_{𝒟}$ among all models of $𝒟$; we say that a dataset $𝒟$ represents an interpretation $\Im$ if $\Im ={\Im }_{𝒟}$.

The immediate consequence operator $T_{\mathrm{\Pi }}$, for a program $\mathrm{\Pi }$, is a function mapping an interpretation $\Im$ to the least interpretation containing $\Im$ and satisfying the following property for each $r\in \mathrm{𝗀𝗋𝗈𝗎𝗇𝖽}(\mathrm{\Pi })$: whenever $\Im$ satisfies each body atom of $r$ at a time point $t$, then $T_{\mathrm{\Pi }}(\Im )$ satisfies the head of $r$ at $t$. The successive application of $T_{\mathrm{\Pi }}$ to ${\Im }_{𝒟}$ defines a transfinite sequence of interpretations $T_{\mathrm{\Pi }}^{\alpha }({\Im }_{𝒟})$, for ordinals $\alpha$, as follows:

The canonical interpretation ${ℭ}_{\mathrm{\Pi },𝒟}$ of $\mathrm{\Pi }$ and $𝒟$ is the interpretation $T_{\mathrm{\Pi }}^{{\omega }_1}({\Im }_{𝒟})$, where ${\omega }_1$ is the first uncountable ordinal. It is known that ${ℭ}_{\mathrm{\Pi },𝒟}$ is the least model of $\mathrm{\Pi }$ and $𝒟$ [11]. In other words, to compute the least model of $\mathrm{\Pi }$ and $𝒟$, we can apply $T_{\mathrm{\Pi }}$ until a fixpoint is reached, that is, no more information can be derived.

To illustrate the process of applying $T_{\mathrm{\Pi }}$, which is the basic reasoning mechanism in DatalogMTL, let us consider the following example.

The main reasoning problem in DatalogMTL we will consider is fact entailment: the problem of checking whether a program and a dataset entail a given relational fact. For instance, Example 4 shows that ${\mathrm{\Pi }}_{\mathrm{𝖾𝗑}}$ and ${𝒟}_{\mathrm{𝖾𝗑}}$ logically entail $\text{NegTest}(\mathrm{𝖡𝖾𝗇})\mathrm{@}[225⁤\frac{2}{3},317⁤\frac{2}{3}]$, because this fact holds in the canonical interpretations ${ℭ}_{{\mathrm{\Pi }}_{\mathrm{𝖾𝗑}},{𝒟}_{\mathrm{𝖾𝗑}}}$. Indeed, it was derived after two applications of the immediate consequence operator.

Another standard problem is consistency checking, which is to check whether a given program and a dataset admit a common model. Notice that our definition of a DatalogMTL rule does not allow for $\perp$ to occur in a head. As a result, in our setting every program $\mathrm{\Pi }$, together with any dataset $𝒟$ admit a common model, and the canonical interpretation ${ℭ}_{\mathrm{\Pi },𝒟}$ is the minimal among their models. However, if we allowed for $\perp$ in rule heads, which is often considered in the literature, some pairs of a program and dataset would not admit models. For instance this would be the case for a dataset with a single fact $P\mathrm{@}[0,1]$ and a program with a single rule $\perp \leftarrow P$, which clearly leads to inconsistency (derivation of $\perp$).

In the passing, we observe that if we allow for $\perp$ in rule heads, then consistency checking and fact entailment in DatalogMTL reduce to the complements of each other. Specifically, to check whether a program $\mathrm{\Pi }$ and a dataset $𝒟$ are inconsistent, it suffices to check whether they entail fact $P\mathrm{@}0$, for $P$ a fresh atom occurring neither in $\mathrm{\Pi }$ nor in $𝒟$. Indeed, $P\mathrm{@}0$ is entailed, that is $P\mathrm{@}0$ holds in all models of $\mathrm{\Pi }$ and $𝒟$ only if $\mathrm{\Pi }$ and $𝒟$ have no models, that is, if $\mathrm{\Pi }$ and $𝒟$ are not consistent. In turn, to check whether $\mathrm{\Pi }$ and $𝒟$ entail a fact $P(𝐜)\mathrm{@}\varrho$, it suffices to check whether the following program and dataset are inconsistent, with $P^{\prime }$ a fresh predicate of the same arity as $P$, $𝐱$ a tuple of distinct variables, and $t$ an arbitrary time point belonging to the interval $\varrho$:

Intervals ${\varrho }_1$ and ${\varrho }_2$ are constructed using $\varrho$ and $t$; for example, if $\varrho =[t_1,t_2)$, then ${\varrho }_1=[0,t-t_1]$ and ${\varrho }_2=[0,t_2-t)$, whereas if $t_2=\mathrm{\infty }$, then $t_2-t$ stands for $\mathrm{\infty }$. As an exercise, we invite the reader to verify the correctness of the reduction when $\varrho =[t_1,t_2)$, namely that $\mathrm{\Pi }$ and $𝒟$ entail $P(𝐜)\mathrm{@}\varrho$ if and only if ${\mathrm{\Pi }}^{\prime }$ and ${𝒟}^{\prime }$ are inconsistent.

It is also worth to mention known computational complexity results. Fact entailment in DatalogMTL is of high complexity; it is ExpSpace-complete [12] and PSpace-complete when measured with respect to the size of a dataset, that is, in data complexity [46]. Tractability in data complexity can be achieved by disallowing certain metric operators and restricting the form of rules [48].

In the remaining sections we will focus on algorithms for checking entailment. In particular, we will be interested in constructing the canonical interpretation ${ℭ}_{\mathrm{\Pi },𝒟}$ for a given program $\mathrm{\Pi }$ and dataset $𝒟$. Once this is done, entailment of any fact can be checked by simply verifying if ${ℭ}_{\mathrm{\Pi },𝒟}$ contains this fact or not. However, as we will show in the next section, construction of the canonical interpretation in DatalogMTL is a very non-trivial task.

Materialisation-based reasoning is the most common technique of choice implemented in scalable Datalog reasoners [13, 32, 19, 9]. Facts entailed by a program and a dataset are derived in successive rounds of rule applications, mimicking applications of the immediate consequence operator. The process continues until a fixpoint is reached and a full materialisation – representing the canonical interpretation – has been computed. At this point, entailment (or answer to more complicated queries) can be checked directly over the computed materialisation.

In this section, we formulate a (possibly non-terminating) generic reasoning procedure for DatalogMTL based on materialisation. In this process, rules are applied by first identifying maximal intervals in which all ground body atoms of a rule hold simultaneously, and then determining intervals in which the head atoms should be derived. Details of this process are presented in Algorithm 1, which performs a single round of rule applications for a given input program and dataset.

To familiarise the reader with this algorithm, let us consider the following example.

The result of applying Algorithm 1 to $\mathrm{\Pi }$ and $𝒟$ is always a dataset (i.e., a finite object), and the following proposition establishes that this dataset represents the interpretation obtained by a single application of the immediate consequence operator associated to $\mathrm{\Pi }$ to the dataset $𝒟$. Thus, Algorithm 1 provides a syntactic counterpart to the application of the immediate consequence operator.

To answer the questions from the end of the previous subsection, we will introduce the notion of finitely materialisable DatalogMTL programs. Intuitively, those are programs for which applications of the immediate consequence operator (or equivalently materialisation steps) allow us to obtain a fixpoint in a finite number of steps.

It follows from Proposition 7 that, for each program $\mathrm{\Pi }$ that is finitely materialisable for a dataset $𝒟$, there exists a dataset representing the canonical interpretation ${ℭ}_{\mathrm{\Pi },𝒟}$. The converse, however, does not hold: the canonical interpretation of a program $\mathrm{\Pi }$ and a dataset $𝒟$ may admit a finite representation, but $\mathrm{\Pi }$ may be not finitely materialisable for $𝒟$, as we show next.

The notion of finite materialisability in Definition 9 is data dependent, in that a given program could be finitely materialisable for a given dataset, but perhaps not for a different dataset. We next provide a data-independent notion of finite materialisability.

Which programs satisfy this stronger notion of finite materialisability? As we show next, any non-recursive DatalogMTL program is guaranteed to be finitely materialisable.

Intuitively non-recursive programs are programs whose rules do not contain derivation loops such as in the rules $Q\leftarrow P$ and $P\leftarrow Q$, where derivation of $P$ allows to derive $Q$, which allows to derive $P$ again, etc. Formally, (non)recursive programs are defined using the notion of the dependency graph of a program. The dependency graph of $\mathrm{\Pi }$ is a directed graph with a vertex $v_P$ for each predicate $P$ in $\mathrm{\Pi }$ and an edge $(v_Q,v_R)$ if there is a rule mentioning $Q$ in its body and $R$ in its head. For example the dependency graph of our ${\mathrm{\Pi }}_{\mathrm{𝖾𝗑}}$ is depicted below.

A program is said to be recursive, if its dependency graph is cyclic. Clearly the dependency graph above is cyclic, which implies that ${\mathrm{\Pi }}_{\mathrm{𝖾𝗑}}$ is a recursive program.

Next, we will show that each non-recursive program $\mathrm{\Pi }$ is finitely materialisable, by establishing a bound on the number of rounds of rule applications until the canonical interpretation is reached. In particular, we will show that this bound is given by the number $\mathrm{𝗉𝗋𝖾𝖽}(\mathrm{\Pi })$ of predicates occurring in $\mathrm{\Pi }$

The aim of this short subsection is to show an interesting result about the regular form of the canonical interpretation ${ℭ}_{\mathrm{\Pi },𝒟}$ [46]. The main concepts that we will use to describe this regularity are those of a $(\mathrm{\Pi },𝒟)$-ruler and the corresponding $(\mathrm{\Pi },𝒟)$-intervals.

Now, we say that an interpretation $\Im$ is a $(\mathrm{\Pi },𝒟)$-interpretation if, for every fact $M\mathrm{@}t$, it holds that $\Im \vDash M\mathrm{@}t$ implies $\Im \vDash M\mathrm{@}\varrho$, where $\varrho$ is the $(\mathrm{\Pi },𝒟)$-interval containing $t$. In other words, relational atoms hold uniformly over the $(\mathrm{\Pi },𝒟)$-intervals. The main result, we will need in the remaining parts of this section, is that the canonical interpretation and all partial materialisations are $(\mathrm{\Pi },𝒟)$-interpretations [46] as stated next.

The proof of this statement is not hard – it can be obtained by induction on $\alpha$, by showing that ${\Im }_{𝒟}$ is a $(\mathrm{\Pi },𝒟)$-interpretation, and each application of the immediate consequence operator leads to a $(\mathrm{\Pi },𝒟)$-interpretation. We invite the reader to write a full proof as an exercise.

In the next subsection we will use the above observation about the canonical intepretation structure to define saturated interpretations.

The main aim of this subsection is to present saturation conditions stating the properties that a partial materialisation $T_{\mathrm{\Pi }}^k({\Im }_{𝒟})$ needs to satisfy so that the it can be used to recover the full canonical interpretation. We call an interpretation satisfying these conditions saturated and show how to compute relevant periods and exploit them to unfold the interpretation into the canonical interpretation of $\mathrm{\Pi }$ and $𝒟$.

For convenience of presentation, we fix for the remainder of this subsection an arbitrary bounded program $\mathrm{\Pi }$, bounded dataset $𝒟$, and natural number $k$. To make the first observation we need to introduce additional notions. We let the depth of a rule $r$, written as $0ptr$, be the sum of the right endpoints in all intervals occurring in $r$ (or $0$ if $r$ mentions no intervals). For example, the depth of Rule (3) is $183+10=193$. The depth of a program $\mathrm{\Pi }$, written as $0pt\mathrm{\Pi }$, is the maximum depth of its rules; hence, bounded programs have finite depth. Moreover, for an interpretation $\Im$ and an interval $\varrho$, we let the projection ${\Im \mid }_{\varrho }$ of $\Im$ over $\varrho$ be the interpretation that coincides with $\Im$ on $\varrho$ and makes all relational atoms false outside $\varrho$.

As shown in the following proposition, the depth of a bounded rule determines the time points that can be “affected” by an application of this rule.