# goaldriven_reasoning_in_datalogmtl_with_magic_sets__fa0649d1.pdf

Goal-Driven Reasoning in Datalog MTL with Magic Sets

Shaoyu Wang1*, Kaiyue Zhao1*, Dongliang Wei1*, Przemysław Andrzej Wałe ga2,3, Dingmin Wang2, Hongming Cai1, Pan Hu1

1School of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, China 2Department of Computer Science, University of Oxford, UK 3School of Electronic Engineering and Computer Science, Queen Mary University of London, UK {royalrasins, Horizon52183, weidongliang9, hmcai, pan.hu}@sjtu.edu.cn, {przemyslaw.walega, dingmin.wang}@cs.ox.ac.uk

Datalog MTL is a powerful rule-based language for temporal reasoning. Due to its high expressive power and flexible modeling capabilities, it is suitable for a wide range of applications, including tasks from industrial and financial sectors. However, due its high computational complexity, practical reasoning in Datalog MTL is highly challenging. To address this difficulty, we introduce a new reasoning method for Datalog MTL which exploits the magic sets technique a rewriting approach developed for (non-temporal) Datalog to simulate top-down evaluation with bottom-up reasoning. We have implemented this approach and evaluated it on publicly available benchmarks, showing that the proposed approach significantly and consistently outperformed state-of-the-art reasoning techniques.

Introduction Datalog MTL (Brandt et al. 2018) extends the well-known declarative logic programming language Datalog (Ceri, Gottlob, and Tanca 1989) with operators from metric temporal logic (MTL) (Koymans 1990), allowing for complex temporal reasoning. It has a number of applications, including ontology-based query answering (Brandt et al. 2018; G uzel Kalayci et al. 2018), stream reasoning (Wałe ga et al. 2023a; Wałe ga, Kaminski, and Cuenca Grau 2019), and reasoning for the financial sector (Colombo et al. 2023; Nissl and Sallinger 2022; Mori et al. 2022), among others. To illustrate capabilities of Datalog MTL, consider a scenario in which we want to reason about social media interactions. The following Datalog MTL rule describes participation of users in the circulation of a viral social media post:

[0,2]P(x) Ð I(x,y) P(y), (1)

namely, it states that if at a time point t a user x interacted with a user y over the post (expressed as I(x,y)), and y participated in the post s circulation (expressed as P(y)), then in the time interval [t,t+2], user x will be continuously participating in the post s circulation ( [0,2]P(x)). One of the main reasoning tasks considered in Datalog MTL is fact entailment, which involves checking whether

*These authors contributed equally. Corresponding author Copyright 2025, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

a program-dataset pair (Π,D) logically entails a given temporal fact. This task was shown to be EXPSPACEcomplete in combined complexity (Brandt et al. 2018) and PSPACE-complete in data complexity (Wałe ga et al. 2019). To decrease computational complexity, various syntactical (Wałe ga et al. 2020b) and semantic (Wałe ga et al. 2020a) modifications of Datalog MTL have been introduced. Datalog MTL was also extended with stratified negation (Tena Cucala et al. 2021), non-stratified negation (Wałe ga et al. 2021, 2024), and with temporal aggregation (Bellomarini, Nissl, and Sallinger 2021). A sound and complete reasoning approach for Datalog MTL can be obtained using an automata-based construction (Wałe ga et al. 2019). Another approach for reasoning is to apply materialisation, that is, successively apply to the initial dataset D rules in a given program Π, to derive all the facts entailed by a program-dataset pair (Π,D). It is implemented, for example, within Vadalog reasoner (Bellomarini et al. 2022). Materialisation, however, does not guarantee termination since Datalog MTL programs can express (infinite) recursion over time. To marry completeness and efficiency of reasoning, a combination of automataand materialisation-based approaches was introduced in the Me Teo R system (Wang et al. 2022). Materialisation-based approach typically outperforms the automata-based approach, so cases in which materialisation-based reasoning is sufficient were studied (Wałe ga, Zawidzki, and Cuenca Grau 2021, 2023). More recently, a very efficient reasoning approach was introduced, which combines materialisation with detection of repeating periods (Wałe ga et al. 2023b). Despite recent advancement in the area, the currently available reasoning methods for Datalog MTL (Wang et al. 2022; Wałe ga et al. 2023b; Bellomarini et al. 2022) can suffer from deriving huge amounts of temporal facts which are irrelevant for a particular query. This, in turn, can make the set of derived facts too large to store in memory or even in a secondary storage. For example, if the input dataset mentions millions of users, together with interactions between them and their participation in posts circulation, application of Rule (1) may result in a huge set of derived facts. However, if we only want to check whether the user Arthur participated on post s circulation on September 10th, 2023, most of the derived facts are irrelevant. Note that determining which exactly facts are relevant is not easy, especially

The Thirty-Ninth AAAI Conference on Artificial Intelligence (AAAI-25)

when a Datalog MTL program contains a number of rules with complex interdependencies. To address these challenges, we take inspiration from the magic set rewriting technique, which was developed for nontemporal Datalog (Abiteboul, Hull, and Vianu 1995; Ullman 1989b; Faber, Greco, and Leone 2007; Ullman 1989a). We extend it to the temporal setting of Datalog MTL, thereby proposing a new variant of magic set rewriting. For example, consider again Rule (1) and assume that we want to check if Arthur participated in a post s circulation on 10/9/2023. Observe that if there is no chain of interactions between Arthur and another user Beatrice in the input dataset, then facts about Beatrice are irrelevant for our query, and so, we do not need to derive them. We will achieve it by rewriting the original program-dataset pair into a new pair (using additional magic predicates) such that the new pair provides the same answers to the query as the original pair, but allows us for a more efficient reasoning. As a result we obtain a goal-driven (i.e. query-driven) reasoning approach. To the best of our knowledge, our work is the first that allows to prune irrelevant derivations in Datalog MTL reasoning. To implement the magic sets technique in the Datalog MTL setting, two main challenges need to be addressed. First, it is unclear how MTL operators affect sideways information passing in magic sets. We address this challenge by carefully examining each type of MTL operators and designing corresponding transformations. Second, for the transformed program-dataset pair established optimisations for reasoning in Datalog MTL may no longer apply or become less efficient. This is indeed the case, and so, we show how these optimisations can be adapted to our new setting. We implemented our approach and tested it using the state-ofthe-art Datalog MTL solver Me Teo R. Experiments show that compared with existing methods, our approach achieves a significant performance improvement.

