We report on our ongoing research on extending Datalog with existential rules and metric temporal operators. Such an extension would be of high practical importance; however, as we show, many commonly studied syntactic restrictions yielding decidable fragments of Datalog with existential rules (known as Datalog∃, Datalog± , or tuple-generating dependencies TGDs) are not applicable in the temporal setting. Indeed, most of these restrictions are either too weak to guarantee decidability or cannot be naturally extended to the our setting. In turn, we propose to combine syntactic restrictions with semantic modifications as a possible path towards decidable reasoning, and present first complexity results in this novel direction. Moreover, we discuss promising alternative properties under which eficient reasoning in the presence of existential quantification and temporal operators may be possible. Our main aim is to extend DatalogMTL [1]-a temporal Datalog with operators from metric temporal logic MTL [2] interpreted over the rational time line-with existential rules while, at the same time, preserving decidability of reasoning. DatalogMTL is a highly expressive language with a number applications, for example, in stream reasoning [3] and temporal ontology-based query answering [4, 5]. By allowing for MTL operators in Datalog atoms, it allows us to write atoms such as x1,4(, ), which states that the atom (, ) did hold at some past time point which is at least 1 and at most 4 seconds ago, whereas ⊟1,4(, ) states that (, ) did hold continuously during the above mentioned interval of time. We propose an extension, DatalogMTL∃, of DatalogMTL with existential rules, which allows us to use existential quantifiers in rule heads. For example, it allows us for writing a rule Datalog 2.0 2022: 4th International Workshop on the Resurgence of Datalog in Academia and Industry, September 05, 2022, Genova - Nervi, Italy $ matthias.lanzinger@cs.ox.ac.uk (M. Lanzinger); przemyslaw.walega@cs.ox.ac.uk (P. A. Wałęga) 0000-0002-7601-3727 (M. Lanzinger); 0000-0003-2922-0472 (P. A. Wałęga) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CPWrEooUrckResehdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g CEUR Workshop Proceedings (CEUR-WS.org)
∃ ⊟[
Nobel10thAniv (), which states that if celebrates the 10th anniversary of receiving the Nobel prize, there needs to exist a category in which, 10 years ago, received the Nobel prize. The access to both MTL operators and existential rules, provides a powerful extension of Datalog. The main obstacle, as we show next, is that combining temporal operators and existential rules quickly leads to bad computational behaviour. Consequently, it raises a question how to construct decidable (and preferably low-complexity) variants of DatalogMTL∃.
In this section, we give a summary of our ongoing research on the complexity of reasoning in DatalogMTL∃ and in its modifications. We also discuss some conceptual challenges which disallow for using standard reasoning techniques in existential rules.
Our so-far obtained results are summarised in Table 1, where we consider DatalogMTL∃ under the natural and uniform semantics, separately, as well as standard syntactical restrictions, constituted by guarded and weakly acyclic programs. By the natural semantics we mean that whenever an existential rule ‘fires’ it can invent arbitrary new constants. Hence, the same ground existential rule can invent diferent constants when fired in diferent time points; this can lead to undesired meaning of existential rules and also to bad computational behaviour— since we consider an infinite, and moreover dense, rational time line. In contrast, by the uniform semantics, we mean that a ground existential rule invents the same constants in all time points it fires; in this sense applications of existential rules are ‘uniform’. Moreover, together with standard open-world assumption (OWA), which allows for new values invention by existential rules, we consider also closed-world assumption (CWA) which cannot invent new constants. Note that existential quantification under CWA can be seen as a disjunction over all explicitly mentioned constants in the program, so it is less interesting from the conceptual point of view, but in practice can be useful for the concise representation of huge disjunctions.
Full DatalogMTL∃
Guarded programs
Weakly acyclic programs Natural se- OWA mantics CWA Uniform semantics
OWA CWA undecidable undecidable undecidable
undecidable undecidable
ExpSpace-co.
Regarding the results in Table 1, we observe that under the natural semantics, undecidability of the full DatalogMTL∃ follows immediately from the well-known undecidability of Datalog∃. However, we additionally show that the guarded and weakly acyclic fragments of DatalogMTL are already undecidable, which is in contrast to Datalog∃. Notably, even the CWA case is undecidable under natural semantics (even for programs that are simultaneously guarded and weakly-acyclic), highlighting the dificulty of reasoning in DatalogMTL∃. Thus, DatalogMTL∃ under natural semantics is undecidable in all case we considered.
Regarding the uniform semantics, we shown that reasoning in DatalogMTL∃ becomes
significantly easier. It is still undecidable already for guarded programs, which is again in a significant
contrast to Datalog∃. However, in the case of weakly acyclic DatalogMTL∃ programs, both fact
entailment and consistency checking are decidable, and in particular, 2-ExpSpace-complete
(cf., 2-ExpTime-completeness of weakly acyclic Datalog∃ [
It is worth emphasising that we use guardedness and weak acyclicity in DatalogMTL∃ in the same way as they are used in Datalog∃, so we do not provide any additional conditions for temporal operators. While it may seem naïve to ignore the temporal dimension, our reductions demonstrate essential obstacles in providing time-sensitive versions of these properties. Indeed, our undecidability argument for the guarded fragment shows that we can construct a program simulating computations of a Turing machine, such that the program uses only a single existential rule without temporal operators and the only temporal operator used in the program is ⊟1, for example, in rules of the form ∃Next (, ) ←
Next (, ) Next (, ) ← ⊟1Next (, ).
Hence, extending the guardedness notion to temporal operators in a way that prohibits our
reduction would have to restrict the language to the point where even the most basic temporal
reasoning is excluded. Notably, our reduction implies also undecidability of existential extensions
of much simpler temporal formalisms such as Temporal Datalog [
Similarly, it may seem natural to extend the definition of weak acyclicity by treating each
predicate as if it had an additional implicit time attribute, and thus also a corresponding vertex
for the time dimension in the dependency graph (cf., [
Among other important fragments for which Datalog∃ is decidable but which are not mentioned
in our analysis so far, are the linear, shy [
In particular, the shy fragment identifies (a subset) of programs that are parsimonious, which
are programs for which inference using the parsimonious chase [
The natural immediate questions that are still open concern the decidability of DatalogMTL∃
for the linear and sticky fragments. However, again techniques from Datalog∃ are dificult to
adapt to the temporal setting and reasoning is significantly more complex even in the linear case.
Indeed, fact entailment in linear DatalogMTL is already PSpace-complete in data complexity,
i.e., the same complexity as in full DatalogMTL [
Sticky Datalog∃ enjoys very good computational properties [
Note that many other fragments of Datalog∃ that have been studied in the literature, such
as the weakly-guarded or frontier-guarded fragments (cf., [
The discussion in the previous sections has highlighted that many of the key properties that
have been identified for decidable Datalog∃ fragments are no longer helpful in DatalogMTL∃.
This motivates the study of new restrictions which lead to decidable reasoning in the presence
of temporal operators and existential quantifiers. Our results suggest that purely syntactical
restrictions are too limited in the presence of temporal operators. In future work we will study
the combination of syntactic fragments that control existential quantification, together with
properties that are known to control expansion in the time dimension in DatalogMTL, such as
MTL-acyclicity [
Finally, since existential rules with MTL operators have proven to be useful in various industry
applications, such as, technical specifications, verification of banking agreements [
Our work has been supported by the EPSRC projects OASIS (EP/S032347/1), AnaLOG (EP/P025943/1), and UK FIRES (EP/S019111/1), the SIRIUS Centre for Scalable Data Access, and Samsung Research UK. Matthias Lanzinger acknowledges support by the Royal Society “RAISON DATA” project (Reference No. RP\R1\201074).