The Temporal Vadalog System

DatalogMTL is Datalog extended with operators from the metric temporal logic. We provide a summary of DatalogMTL with stratified negation under continuous semantics. DatalogMTL is defined over the rational timeline, i.e., an ordered set of rational numbers $\mathbb{Q}$. An interval $\varrho =⟨{\varrho }^{-},{\varrho }^{+}⟩$ is a non-empty subset of $\mathbb{Q}$ such that for each $t\in \mathbb{Q}$ where , $t\in \varrho$, and the endpoints ${\varrho }^{-},{\varrho }^{+}\in \mathbb{Q}\cup \{-\mathrm{\infty },\mathrm{\infty }\}$. The brackets denote whether the interval is closed (“$[]$”), half-open (“$[)$”,“$(]$”) or open (“$()$”), whereas angle brackets (“$⟨⟩$”) are used when unspecified. An interval is punctual if it is of the form $[t,t]$, positive if ${\varrho }^{-}\ge 0$, and bounded if ${\varrho }^{-},{\varrho }^{+}\in \mathbb{Q}$.

DatalogMTL extends the syntax of Datalog with negation with temporal operators [15]. For the following definitions, we consider a function-free first-order signature. An atom is of the form $P(𝝉)$, where $P$ is a $n$-ary predicate and $𝝉$ is a $n$-ary tuple of terms, where a term is either a constant or a variable. An atom is ground if it contains no variables. A fact is an expression $P(𝝉)\mathrm{@}\varrho$, where $\varrho$ is an interval and $P(𝝉)$ a ground atom and a database is a set of facts. A literal is an expression given by the following grammar, where $\varrho$ is a positive interval: $A::=\top \mid \perp \mid P(𝝉)\mid {\boxminus }_{\varrho }A\mid {⊞}_{\varrho }A\mid {\text{<object type="image/svg+xml" data="dagpub-standalone-manual-dagpub-svg-2026-01-09-17-57-57.pdf2svg.svg" id="A1.p2.m10.g1nest" class="ltx\_graphics ltx\_img\_square" width="7" height="7" style="width: 14px; height: unset; max-width: 100\%"></object>}}_{\varrho }A\mid {\text{<object type="image/svg+xml" data="dagpub-standalone-manual-dagpub-svg-2026-01-09-17-57-55.pdf2svg.svg" id="A1.p2.m10.g2nest" class="ltx\_graphics ltx\_img\_square" width="7" height="7" style="width: 14px; height: unset; max-width: 100\%"></object>}}_{\varrho }A\mid A{𝒮}_{\varrho }A\mid A{𝒰}_{\varrho }A$. A rule is an expression given by the following grammar, where $i,j\ge 0$, each $A_k$ ($k\ge 0$) is a literal and $B$ is an atom: $A_1\wedge \mathrm{\cdots }\wedge A_i\wedge \mathrm{not}{A}_{i+1}\wedge \mathrm{\cdots }\wedge \mathrm{not}{A}_{i+j}\to B$. The conjunction of literals $A_k$ is the rule body, where $A_1\wedge \mathrm{\cdots }\wedge A_i$ denote positive literals and $A_{i+1}\wedge \mathrm{\cdots }\wedge A_{i+j}$ denote negated (i.e., prefixed with not) literals. The atom $B$ is the rule head. A rule is safe if each variable occurs in at least one positive body literal, positive if it has no negated body literals (i.e., $j=0$), and ground if it contains no variables. A program $\mathrm{\Pi }$ is a set of safe rules and is stratifiable if there exists a stratification of a program $\mathrm{\Pi }$. A stratification of $\mathrm{\Pi }$ is defined as a function $\sigma$ that maps each predicate $P$ in $\mathrm{\Pi }$ to a positive integer (stratum) s.t. for each rule, where $P^h$ denotes a predicate of the head, and $P^{+}$ (resp. $P^{-}$) a positive (negative) body predicate, $\sigma (P^h)\ge \sigma (P^{+})$ and $\sigma (P^h)>\sigma (P^{-})$. The semantics of DatalogMTL is given by an interpretation $𝔐$ that specifies for each time point $t\in \mathbb{Q}$ and each ground atom $P(𝝉)$, whether $P(𝝉)$ is satisfied at $t$, in which case we write $𝔐,t\vDash P(𝝉)$. This satisfiability notion extends to ground literals as follows:

An interpretation $𝔐$ satisfies $\mathrm{not}A$ ($𝔐,t\vDash \mathrm{not}A$), if $𝔐,t\vDash ̸A$, a fact $P(𝝉)\mathrm{@}\varrho$, if $𝔐,t\vDash P(𝝉)$ for all $t\in \varrho$, and a set of facts $𝒟$ if it is a model of each fact in $𝒟$. Furthermore, $𝔐$ satisfies a ground rule $r$ if $𝔐,t\vDash A_k$ for $0\le k\le i$ and $𝔐,t\vDash \mathrm{not}{A}_k$ for $i+1\le k\le i+j$ for every $t$; for every $t$, if the literals in the body are satisfied, so is the head $𝔐,t\vDash B$; $𝔐$ satisfies a rule when it satisfies every possible grounding of the rule. Moreover, $𝔐$ is a model of a program if it satisfies every rule in the program and the program has a stratification, i.e., it is stratifiable. Given a stratifiable program $\mathrm{\Pi }$ and a set of facts $𝒟$, we call ${ℭ}_{\mathrm{\Pi },𝒟}$ the canonical model of $\mathrm{\Pi }$ and $𝒟$ [8], and define it as the minimum model of $\mathrm{\Pi }$ and $𝒟$, i.e., ${ℭ}_{\mathrm{\Pi },𝒟}$ is the minimum model for all the facts of $𝒟$ and the rules of $\mathrm{\Pi }$. In this context, “minimum” means that the set of positive literals in $𝔐$ is minimized or, equivalently, that the positive literals of this model are contained in every other model. Since $\mathrm{\Pi }$ is stratifiable, this minimum model exists and is unique [12]. According to Tena Cucala’s notation [15], we say that a stratifiable program $\mathrm{\Pi }$ and a set of facts $𝒟$ entail a fact $P(𝝉)\mathrm{@}\varrho$, written as $(\mathrm{\Pi },𝒟)\vDash P(𝝉)\mathrm{@}\varrho$, if ${ℭ}_{\mathrm{\Pi },𝒟}\vDash P(𝝉)\mathrm{@}\varrho$. In the remainder of the paper, we will assume the stratification of programs (or set of rules) as implicit.

In this context, the query answering or reasoning task is defined as follows: given the pair $Q=(\mathrm{\Pi },\mathrm{𝐴𝑛𝑠})$, where $\mathrm{\Pi }$ is a set of rules, $\mathrm{𝐴𝑛𝑠}$ is an $n$-ary predicate, and the query $Q$ is evaluated over $𝒟$, then $Q(𝒟)$ is defined as $Q(𝒟)=\{(\overline{t},\varrho )\in \mathrm{𝑑𝑜𝑚}{(𝒟)}^n\times \mathrm{𝑡𝑖𝑚𝑒}(𝒟)\mid (\mathrm{\Pi },𝒟)\vDash \mathrm{𝐴𝑛𝑠}(\overline{t})\mathrm{@}\varrho \}$, where $\overline{t}$ is a tuple of terms, the domain of $𝒟$, denoted $\mathrm{𝑑𝑜𝑚}(𝒟)$, is the set of all constants that appear in the facts of $𝒟$, and the set of all the time intervals in $𝒟$ is denoted as $\mathrm{𝑡𝑖𝑚𝑒}(𝒟)$. As we shall see in practical cases, the $\mathrm{𝐴𝑛𝑠}$ predicate of $\mathrm{\Pi }$ will be sometimes called “query predicate” and provided to the reasoning system with specific conventions, which we omit for space reasons, but will render in textual explanations.