Preliminaries We briefly summarise the core concepts of Datalog MTL and provide a recapitulation of magic set rewriting in the nontemporal setting.

Syntax of Datalog MTL. Throughout this paper, we assume that time is continuous, in particular, that the timeline is composed of rational numbers. A time interval is a set of continuous time points ϱ of the form t1,t2 , where t1,t2 Q { , }, whereas is [ or ( and likewise is ] or ). An interval is punctual if it is of the form [t,t], for some t Q; we will often represent it as t. An interval is bounded if both of its endpoints are rational numbers (i.e. neither or ). Although time points are rational numbers, we will sometimes use dates instead. For example, 10/9/2023 (formally it can be treated as the number of days that passed since 01/01/0000). When it is clear from the context, we may abuse distinction between intervals (i.e. sets of time points) and their representation t1,t2 . Objects are represented by terms: a term is either a variable or a constant. A relational atom is an expression R(t), where R is a predicate and t is a tuple of terms of arity matching R. Metric atoms extend relational atoms by allow-

ing for operators from metric temporal logic (MTL), namely, ϱ, ϱ, |ϱ, xϱ, Uϱ, and Sϱ, with arbitrary intervals ϱ. Formally, metric atoms, M, are generated by the grammar

M = R(t) ϱM ϱM |ϱM xϱM MUϱM MSϱM,

where and are constants for, respectively, truth and falsehood, whereas ϱ are any intervals containing only nonnegative rationals. A Datalog MTL rule, r, is of the form

M M1 M2 Mn, for n 1,

where each Mi is a metric atom and M is a metric atom not mentioning , |, x, U, and S. Note that similarly as Wałe ga et al. (2023b), we do not allow for in M to ensures consistency and to focus on derivation of facts. We call M the head of r and the set {Mi i {1,...,n}} the body of r, and represent them as head(r) and body(r), respectively. For an example of a Datalog MTL rule see Rule (1). We call a predicate intensional (or idb) in Π if it appears in the head of some rule in Π, and we call it extensional (or edb) in Π otherwise. Rule r is safe if each variable in r s head appears also in r s body. A Datalog MTL program, Π, is a finite set of safe rules. An expression (e.g. a relational atom, a rule, or a program) is ground if it does not mention any variables. A fact is of the form R(t)@ϱ, where R(t) is a ground relational atom and ϱ is an interval. A query is of a similar form as a fact, but its relational atom R(t) does not need to be ground. A dataset, D, is a finite set of facts. A dataset or program is bounded, if all the intervals they mention are bounded.

Semantics of Datalog MTL. A Datalog MTL interpretation I is a function which maps each time point t Q to a set of ground relational atoms (namely to atoms which hold at t). If R(t) belongs to this set, we write I,t R(t). This extends to metric atoms as presented in Table 1. Interpretation I satisfies a fact R(t)@ϱ, if I,t R(t) for each t ϱ, and I satisfies a set B of ground metric atoms, in symbols I,t B, if I,t M for each M B. Interpretation I satisfies a ground rule r if I,t body(r) implies I,t head(r) for each t Q. A ground instance of r is any ground rule r such that there is a substitution σ mapping variables into constants so that r = σ(r) (for any expression e, we will use σ(e) to represent the expression obtained by applying σ to all variables in e). Interpretation I satisfies

I,t for every t Q I,t for no t Q I,t ϱM iff I,t1 M for all t1 s.t. t1 t ϱ I,t ϱM iff I,t1 M for all t1 s.t. t t1 ϱ I,t |ϱM iff I,t1 M for some t1 s.t. t1 t ϱ I,t xϱM iff I,t1 M for some t1 s.t. t t1 ϱ I,t M2UϱM1 iff I,t1 M1 for some t1 s.t. t1 t ϱ,

and I,t2 M2 for all t2 (t,t1) I,t M2SϱM1 iff I,t1 M1 for some t1 s.t. t t1 ϱ,

and I,t2 M2 for all t2 (t1,t)

Table 1: Semantics for ground metric atoms

a rule r, if it satisfies all ground instances of r, and it is a model of a program Π, if it satisfies all rules of Π. If I satisfies every fact in a dataset D, then I is a model of D. I is a model of a pair (Π,D) if I is both a model of Π and a model of D. A pair (Π,D) entails a fact R(t)@ϱ, in symbols (Π,D) R(t)@ϱ, if all models of (Π,D) satisfy R(t)@ϱ. Given (Π,D), an answer to a query q is any fact R(t)@ϱ such that (Π,D) entails R(t)@ϱ and R(t)@ϱ = σ(q), for some substitution σ. An interpretation I contains interpretation I if I satisfies every fact that I does and I = I if they contain each other. Each dataset D has a unique least interpretation ID, which is the minimal (with respect to containment) model of D. Given a program Π, we define the immediate consequence operator TΠ as a function mapping an interpretation I into the least interpretation containing I and satisfying for each time point t and each ground instance r (which does not mention in the head) of a rule in Π the following: I,t body(r) implies TΠ(I),t head(r). Now we are ready to define the canonical interpretation for a programdataset pair (Π,D). Repeated application of TΠ to ID yields a transfinite sequence of interpretations I0,I1,... such that (i) I0 = ID, (ii) Iα+1 = TΠ(Iα) for α a successor ordinal, and (iii) Iβ = α<β Iα for β a limit ordinal and successor ordinals α (here union of two interpretations is the least interpretations satisfying all facts satisfied in these interpretations); then, Iω1, where ω1 is the first uncountable ordinal, is the canonical interpretation of (Π,D), denoted as CΠ,D (Brandt et al. 2018).

Reasoning Task. We focus on fact entailment, the main reasoning task in Datalog MTL, which involves checking whether a given pair of Datalog MTL program and dataset (Π,D) entails a fact R(t)@ϱ. This task is EXPSPACEcomplete (Brandt et al. 2018) in combined complexity and PSPACE-complete in data complexity (Wałe ga et al. 2019).

Magic Set Rewriting. We now recapitulate magic set rewriting for Datalog. For a detailed description of magic sets we refer ar reader to the work of Abiteboul, Hull, and Vianu (1995); Ullman (1989b); Faber, Greco, and Leone (2007); Ullman (1989a). Datalog can be seen as a fragment of Datalog MTL that disallows metric temporal operators and discards the notion of time. In the context of Datalog, given a query (which is now a relational atom) q and a program-dataset pair (Π,D), the magic set approach constructs a pair (Π ,D ) such that (Π ,D ) and (Π,D) provide the same answers to q. The first step of magic set rewriting involves program adornment (adding superscripts to predicates). Adornments will guide construction of Π . The adorned program Πa is constructed as follows:

Step 1: assume that the query is of the form q = Q(t). We adorn Q with a string γ of letters b and f, which stand for bound and free terms. The length of γ is the arity of Q; the ith element of γ is b if the ith term in t is a constant, and f otherwise. For example Q(x,y, Arthur) yields Qffb. We set A = {Qγ} and Πa = . Step 2: we remove one adorned predicate Rγ from A (in

the first application of Step 2, set A contains only one element, but on later stages A will be modified). For each rule r whose head predicate is R, we generate an adorned rule ra and add it to Πa. The rule ra is constructed from r as follows. We start by replacing the head predicate R in r with Rγ. Next we label all occurrences of terms in r as bound or free as follows: (i) terms in head(r) are labelled according to γ (i.e. the ith term is bound iff the ith element of γ is b), (ii) each constant in body(r) is labelled as bound, (iii) each variable that is labelled as bound in head(r) is labelled as bound in body(r), (iv) if a variable occurs in a body atom, all its occurrences in the subsequent atoms (i.e. located to the right of this body atom) are labelled as bound, (v) all remaining variables in body(r) are labelled as free.

Then each body atom P(t ) in r is replaced with P γ (t ) such that the ith letter of γ is b if the ith term of t is labelled as bound, and it is f otherwise. Moreover, if P is idb in Π and P γ was never constructed so far, we add P γ to A. For example if Rγ is Qffb and r is Q(x,Arthur,y) Ð P(x,Beatrice) R(x,y), then ra is Qffb(x,Arthur,y) Ð P fb(x,Beatrice) Rbb(x,y). Then, we keep repeating Step 2 until A becomes empty. Next, we generate the final Π from the above constructed Πa. For a tuple of terms t and an adornment γ of the same length, we let bt(t,γ) and bv(t,γ) be, respectively, the sequences of terms and variables in t, which are bound according to γ (so bv(t,γ) is always a subsequence of bt(t,γ)). For example, bt((x,y, Arthur),bfb) = (x,Arthur) and bv((x,y, Arthur),bfb) = (x). Then, for each rule ra Πa, represented as

Rγ(t) Ð Rγ1 1 (t1) Rγn n (tn),

we add to Π the rule

R(t) m Rγ(t ) R1(t1) Rn(tn) (2)

and the following rules, for all i {1,...,n} such that Ri is an idb predicate in Π:

m Rγi i (t i) m Rγ(t ) R1(t1) Ri 1(ti 1), (3)

where t = bv(t,γ), t i = bv(ti,γi), and m Rγ and m Rγi i are newly introduced magic predicates with arities t and t i , respectively. Intuitively, magic predicates are responsible for storing tuples relevant for the derivations of query answers. In particular, Rule (2) considers only derivations that are (i) considered by the original rule r and (ii) allowed by the magic predicate m Rγ. Rule (3) is responsible for deriving facts about magic predicates. Finally, assuming that the input query is of the form q = Q(t), we construct D by adding m Qγ(bt(t,γ)) to D, where γ is the adornment from Step 1. The new pair (Π ,D ) provides the same answers to query q as (Π,D), but allows us to provide answers to q faster than (Π,D). As an example of application of magic set rewriting, consider a Datalog dataset D, a Datalog version of Rule (1):

P(x) Ð I(x,y) P(y), (4)

and a query P(Arthur). After applying Step 1 we get A = {P b} and Πa = . Then, in Step 2, we remove P b from A, and adorn Rule (4) according to conditions (i) (v). As a result, we obtain the following rule:

P b(x) Ð Ibf(x,y) P b(y)

as a single rule in Πa. No predicate is added to A, so A = , and so we do not apply Step 2 any more. Next, we generate the following program Π from Πa:

P(x) Ð m P b(x) I(x,y) P(y),

m P b(y) Ð m P b(x) I(x,y).

Finally, we set D = D {m P b(Arthur)}, which concludes the construction of (Π ,D ). The newly constructed (Π ,D ) and the initial (Π,D) have the same answers to the query P(Arthur). However, (Π ,D ) entails a smaller amount of facts about P. Indeed, if in the dataset D there is no chain of interactions I connecting a constant Beatrice with Arthur, then neither P(Beatrice) nor m P b(Beatrice) will be entailed by (Π ,D ).

Magic Sets for Datalog MTL In this section we explain how do we extend magic set rewriting to the Datalog MTL setting. Since the approach is relatively complex, we start by providing an example how, given a particular query q and a Datalog MTL programdataset pair (Π,D), we construct (Π ,D ). For simplicity, in the example we will use a ground query q (i.e. a fact), but it is worth emphasising that our approach supports also non-ground queries.

Example. Consider a query q = P(Arthur)@10/9, a Datalog MTL dataset D, and a program consisting of the rules

[0,2]P(x) I(x,y) P(y), (r1)

[0,1]P(x) I(x,y) x[0,1]P(y). (r2)

We construct D by adding m P b(Arthur)@10/9 to D. Hence, the construction of D is similar as in the case of (non-temporal) Datalog, but now the fact with magic predicate mentions also the time point from the input query. This will allow us not only to determine which atoms, but also which time points are relevant for answering the query. Next, we construct an adorned program Πa as below:

[0,2]P b(x) Ibf(x,y) P b(y), (ra1)

[0,1]P b(x) Ibf(x,y) x[0,1]P b(y). (ra2)

The construction of Πa is analogous to that in Datalog (see the previous section), but Πa now contains temporal operators. As in the case of Datalog, we will obtain Π by constructing two types of rules, per a rule in Πa. However, the construction of these rules will require further modifications. Rules of the first type are extensions of rules in Πa obtained by adding atoms with magic predicates to rule bodies. We can observe, however, that the straightforward adaptation of Rule (2) used in Datalog is not appropriate in the temporal setting. To observe an issue, let us consider

Rule (ra1). The na ıve adaptation of Rule (2) would construct from Rule (ra1) the following rule:

[0,2]P(x) m P b(x) I(x,y) P(y).

Recall that our goal is to construct (Π ,D ) which will have exactly the same answers to the input query as the original (Π,D). The rule above, however, would not allow us to achieve it. Indeed, if D consists of facts I(Arthur,Beatrice)@8/9 and P(Beatrice)@8/9, then the original Rule (r1) allows us to derive P(Arthur)@[8/9,10/9], and so, the query fact P(Arthur)@10/9 is derived. However, the rule constructed above does not allow us to derive any new fact from D , because we do not have m P b(Arthur)@8/9 in D , which is required to satisfy the rule body. Our solution is to use |[0,2]m P b(x) instead of m P b(x) in the rule body, namely we construct the rule

[0,2]P(x) |[0,2]m Pb(x) I(x,y) P(y). This allows us to obtain missing derivations; in particular, in our example above, this new rule allows us to derive P(Arthur)@[8/9,10/9], and so, P(Arthur)@10/9, as required. Similarly, for Rule (ra2) we construct

[0,1]P(x) |[0,1]m P b(x) I(x,y) x[0,1]P(y). Next we construct rules of the second type, by adapting the idea from Rule (3). For Rule (ra1) we use the form of Rule (3), but we additionally precede the magic predicate in the body with the diamond operator, to prevent the observed issue with missing derivations. Hence, we obtain

m Pb(y) |[0,2]m P b(x) I(x,y).

The case of Rule (ra2), however, is more challenging as this rule mentions a temporal operator in the body. Because of that, we observe that the below rule would not be appropriate

m P b(y) |[0,1]m P b(x) I(x,y). To observe the issue, let us consider a program Π, which instead of Rule (r1) has Rule (r3) which is of the form P(x) S(x). Therefore, Rule (ra3) is P b(x) Sb(x) and its first-type-rule is P(x) m P b(x) S(x). Assume moreover, that D consists of S(Beatrice)@8/9 and I(Arthur,Beatrice)@9/9. Hence, Rule (r3) allows us to derive P(Beatrice)@8/9, and then Rule (r2) derives P(Arthur)@[9/9,10/9]. Although with the rule generated above from Rule (ra2), we can derive from D the fact m P b(Beatrice)@9/9, we cannot derive m P b(Beatrice)@8/9. This, in turn, disallows us to derive P(Arthur)@10/9. In order to overcome this problem, it turns out that it suffices to add a temporal operator in the head of the rule. In our case, we construct the following rule:

[0,1]m P b(y) |[0,1]m P b(x) I(x,y).

Hence, the finally constructed Π consists of the rules

[0,2]P(x) |[0,2]m Pb(x) I(x,y) P(y),

[0,1]P(x) |[0,1]m P b(x) I(x,y) x[0,1]P(y),

m Pb(y) |[0,2]m P b(x) I(x,y),

[0,1]m P b(y) |[0,1]m P b(x) I(x,y).

In what follows we will provide details of this construction and show that (Π ,D ) and (Π,D) have the same answers to the input query.

Algorithm Overview. Our approach to constructing (Π ,D ) is provided in Algorithm 1. The algorithm takes as input a Datalog MTL program Π, dataset D, and query q = Q(t)@ϱ, and it returns the rewritten pair (Π ,D ). For simplicity of presentation we will assume that rules in Π do not have nested temporal operators and that their heads always mention either or . Note that these assumptions are without loss of generality, as we can always flatten nested operators by introducing additional rules, whereas an atom M with no temporal operators can be written as 0M (or equivalently as 0M) (Brandt et al. 2018). Note, moreover, that our rewriting technique does not require the input query to be a fact, namely the sequence t in the query Q(t)@ϱ can contain variables. Line 1 of Algorithm 1 computes D as an extension of D with the fact m Qγ0(bt(t,γ0))@ϱ. It is obtained from the query Q(t)@ϱ using a sequence γ0 of b and f such that the ith element is b if and only if the ith element of t is a constant. Lines 2 3 compute the adorned program Πa. In particular, Line 2 initialises the set A of adorned idb predicates that are still to be processed and the set Πa of adorned rules. Then, Line 3 constructs Πa in the same way as in the case of Datalog (see Preliminaries). Line 4 initialises, as an empty set, Π and two auxiliary sets of rules Π 1 and Π 2. Then, Lines 5 9 compute a set Π 1 of rules of the first type and Lines 10 15 compute a set Π 2 of rules of the second type (to be precise, Π 1 and Π 2 become rules of the first and the second type after removing adornments in Line 17). In particular, the loop from Lines 5 9 constructs from each r Πa a rule r and adds it to Π 1. To construct r , Lines 7 8 check if the head of r mentions or . In the first case, Line 7 adds an atom with | and a magic predicate to the rule body. In the second case, Line 8 adds an atom with x and a magic predicate to the rule body. Then, Line 9 adds r to Π 1. Lines 10 15 construct rules Π 2 of the second type from rules in Π 1. To this end, for each rule r in Π 1 (Line 10) and each body atom M in r which mentions an idb predicate (Line 11) the algorithm performs the following computations. In Line 12 it computes a set H of atoms with magic predicates which will be used to construct rule heads. This is performed with a function Magic Head Atoms implemented with Algorithm 2, which we will describe later. Then, the loop in Lines 13 15 computes a rule r for each atom M in H and adds this r to Π 2. Rule r is constructed from r in Line 14, by replacing the head with M and deleting from the rule body M as well as all the other body atoms located to the right of M. To construct the final program Π from Π 1 and Π 2, Line 16 constructs the union of these two sets and Line 17 deletes from these rules all the adornments of predicates which are non-magic, that is, not preceded by m . Line 18 returns the pair consisting of Π and D .

Algorithm 1: Magic Rewriting

Input : A Datalog MTL program Π, dataset D, and query q = Q(t)@ϱ Output: A Datalog MTL program Π and dataset D

1 D = D {m Qγ0(bt(t,γ0))@ϱ} ;

2 A = {Qγ0} ; Πa = ;

3 Πa = a program obtained from Π by applying Step 2 from Section Magic Set Rewriting until A = ;

4 Π = ; Π 1 = ; Π 2 = ;

5 foreach rule r Πa do

6 Let ϱ Rγ(t), with { , }, be the head of r ;

7 if = then r = r with |ϱ m Rγ(bv(t,γ)) added as the first body atom ;

8 if = then r = r with xϱ m Rγ(bv(t,γ)) added as the first body atom ;

9 Π 1 = Π 1 {r } ;

10 foreach rule r Π 1 do

11 foreach M body(r) with an idb predicate do

12 H = Magic Head Atoms(M) ;

13 foreach atom M H do

14 r = r with head replaced by M and body modified by deleting M and all body atoms to the right of M ;

15 Π 2 = Π 2 {r } ;

16 Π = Π 1 Π 2 ;

17 Delete adornments from non-magic predicates in Π ;

18 return (Π ,D );

Magic Head Atoms. The function Magic Head Atoms is used to construct rules of the second type (i.e. the set Π 2), as presented in Algorithm 2. The algorithm takes as input a metric atom M and returns a set H of metric atoms, whose predicates are magic predicates. Line 1 initialises H as the empty set and introduces an auxiliary M which is set to M. The loop in Lines 2 3 modifies M by replacing idb predicates with magic predicates. Then, Lines 4-18 construct the set H depending on the form of M . Line 4 consider the cases when M mentions or . Line 5 considers the case when M mentions |, and Line 6 when M mentions x. Lines 7-12 are for the case when M mentions S and Lines 13-18 when M mentions U. The final set H is returned in Line 19.

Correctness of the Algorithm. Next we aim to show that, given a program Π, a dataset D, and a query q = Q(t)@ϱ, the pair (Π ,D ) returned by Algorithm 1 entails the same answers to q as (Π,D). This result is provided by the following theorem. Theorem 1. Let Π be a Datalog MTL program, D a dataset, Q(t)@ϱ a query, and (Π ,D ) the output of Algorithm 1 when run on Π, D, and Q(t)@ϱ. For each time point t ϱ and each substitution σ mapping variables in t to constants we have

(Π,D) Q(σ(t))@t iff (Π ,D ) Q(σ(t))@t.

Proof Sketch. For the if part, we leverage the fact that the first kind of rules in Π (i.e. rules in Π 1) are constructed by

Algorithm 2: Magic Head Atoms

Input : A metric atom M Output: A set H of metric atoms with magic predicates

1 H = ; M = M ;

2 foreach adorned idb relational atom Rγ(t) in M do

3 Replace Rγ(t) in M with m Rγ(bv(t,γ)) ;

4 if M = ϱM1 or M = ϱM1 then H = {M } ;

5 if M = |ϱM1 then H = { ϱM1} ;

6 if M = xϱM1 then H = { ϱM1} ;

7 if M = M2 SϱM1 then

8 tmax = the right endpoint of ϱ ;

9 if M2 contains a magic predicate then

10 H = H { [0,tmax]M2} ;

11 if M1 contains a magic predicate then

12 H = H { ϱM1} ;

13 if M = M2 UϱM1 then

14 tmax = the right endpoint of ϱ ;

15 if M2 contains a magic predicate then

16 H = H { [0,tmax]M2} ;

17 if M1 contains a magic predicate then

18 H = H { ϱM1} ;

19 return H ;

adding body atoms with magic predicates to the bodies of rules in Π. Hence, we can show that each fact entailed by (Π ,D ) is also entailed by (Π,D). The opposite direction is more challenging. The main part of the proof is to show that if (Π,D) R(t)@t and (Π ,D ) m Rγ(bt(t,γ))@t for some R(t)@t and γ, then (Π ,D ) Rγ(bt(t,γ))@t. This is sufficient to finish the proof. Indeed, note that by the construction of D , it contains m Qγ0(bt(t,γ0))@ϱ. Therefore, by the implication above we have (Π ,D ) m Qγ0(bt(t,γ0))@t, as required. To show the needed implication we conduct a proof by a transfinite induction on the number of TΠ applications to ID and TΠ applications to ID .

Reasoning with the Algorithm. Theorem 1 shows us that to answer a query q with respect to Π and D, we can instead answer q with respect to Π and D constructed by Algorithm 1. In what follows we will show how to efficiently answer q with respect to Π and D . For this, we will use a recently introduced approach by Wałe ga et al. (2023b), which constructs a finite representation of (usually infinite) canonical model of a program and a dataset. Importantly, this approach is guaranteed to terminate, which stands in contrast with a pure materialisation approach in Datalog MTL that often requires a transfinite number of rule applications. Although the approach of Wałe ga et al. (2023b), presented in their Algorithm 1, overperforms other reasoning techniques for Datalog MTL, it is worth observing that it is guaranteed to terminate only if the input program and dataset are both bounded (i.e. mention only bounded intervals). Moreover, the runtime of their algorithm heavily depends on the distance between the minimal and maximal time points in the input dataset. This makes applying their algorithm in our

setting challenging, because time points of our D depend on the input query. Indeed, D constructed in Line 1 of our Algorithm 1 contains the fact m Qγ0(bt(t,γ0))@ϱ, whose interval ϱ is copied from the input query q = Q(t)@ϱ. Hence, if ϱ is large, then applying the approach of Wałe ga et al. (2023b) may be inefficient. Moreover, if ϱ is unbounded, then so is D , and we loose the guarantee of termination. We will address these challenges below. First, we observe that given a program Π, dataset D, and query q = Q(t)@ϱ, instead of computing Magic Rewriting(Π,D,Q(t)@ϱ) we can compute Magic Rewriting(Π,D,Q(t)@( ,+ )) and the new program-dataset pair will still entail the same answers to q as the the input Π and D. This is a simple consequence of Theorem 1 as stated formally below. Corollary 2. Let Π be a Datalog MTL program, D a dataset, Q(t)@ϱ a query, and (Π ,D ) the output of Algorithm 1 when run on Π, D, and Q(t)@( ,+ ). For each time point t ϱ and each substitution σ mapping variables in t to constants we have

(Π,D) Q(σ(t))@t iff (Π ,D ) Q(σ(t))@t.

We note that Magic Rewriting(Π,D,Q(t)@( ,+ )) constructs a pair (Π ,D ) such that D contains m R(t)@( ,+ ). Hence, D is not bounded, and so, application of Algorithm 1 by Wałe ga et al. (2023b) to Π , D , and q is not guaranteed to terminate. What we show next, however, is that unboundedness of m R(t)@( ,+ ) does not lead to non-termination. Indeed, if Π and D are bounded, then the algorithm of Wałe ga et al. (2023b) is guaranteed to terminate on Π , D , and q, as stated next. Theorem 3. Let Π be a bounded program, D a bounded dataset, q = Q(t)@ϱ a fact, and (Π ,D ) the output of Algorithm 1 when run on Π, D, and Q(t)@( ,+ ). Application of Algorithm 1 by Wałe ga et al. (2023b) is guaranteed to terminate on Π , D , and q, even though D is not bounded.

Proof Sketch. Observe that the program Π constructed by our Algorithm 1 is bounded and the only unbounded fact in D is m Qγ0(bt(t,γ0))@( ,+ ). To show that application of Algorithm 1 by Wałe ga et al. (2023b) terminates on Π , D , and q, we replace the unbounded fact in D with an additional rule in Π , namely we construct Π by extending Π with a single rule m Qγ0(bt(t,γ0)) , which simulates m Qγ0(bt(t,γ0))@( ,+ ). We can show that the number of iterations of their algorithm running on (Π ,D,q) is equal to or greater than the number of its iterations on (Π ,D ,q) by one. Since Π and D are bounded, both of the above mentioned numbers of iterations need to be finite. Hence, the algorithm is guaranteed to terminate on Π , D , and q, as stated in the theorem.

Hence, we obtain a terminating approach for reasoning in Datalog MTL with magic set rewriting. To sum up, our approach to check entailment of a fact q = Q(t)@ϱ with respect to a program Π and a dataset D consists of two steps. The first step is to construct Π and D by applying our Algorithm 1 to Π, D, and Q(t)@( ,+ ). The second step is to apply Algorithm 1 of Wałe ga et al. (2023b) to Π , D , and q. This method is guaranteed to terminate and correctly

answer if Π and D entail q. In the next section we will study performance of this new approach.

Empirical Evaluation

We implemented our algorithm and evaluated it on LUBMt (Wang et al. 2022) a temporal version of LUBM (Guo, Pan, and Heflin 2005) , on i Temporal (Bellomarini, Nissl, and Sallinger 2022), and on the meteorological (Maurer et al. 2002) benchmarks. The aim of our experiments is to check how the performance of reasoning with magic programs compare with reasoning using original programs. The three programs we used have 85, 11, and 4 rules, respectively. Moreover, all our test queries are facts (i.e. they do not have free variables) since current Datalog MTL system do not allow for answering queries with variables (they are designed to check entailment). Given a program Π and a dataset D we used Me Teo R system (Wałe ga et al. 2023b) to perform reasoning. The engine first loads the pair and preprocesses the dataset before it starts reasoning. Then, for each given query fact, we record the wall-clock time that the baseline approach (Wałe ga et al. 2023b) takes to answer the query. For our approach, we record the time taken for running Algorithm 1 to generate the transformed pair (Π ,D ) plus the time of answering the query via the materialisation of (Π ,D ). We ran the experiments on a server with 256 GB RAM, Intel Xeon Silver 4210R CPU @ 2.40GHz, Fedora Linux 40, kernel version 6.8.5-301.fc40.x86 64. In each test case, we verified that both our approach and the baseline approach produced the same answer to the same query. Moreover, we observed that the time taken by running Algorithm 1 was in all test cases less than 0.01 second, so we do not report these numbers separately. Note that our results are not directly comparable to those presented by Wałe ga et al. (2023b) and Wang et al. (2022), since the datasets and queries are generated afresh, and different hardware is used. The datasets we used, the source code of our implementation, as well as an extended technical report, are available online.1

Comparison With Baseline. We compared the performance of our approach to that of the reasoning with original programs on datasets from LUBMt with 106 facts, i Temporal with 105 facts, and ten year s worth of meteorological data. We ran 119, 35, and 28 queries on them respectively. These queries cover every idb predicate and are all facts. The results are summarised on the box plot in Figure 1. The red and orange boxes represent time statistics for magic programs and the original program, respectively, while the blue box represents the per-query time ratios. Since computing finite representations using the baseline programs requires too much time for LUBMt and i Temporal (more than 100,000s and 50,000s) and memory and time consumption should theoretically stay the same across each computation, we used an average time for computing finite representations as the query time for each not entailed query instead of actually running them. For the LUBMt case, we achieved a performance boost on

1https://github.com/Royal Raisins/Magic-Sets-for-Datalog MTL

every query, the least enhanced (receiving the least speedup among other queries compared with the original program) of these received a 1.95 times speedup. For the entailed queries, half were accelerated by more than 3.46 times, 25% were answered more than 112 times faster. The most enhanced query were answered 2,110 times faster. For the not entailed queries, every query was accelerated by more than 12 times. Three quarters of the queries were answered more than 128 times faster using magic programs than the original program, 25% were answered more than 9,912 times faster. The most enhanced query were answered 111,157 times faster. It is worth noting that for the queries where a performance uplift are most needed, which is when the original program s finite representation needs to be computed, especially when the query fact is not entailed, our rewritten pairs have consistently achieved an acceleration of more than 12 times, making the longest running time of all tested queries 12 times shorter. This can mean that some program-dataset pairs previously considered beyond the capacity of the engine may now be queried with acceptable time costs.

For the meteorological dataset case, the results resemble those of LUBMt, with the least accelerated query being answered 1.58 times faster. Half of the queries were answered more than 3.54 times. One particular query was answered more than 1 million times faster.

For the i Temporal case, we achieved a more than 69,000 times performance boost on every query, some over a million times. As can be observed from the chart on the right in Figure 1, the general performance boost is considerable and rather consistent across queries. The huge performance boost is because in this case, an idb fact has very few relevant facts and derivations of the vast majority of idb facts were avoided by magic programs.

Scalability Experiments. We conducted scalability experiments on both LUBMt and i Temporal benchmarks as they are equipped with generators allowing for constructing datasets of varying sizes. For LUBMt, we generated datasets of 5 different sizes, 102 106, and used the program provided along with the benchmark; for each dataset size, we selected 30 queries. For i Temporal, the datasets are of sizes 10 105 and the program was automatically generated; for each dataset size, we selected 270 queries. To rule out the impact of early termination and isolate the effect that magic sets rewriting has on the materialisation time, we only selected queries that cannot be entailed so that the finite representation is always fully computed. These queries were executed using both approaches, with the average execution time computed and displayed as the red (Π for original program) and blue (Π for magic program) lines in Figure 2.

As the chart shows, our magic programs scale better for LUBMt than the original program in terms of canonical model computation. For i Temporal, the first two datasets are too small that both approaches compute the results instantaneously. As the size of a dataset increases from 103 to 105, we observe a similar trend as LUBMt.

Π Π Π/Π Π Π Π/ Π 100

Π Π Π/Π Π Π Π/ Π 10 2 10 1 100 101 102 103 104 105

Π Π Π/Π Π Π Π/ Π 10 4 10 3 10 2 10 1 100 101 102 103

Meteorological

Figure 1: Comparison with baseline; ( )Π , ( )Π, ( )Π/( )Π refer to time consumed by (not) entailed queries on magic programs, the baseline program, and to per-query time ratios. Scales for ratios are on the right

Conclusion and Future Work

We have extended the magic set rewriting technique to the temporal setting, which allowed us to improve performance of query answering in Datalog MTL. We have obtained a goal-driven approach, providing an alternative to the state-of-the-art materialisation-based method in Datalog MTL. Our new approach can be particularly useful in applications where the input dataset changes frequently or the materialisation of the entire program and dataset is not feasible due to too high time and space consumption. In future, we plan to consider developing a hybrid approach that combines magic sets technique with materialisation. Another interesting avenue is to extend the magic sets approach to languages including such features such as negation and aggregation.

102 103 104 105 106 10 1 100 101 102 103 104 105 106

LUBM Dataset Size

101 102 103 104 105 10 2 10 1 100 101 102 103 104 105

i Temporal Dataset Size

Figure 2: Scalability results, where Π stands for a magic program and Π for an original program

Acknowledgements This work was funded by NSFC grants 62206169 and 61972243. It is also partially supported by the EPSRC projects OASIS (EP/S032347/1), Con Cu R (EP/V050869/1) and UK FIRES (EP/S019111/1), as well as SIRIUS Centre for Scalable Data Access and Samsung Research UK. For the purpose of Open Access, the authors have applied a CC BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission. We thank Prof. Boris Motik for proofreading the manuscript and providing insightful comments.

References Abiteboul, S.; Hull, R.; and Vianu, V. 1995. Foundations of Databases. Addison-Wesley. Bellomarini, L.; Blasi, L.; Nissl, M.; and Sallinger, E. 2022. The Temporal Vadalog System. In Rules and Reasoning - International Joint Conference on Rules and Reasoning, Rule ML+RR, volume 13752, 130 145. Bellomarini, L.; Nissl, M.; and Sallinger, E. 2021. Monotonic Aggregation for Temporal Datalog. In 15th International Rule Challenge, 7th Industry Track, and 5th Doctoral Consortium @ Rule ML+RR, volume 2956. Bellomarini, L.; Nissl, M.; and Sallinger, E. 2022. i Temporal: An Extensible Generator of Temporal Benchmarks. In International Conference on Data Engineering, ICDE 2022, 2021 2033. Brandt, S.; Kalayci, E. G.; Ryzhikov, V.; Xiao, G.; and Zakharyaschev, M. 2018. Querying Log Data with Metric Temporal Logic. J. Artif. Intell. Res., 62: 829 877. Ceri, S.; Gottlob, G.; and Tanca, L. 1989. What you Always Wanted to Know About Datalog (And Never Dared to Ask). IEEE Trans. Knowl. Data Eng., 1(1): 146 166. Colombo, A.; Bellomarini, L.; Ceri, S.; and Laurenza, E. 2023. Smart Derivative Contracts in Datalog MTL. In International Conference on Extending Database Technology, EDBT, 773 781. Faber, W.; Greco, G.; and Leone, N. 2007. Magic Sets and their application to data integration. J. Comput. Syst. Sci., 73(4): 584 609. Guo, Y.; Pan, Z.; and Heflin, J. 2005. LUBM: A benchmark for OWL knowledge base systems. J. Web Semant., 3(2-3): 158 182.

G uzel Kalayci, E.; Xiao, G.; Ryzhikov, V.; Kalayci, T. E.; and Calvanese, D. 2018. Ontop-temporal: a tool for ontology-based query answering over temporal data. In ACM International Conference on Information and Knowledge Management, 1927 1930. Koymans, R. 1990. Specifying Real-Time Properties with Metric Temporal Logic. Real Time Syst., 2(4): 255 299. Maurer, E. P.; Wood, A. W.; Adam, J. C.; Lettenmaier, D. P.; and Nijssen, B. 2002. A Long-Term Hydrologically Based Dataset of Land Surface Fluxes and States for the Conterminous United States. Journal of Climate, 15(22): 3237 3251. Mori, M.; Papotti, P.; Bellomarini, L.; and Giudice, O. 2022. Neural Machine Translation for Fact-checking Temporal Claims. In Fact Extraction and VERification Workshop, 78 82. Nissl, M.; and Sallinger, E. 2022. Modelling Smart Contracts with Datalog MTL. In Workshops of the EDBT/ICDT, volume 3135. Tena Cucala, D. J.; Wałe ga, P. A.; Cuenca Grau, B.; and Kostylev, E. V. 2021. Stratified Negation in Datalog with Metric Temporal Operators. In AAAI Conference on Artificial Intelligence, 6488 6495. Ullman, J. D. 1989a. Bottom-up beats top-down for datalog. In Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS, 140 149. Ullman, J. D. 1989b. Principles of Database and Knowledge-Base Systems, Volume II. Computer Science Press. Wałe ga, P.; Zawidzki, M.; and Cuenca Grau, B. 2021. Finitely Materialisable Datalog Programs with Metric Temporal Operators. In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 619 628. Wałe ga, P.; Zawidzki, M.; and Cuenca Grau, B. 2023. Finite materialisability of Datalog programs with metric temporal operators. Journal of Artificial Intelligence Research, 76: 471 521. Wałe ga, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2019. Datalog MTL: Computational Complexity and Expressive Power. In International Joint Conference on Artificial Intelligence, IJCAI, 1886 1892. Wałe ga, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2020a. Datalog MTL over the integer timeline. In International Conference on Principles of Knowledge Representation and Reasoning, KR, 768 777. Wałe ga, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2020b. Tractable Fragments of Datalog with Metric Temporal Operators. In International Joint Conference on Artificial Intelligence, IJCAI, 1919 1925. Wałe ga, P. A.; Kaminski, M.; and Cuenca Grau, B. 2019. Reasoning over streaming data in metric temporal Datalog. In AAAI Conference on Artificial Intelligence, 3092 3099. Wałe ga, P. A.; Kaminski, M.; Wang, D.; and Cuenca Grau, B. 2023a. Stream reasoning with Datalog MTL. Journal of Web Semantics, 76: 100776.

Wałe ga, P. A.; Tena Cucala, D. J.; Cuenca Grau, B.; and Kostylev, E. V. 2024. The stable model semantics of datalog with metric temporal operators. Theory and Practice of Logic Programming, 24(1): 22 56. Wałe ga, P. A.; Tena Cucala, D. J.; Kostylev, E. V.; and Cuenca Grau, B. 2021. Datalog MTL with Negation Under Stable Models Semantics. In International Conference on Principles of Knowledge Representation and Reasoning, KR, 609 618. Wałe ga, P. A.; Zawidzki, M.; Wang, D.; and Cuenca Grau, B. 2023b. Materialisation-Based Reasoning in Datalog MTL with Bounded Intervals. In AAAI Conference on Artificial Intelligence, 6566 6574. Wang, D.; Hu, P.; Wałe ga, P. A.; and Cuenca Grau, B. 2022. Me Teo R: Practical Reasoning in Datalog with Metric Temporal Operators. In AAAI Conference on Artificial Intelligence, 5906 5913.