Combining Rewriting and Incremental Materialisation Maintenance for Datalog Programs with Equality

1 Introduction

Datalog [Abiteboul et al., 1995] is a declarative, rule-based language that can describe (possibly recursive) data dependencies. It is widely used in applications as diverse as enterprise data management [Aref, 2010] and query answering over ontologies in the OWL 2 RL profile [Motik et al., 2009] extended with SWRL rules [Horrocks et al., 2004].

Querying the set Π∞(E) of consequences of a set of explicit facts E and a datalog program Π is a key service in datalog systems. It can be supported by precomputing and storing Π∞(E) so that queries can be evaluated directly, without further reference to Π. Set Π∞(E) and the process of computing it are called the materialisation of E w.r.t. Π. This technique is used in the state of the art systems such as Olwgres [Stocker and Smith, 2008], WebPIE [Urbani et al., 2012], Oracle's RDF store [Wu et al., 2008], GraphDB (formerly OWLIM) [Bishop et al., 2011], and RDFox [Motik et al., 2014].

Although datalog traditionally employs the unique name assumption (UNA), in some applications uniqueness of identifiers cannot be guaranteed. For example, due to the distribution and the independence of data sources, in the Semantic Web different identifies are often used to refer to the same domain object. Handling such use cases requires an extension of datalog without UNA, in which one can infer equalities between constants using a special equality predicate ≈ that can occur in facts and rule heads. The semantics of ≈ can be captured explicitly using rules that axiomatise ≈ as a congruence relation; however, this is known to be inefficient when equality is used extensively. Therefore, systems commonly use rewriting [Baader and Nipkow, 1998; Nieuwenhuis and Rubio, 2001]-an optimisation where equal constants are replaced with a canonical representative, and only facts containing such representatives are stored. The benefits of rewriting have been well-documented in practice [Wu et al., 2008; Urbani et al., 2012; Bishop et al., 2011; Motik et al., 2015b].

Moreover, datalog applications often need to handle continuous updates to the set of explicit facts E. Rematerialisation (i.e., computing the materialisation from scratch) is often very costly, so incremental maintenance algorithms are often used in practice. Adding facts to E is trivial as one can simply continue from where the initial materialisation has finished; hence, given a materialisation Π∞(E) of E w.r.t. Π and a set of facts E-, the main challenge for an incremental algorithm is to efficiently compute Π∞(E \ E-). Several such algorithms have already been proposed. Truth maintenance systems [Doyle, 1979; de Kleer, 1986; Goasdou´e et al., 2013] track dependencies between facts to efficiently determine whether a fact has a derivation from E \ E-, so only facts for which no such derivations exist are deleted. Such approaches, however, store large amounts of auxiliary information and are thus often unsuitable for data-intensive applications. Counting [Nicolas and Yazdanian, 1983; Gupta et al., 1993; Urbani et al., 2013; Goasdou´e et al., 2013] stores with each fact F ∈ Π∞(E) the number of times F has been derived during initial materialisation, and this number is used to determine when to delete F ; however, in its basic form counting works only with nonrecursive rules, and a proposed extension to recursive rules requires multiple counts per fact [Dewan et al., 1992], which can be costly. The Delete/Rederive (DRed) algorithm [Gupta et al., 1993] handles recursive rules with no storage overhead: to delete E- from E, the algorithm first overdeletes all consequences of E- in Π∞(E) and then rederives all facts provable from E \ E-. The Backward/Forward (B/F) algorithm combines backward and forward chaining in a way that outperforms DRed on inputs where facts have many alternative derivations-a common scenario in Semantic Web applications [Motik et al., 2015c].

Combining rewriting and incremental maintenance is difficult due to complex interactions between the two techniques: removing E- from E may entail retracting equalities, which may (partially) invalidate the rewriting and require the restoration of rewritten facts (see Section 3). To the best of our knowledge, such a combination has not been considered in the literature, and practical systems either use rewriting with rematerialisation, or axiomatise equality and use incremental maintenance; in either case they give up a technique known to be critical for performance. In this paper we present the B/F≈ algorithm, which combines rewriting with B/F: given a set of facts E-, our algorithm efficiently updates the materialisation of E w.r.t. Π computed using the rewriting approach by Motik et al. (2015b). Extensions of datalog with equality are nowadays used mainly for querying RDF data extended with OWL 2 RL ontologies and SWRL rules, so we formalise our algorithm in the framework of RDF; however, our approach can easily be adapted to general datalog.

We have implemented B/F≈ in the open-source RDFox system 1 and have evaluated it on several real-world and synthetic datasets. Our results show that the algorithm indeed combines the best of both worlds, as it is often several orders of magnitude faster than either rematerialisation with rewriting, or B/F with axiomatised equality.

2 Preliminaries

Datalog. A term is a constant (a, b, A, R, etc.) or a variable (x, y, z, etc.). An (RDF) atom has the form 〈t1, t2, t3〉, where t1, t2, t3 are terms; an (RDF) fact (also called a triple) is a variable-free RDF atom; and a dataset is a finite set of facts. A (datalog) rule r is an implication of the form (1), where H,B1, . . . ,Bn are atoms and each variable occurring in H also occurs in some Bi; h(r) ··= H is the head atom of r; each Bi is a body atom of r; and b(r) is the set of all body atoms of r. A (datalog) program is a finite set of rules.

A substitution is a partial mapping of variables to terms. For α a term, atom, rule, or a set of these, voc(α) is the set of all constants in α, and ασ is the result of applying a substitution σ to α. The materialisation Π∞(E) of a dataset E w.r.t. a program Π is the smallest superset of E containing h(r)σ for each rule r ∈ Π and substitution σ with b(r)σ ⊆ Π∞(E).

Equality. The constant owl:sameAs (abbreviated ≈) can be used to encode equality between constants. For example, fact 〈P. Smith,≈, Peter Smith〉 states that P. Smith and Peter Smith are one and the same object. Facts of the form 〈s,≈, t〉 are called equalities and, for readability, are abbreviated as s ≈ t; note that ≈ ∈ voc(s ≈ t). Program Π≈ consisting of rules (≈1)-(≈4) axiomatises ≈ as a congruence relation. If a program Π or a dataset E contain ≈, systems then answer queries in the materialisation of E w.r.t. Π ∪ Π≈.

1 http://www.cs.ox.ac.uk/isg/tools/RDFox/

Rewriting is a well-known optimisation of this approach. For π a mapping of constants to constants and α a constant, fact, rule, dataset, or substitution, π(α) is the result of replacing each constant c in α with π(c); such α is normal w.r.t. π if π(α) = α; and π(α) is the representative of α in π. For c a constant, let cπ ··= {d | π(d) = c}. For U a dataset, let U π ··= {〈s, p, o〉 | 〈π(s), π(p), π(o)〉 ∈ U}; and, for F a fact, let F π ··= {F}π . We assume that all constant are totally ordered such that ≈ is the smallest constant; then, for S a nonempty set of constants, minS (resp. maxS) is the smallest (resp. greatest) element of S. Let U be a dataset and let Ec(U) ··= {c} ∪ {d | c ≈ d ∈ U}; then, the rewriting of U is the pair (π, I) such that

Note that π(≈) = ≈, that the rewriting is unique for U, and that Π∞≈ (U) = U implies I π = U. The r-materialisation of a dataset E w.r.t. a program Π is the rewriting (π, I) of the dataset J = (Π ∪ Π≈)∞(E). Motik et al. (2015b) show how to answer queries over J by materialising (π, I) instead of J.

3 Updating R-Materialisation Incrementally

Let E and E- be datasets, let E′ = E \ E-, and let Π be a program. Moreover, let J (resp. J ′ ) be the materialisation of E (resp. E′ ) w.r.t. Π∪Π≈, and let (π, I) (resp. (π′ , I ′ )) be the r-materialisation of E (resp. E′ ) w.r.t. Π. Given (π, I), Π, and E-, the B/F≈ algorithm computes (π′ , I ′ ) efficiently by combining the B/F algorithm by Motik et al. (2015c) for incremental maintenance in datalog without equality with the r-materialisation algorithm by Motik et al. (2015b). We discuss the intuition in Section 3.1 and some optimisations in Section 3.2, and we formalise the algorithm in Section 3.3.

3.1 Intuition

Main Difficulty. An update may lead to the deletion of equalities, which may require adding facts to I. The following example program Π and dataset E exhibit such behaviour.

Relation R is bijective in Π, so a ≈ c ∈ J as both a and c have outgoing R-edges to d, and b ≈ d ∈ J as both b and d have incoming R-edges from a. By rewriting, we represent each fact 〈α, R, β〉 from J using a single fact 〈a, R, b〉, and analogously for facts involving ≈; thus, instead of 14 facts, we store just five facts. Assume now that we remove Efrom E. In J and J ′ we ascribe no particular meaning to ≈, so the monotonicity of datalog ensures J ⊆ J ′ ; thus, the B/F algorithm just needs to delete facts that no longer hold.

However, a ≈ c ̸∈ J ′ and b ≈ d ̸∈ J ′ , so we must update π and extend I with the facts from J ′ that are not represented via π′ . Thus, in our example, I ′ actually contains I.

Solution Overview. B/F≈ consists of Algorithms 1-7 that follow the same basic idea as B/F; to highlight the differences, lines that exist in B/F in a modified form are marked with '∗', and new lines and algorithms are marked with'▷'.

We initially mark all facts in π(E-) as 'doubtful'-that is, we indicate that their truth might change. Next, for each 'doubtful' fact F, we determine whether F is provable from E′ and, if not, we identify the immediate consequences of F (i.e., the facts in I that can be derived using F ) and mark them as 'doubtful'; we know exactly which facts have changed after processing all 'doubtful' facts. To check the provability of F , we use backward chaining to identify the facts in I that can prove F, and we use forward chaining to actually prove F. The latter process also identifies the necessary changes to π and I, which we apply to (π, I) in a final step. We next describe the components of B/F≈ in more detail.

Procedure saturate() is given a dataset C ⊆ I of checked facts, and it computes the set L containing each fact F derivable from E′ such that each fact in a derivation of F is contained in C π ; thus, C identifies the part of J ′ to recompute. Rather than storing L directly, we adapt the r-materialisation algorithm by Motik et al. (2015b) and represent L by its rewriting (γ, P \ ˆ P); the role of the two sets P and ˆ P is discussed shortly. Lines 36-40 compute the facts in L derivable immediately from E′ : we iterate over each F ∈ C and each G ∈ F π ; since we represent L by its rewriting, we add γ(G) to P. The roles of set Y and lines 37-39 will be discussed shortly. Lines 41-50 compute the facts in L derivable using rules: we consider each fact F in P \ ˆ P (lines 41-42), each rule r, and each match σ of F to a body atom of r (line 48), we evaluate the remaining body atoms of r (line 49), and we derive γ(h(r)τ) for each match τ (line 50). This basic idea is slightly more complicated by rewriting: if F = a ≈ b, we modify γ so that one constant becomes the representative of the other one (line 45). As a consequence, facts can become 'outdated' w.r.t. γ, so we keep track of such facts using ˆ P: if F is 'outdated', we add F to ˆ P and γ(F) to P (line 44); due to the latter, P \ ˆ P eventually contains all 'up to date' facts. Finally, we apply the reflexivity rules (≈4) to F (line 47).

Procedure saturate() is repeatedly called in B/F≈. Set C, however, never shrinks between successive calls, so set L never shrinks either; hence, at each call we can just continue the computation instead of starting 'from scratch'. A minor problem arises if we derive a fact F with F ̸∈ C π and so we do not add γ(F) to P , but C is later extended so that F ∈ C π holds. We handle this by maintaining a set Y of 'delayed' facts: in line 59 we add F to Y if F ̸∈ C π ; and in line 40 we identify each 'delayed' fact G ∈ C π ∩ Y and add γ(G) to P .

Procedure rewrite(a, b) implements rewriting: we update γ (line 52), apply the replacement rules (≈1)-(≈3) to already processed facts containing 'outdated' constants (line 54), ensure that Γ is normal w.r.t. γ (line 56), and reapply the normalised rules (lines 57-58). Motik et al. (2015b) discuss in detail the issues related to rule updating and reevaluation.

Procedure checkProvability() takes a fact F ∈ I and ensures that, for each G ∈ F π , we have G ∈ J ′ iff γ(G) ∈ P \ ˆ Pthat is, we know the correct status of each fact that F represents. To this end, we add F to C (line 22) and thus ensure that (γ, P \ ˆ P) correctly represents L (line 23). Each fact is added to C only once, which guarantees termination of the recursion. We then use backward chaining to examine facts occurring in proofs of F and recursively check their provability; we stop at any point during that process if all facts in F π become provable (lines 24, 28, 31, and 35). Lines 2524 handle the reflexivity rules (≈4): to check provability of c ≈ c, we recursively check the provability each fact containing c. Lines 29-31 handle replacement rules (≈1)-(≈3): we recursively check the provability of c ≈ c for each constant c occurring in F . Finally, lines 32-35 handle the rules in π(Π): we consider each rule r ∈ π(Π) whose head matches F and each substitution τ that matches the body of r in I, and we recursively check the provability of b(r)τ .

Procedure BF≈() computes the set D ⊆ I of 'doubtful' facts. After initialising D to π(E-) (lines 3-4), we consider each fact F ∈ D (lines 5-16) and determine whether some G ∈ F π is no longer provable (line 6); if so, we add to D all facts that might be affected by the deletion of G. Lines 9-11 handle rules (≈1)-(≈3); line 12 handles rules (≈4); and lines 13-15 handle π(Π): we identify each rule r ∈ π(Π) where F matches a body atom of r, we evaluate the remaining body atoms of r in I, and we add h(r)τ to D for each τ such that b(r)τ ⊆ I. Once D is processed, (γ, P \ ˆ P) reflects the changes to (π, I), which we exploit in Algorithm 2.

3.2 Optimisations

Reflexivity. Facts of the form F = c ≈ c can be expensive for backward chaining: due to reflexivity rules (≈4), in lines 2528 we may end up recursively proving each fact G that mentions c. However, F holds trivially if E′ contains a fact mentioning c, in which case we can consider F proven and avoid any recursion. This is implemented in lines 37-39.

Avoiding Redundant Derivations. Assume that Γ contains a rule y1 ≈ y2 ← 〈x, R, y1〉 ∧ 〈x, R, y2〉, and consider a call to saturate() in which facts 〈a, R, b〉 and 〈a, R, d〉 both end up in P . Unless we are careful, in line 50 we might consider substitution τ1 = {x ↦→ a, y1 ↦→ b, y2 ↦→ d} twice: once when we match 〈a,R, b〉 to 〈x, R, y1〉, and once when we match 〈a,R, d〉 to 〈x, R, y2〉. Such redundant derivations can substantially degrade performance.

To solve this problem, set V keeps track of the processed subset of P: after we extract a fact F from P, in line 42 we transfer F to V ; moreover, in line 49 we evaluate rule bodies in V \ ˆ P instead of P \ ˆ P. Now if 〈a,R, b〉 is processed before 〈a,R, d〉, at that point we have 〈a,R, d〉 ̸∈ V , so τ1 is not returned as a match in line 49; the situation when 〈a,R, d〉 is processed first is analogous. This, however, does not eliminate all repetition: τ2 = {x ↦→ a, y1 ↦→ b, y2 ↦→ b} is still considered when 〈a,R, b〉 is matched to either of the two body atoms in the rule. Therefore, we annotate (see Section 3.3) the body atoms of rules so that, whenever F is matched to some body atomBi, no atomBj preceding Bi in the body of r can be matched to F . In our example, τ2 is thus considered only when 〈a, R, b〉 is matched to 〈x, R, y1〉.

B/F≈ avoids redundant derivations in similar vein: set O tracks the processed subset of D; in lines 10 and 14 we match the relevant rules in I \ O; and in line 16 we add a fact to O once it has been processed.

Disproved Facts. For each F ∈ I with F π ∩ J ′ = ∅, no fact in F π participates in a proof of any fact in J ′ . Thus, in line 7 we collect all such facts in a set S of disproved facts, and in lines 26, 29, and 33 we exclude S from backward chaining.

Singletons. If we encounter F = c ≈ c in line 9 or 29 where c represents only itself (i.e., |cπ | = 1), then we know that no fact in F π can derive a new fact using rules (≈1)-(≈3), and so we can avoid considering rules (≈1)-(≈3).

3.3 Formalisation

We borrow the notation by Motik et al. (2015c) to formalise B/F≈. We recapitulate some definitions, present the pseudocode, and formally state the algorithm's properties.

Given a dataset X and a fact F , operation X.add(F) adds F to X, and operation X.delete(F) removes F fromX; both return t if X was changed. For iteration, operation X.next returns the next fact fromX, or ε if no such fact exists.

An annotated query has the form Q = B▷◁1 1 ∧ · · · ∧B▷◁k k , where each Bi is an atom and annotation ▷◁i is either empty or equal to ̸=. Given datasets X and Y and a substitution σ, operation X.eval(Q, Y, σ) returns a set containing each smallest substitution τ such that σ ⊆ τ and, for 1 ≤ i ≤ k, (i) Biτ ∈ X if ▷◁i is empty or (ii) Biτ ∈ X \ Y if ▷◁i is ̸=. We often write [Z \W] instead of X, meaning that Q is evaluated in the difference of sets Z and W.

Given a fact F, operation Π.matchHead(F) returns all tuples 〈r,Q, σ〉 with r ∈ Π a rule of the form (1), σ a substitution such that Hσ = F, and Q = B1 ∧ · · · ∧Bn. Moreover, operation Π.matchBody(F) returns all tuples 〈r,Q, σ〉 with r ∈ Π a rule of the form (1), σ a substitution such that Biσ = F for some 1 ≤ i ≤ n, and Q is defined as

Finally, given a mapping γ of constants to constants, and constants d and c, operation γ.mergeInto(d, c) modifies γ so that γ(e) = c holds for each constant e with γ(e) = d.

B/F≈ consists of Algorithms 1-7. Theorem 1 shows that the algorithm is correct and that, just like the semina¨ıve algorithm [Abiteboul et al., 1995], it does not repeat derivations; the proof is given in a technical report [Motik et al., 2015a].

4 Evaluation

We have implemented and evaluated the B/F≈ algorithm in the open-source RDF data management system RDFox. The system and the test data are all available online. 2

Objectives. Updates can be handled either incrementally or by rematerialisation, and equality can be handled either by rewriting or by axiomatisation, giving rise to four possible approaches to updates. Our first objective was to compare all of them to determine their relative strengths and weaknesses.

2 https://krr-nas.cs.ox.ac.uk/2015/IJCAI/RDFox/index.html

As E- increases in size, incremental update becomes harder, but rematerialisation becomes easier. Thus, our second objective was to investigate the relationship between the update size and the performance of the respective approaches.

Datasets. Equality is often used in OWL ontologies on the Semantic Web, so we based our evaluation on several wellknown synthetic and 'real' RDF datasets.

Each dataset comprises an OWL ontology and a set of explicit facts E. UOBM [Ma et al., 2006] extends LUBM [Guo et al., 2005], and we used the data generated for 100 universities; we did not use LUBM because it does not use ≈. Claros contains information about cultural artefacts. 3 DBpedia consists of structured information extracted from Wikipedia. 4 UniProt is a knowledge base about protein sequences; 5 we selected a subset of the original (very large) set of facts. Finally, OpenCyc is an extensive, manually curated upper ontology. 6

Following Zhou et al. (2013), we converted the ontologies into lower (L) and upper bound (U) programs: the former is the OWL 2 RL subset of the ontology transformed into datalog as described by Grosof et al. (2003), and the latter captures all consequences of the ontology using an unsound approximation. Upper bound programs are interesting as they tend to be 'hard'. We also manually extended the lower bound (LE) of Claros with 'hard' rules (e.g., we defined related documents as pairs of documents that refer to the same topic).

Update Sets. For each dataset, we randomly selected several subsets E- of E. We considered small updates of 100 and 5k facts on all datasets. Moreover, for each dataset we identified the 'equilibrium' point n at which B/F≈ and Remat≈ take roughly the same time. If n was large, we generated subsets E- with sizes equal to 25%, 50%, 75%, and 100% of n; otherwise, we divided n in an ad hoc way.

Test Setting. We used a Dell server with two 2.60GHz Intel Xeon E5-2670 CPUs and 256 GB of RAM running Fedora release 20, kernel version 3.17.7-200.fc20.x86 64.

Test Results. Table 1 summarises our test results. For each dataset, we show the numbers of explicit facts (|E|) and rules (|Π|), the number of facts in the initial r-materialisation (|I ≈|), and the time (T ≈) and the number of derivations (D≈) used to compute it via rewriting; moreover, we show the latter three numbers for the initial materialisation computed using axiomatised equality (|I A|, T A, and DA). For each set E-, we show the numbers ∆|I ≈| and ∆|I A| of deleted facts with rewriting and axiomatisation, respectively, as well as the times (T) and the number of derivations (D) for each of the four update approaches. All times are in seconds. We could not complete all axiomatisation tests with Claros-LE as each run took about two hours. Due to the upper bound transformation, the r-materialisation of UOBM-100-U contains a constant c with |cπ | = 3930; thus, when ≈ is axiomatised, deriving just all equalities involving cπ requires 39303 = 60 billion derivations, which causes the initial materialisation to last longer than four hours. The number of derivations D in

3 http://www.clarosnet.org/XDB/ASP/clarosHome/

4 http://dbpedia.org/

5 http://www.uniprot.org

6 http://www.cyc.com/platform/opencyc

Input Variables

E : the explicit facts

Π : the datalog program

(π, I) : the r-materialisation of E w.r.t. Π

E- : the facts to delete fromE

Global Temporary Variables

• D : the consequences of E- that may require deletion
• O : the processed subset of D
• C : the facts whose provability must be checked
• γ : the mapping recording the changes needed to π
• P : the proved facts
• ˆ P : the proved rewritten facts
• Y : the proved facts not in C π
• V : the processed subset of P
• S : the set of disproved facts

Algorithm 1 B/F≈()

• ∗ 1: C ··=D ··= P ··= ˆ P ··= Y ··= O ··= S ··= V ··= ∅
• ▷ 2: initialise γ as identity and Γ ··= Π
• 3: for each F ∈ E- do
• 4: if E.delete(F) then D.add(π(F))
• 5: while (F ··=D.next) ̸= ε do
• 6: checkProvability(F)
• ∗ 7: for each G ∈ C s.t. allDisproved(G) do S.add(G)
• ∗ 8: if not allProved(F) then
• ▷ 9: if F = c ≈ c and |cπ | > 1 then
• ▷10: for each G ∈ I \ O with c ∈ voc(G) do ▷11: D.add(G)
• ▷12: for each c ∈ voc(F ) do D.add(c ≈ c)
• 13: for each 〈r, Q, σ〉 ∈ π(Π).matchBody(F ) do
• 14: for each τ ∈ [I \ O].eval(Q, {F}, σ) do
• 15: D.add(h(r)τ )
• 16: O.add(F)
• ∗17: propagateChanges()

▷ Algorithm 2 propagateChanges()

• 18: for each c ≈ c ∈ C and each d with π(d) = c do
• 19: π(d) ··= γ(d)
• 20: for each F ∈ D \ (P \ ˆ P ) do I .delete(F )
• 21: for each F ∈ P \ ˆ P do I.add(π(F))

▷ Algorithm 3 Auxiliary functions

allProved(F ): t iff F ̸∈ S and γ(F π ) ⊆ (P \ ˆ P ) allDisproved(F ): t iff γ(F π ) ∩ (P \ ˆ P) = ∅

Theorem 1. Let (π, I) be the r-materialisation of a dataset E w.r.t. a program Π, and let E- be a dataset.

1. Algorithm 1 terminates, at which point (π, I) contains the r-materialisation of E \ E- w.r.t. Π.
2. Each combination of a rule r and a substitution τ is considered at most once in line 50 or line 58, but not both.
3. Each combination of a rule r and a substitution τ is considered at most once in line 15.

Algorithm 4 checkProvability(F )

• 22: if not C.add(F) then return
• 23: saturate()
• ∗24: if allProved(F) then return
• ▷25: if F = c ≈ c then
• ▷26: for each G ∈ I \ S with c ∈ voc(G) do
• ▷27: checkProvability(G)
• ▷28: if allProved(F) then return
• ▷29: for each c ∈ voc(F) with c ≈ c ̸∈ S and |cπ | > 1 do
• ▷30: checkProvability(c ≈ c)
• ▷31: if allProved(F) then return
• 32: for each 〈r,Q, σ〉 ∈ π(Π).matchHead(F) do
• 33: for each τ ∈ [I \ S].eval(Q, ∅, σ) and G ∈ b(r)τ do
• 34: checkProvability(G)
• 35: if allProved(F) then return

Algorithm 5 saturate()

• 36: while (F ··= C.next) ̸= ε do
• ▷37: if F = c ≈ c then

▷38:

▷39:

• for each d ∈ voc(E) with π(d) = c do P.add(γ(d) ≈ γ(d))
• ∗40: for each G ∈ F π ∩ (E ∪ Y ) do P.add(γ(G))
• 41: while (F ··= P.next) ̸= ε do
• ∗42: if F ∈ P \ ( ˆ P ∪ V ) and V.add(F) then ▷43: G ··= γ(F)
• ▷44: if F ̸= G then ˆ P .add(F ) and P.add(G)
• ▷45: else if F = a ≈ b and a ̸= b then rewrite(a, b) ▷46: else
• ∗47: for each c ∈ voc(G) do prove(c ≈ c)
• 48: for each 〈r, Q, σ〉 ∈ Γ.matchBody(G) do

for each τ ∈ [V \ ˆ

• ∗49: P ].eval(Q, {G}, σ) do ∗50: prove(h(r)τ )

▷ Algorithm 6 rewrite(a, b)

• 51: c ··=min{a, b} d ··=max{a, b}
• 52: γ.mergeInto(d, c)
• 53: for each F ∈ P \ ˆ P with d ∈ voc(F) do
• 54: ˆ P .add(F ) and P.add(γ(F ))
• 55: for each r ∈ Γ with r ̸= γ(r) do
• 56: replace r in Γ with r′ ··= γ(r)
• 57: for each τ ∈ [V \ ˆ P ].eval(b(r′ ), ∅, ∅) do
• 58: prove(h(r′ )τ )

▷ Algorithm 7 prove(F )

59: if π(F) ∈ C then P.add(F) else Y.add(F)

Claros-L

|E| = 18.8M |I ≈| = 79.5M T ≈ = 83 D≈ = 129M

|Π| = 1.3k |I A| = 102M T A = 3.9k DA = 11.0G

Claros-LE |E| = 18.8M |I ≈| = 539M T ≈ = 4514 D≈ = 12.6G

|Π| = 1.3k |I A| = 562M T A = 9048 DA = 26.3G

UniProt-L

|E| = 123M |I ≈| = 179M T ≈ = 118 D≈ = 183M

|Π| = 451 |I A| = 229M T A = 527 DA = 1.6G

B/F≈ is the sum of the number of times a fact is determined as 'doubtful' (lines 11, 12, and 15), checked in backward chaining (lines 27, 30, and 34), or derived in forward chaining (line 59); we use this number to estimate reasoning difficulty independently from implementation details.

Discussion. For updates of 100 facts, B/F≈ outperforms all other approaches, often by orders of magnitude, and in most cases it does so even for much larger updates.

Even when |I A| - |I ≈| is 'small' (i.e., when not many equalities are derived), B/F≈ outperforms B/FA. This seems to be mainly because B/FA ascribes no special meaning to Π≈ and so it does not use the optimisation from lines 37-39; thus, when trying to prove c ≈ c, B/FA performs backward chaining via rules (≈4) and so it potentially examines each fact containing c. On Claros-L, although |I A| and |I ≈| are of similar sizes, I A contains one constant c with |cπ | = 306, which gives rise to 3063 derivations; this explains the difference in the performance of B/F≈ and B/FA.

Remat≈ outperforms B/F≈ in cases similar to those described by Motik et al. (2015c). For example, in UOBM, relation hasSameHomeTownWith is symmetric and transitive, which creates cliques of connected constants; B/F always recomputes each changed clique, thus repeating most of the

'hard' work. Equality connects constants in cliques, which poses similar problems for B/F≈. For example, due to the constant c with |cπ | = 3930, deleting 5k facts in UOBM-100U results in only 961k (about 1.2% of |I ≈|) facts being added to set C in line 22, but these facts contribute to 73% of the derivations from the initial r-materialisation; thus, B/F≈ repeats in Algorithm 5 a substantial portion of the initial work.

On OpenCyc-L, Remat≈ already outperforms B/F≈ on updates of 1k triples, which was surprising since the former makes more derivations than the latter. Our investigation revealed that OpenCyc-L contains about 200 rules of the form 〈x, type, y〉 ← 〈x, Ri, y〉 that never fire during forward chaining; however, to check provability of 〈a, type,C〉, Algorithm 4 considers in line 32 each time each of the 200 rules. After removing all such 'idle' rules manually, B/F≈ and Remat≈ could update 1k tuples in roughly the same time. Further analysis revealed that the slowdown in B/F≈ occurs mainly in line 40: the condition is checked for 13.3M facts F, and these give rise to 139M facts in F π , each requiring an index lookup; the latter number is similar to the number of derivations in rematerialisation, which explains the slowdown. We believe one can check this condition more efficiently by using additional book-keeping.

5 Conclusion

This paper describes what we believe to be the first approach to incremental maintenance of datalog materialisation when the latter is computed using rewriting-a common optimisation used when programs contain equality. Our algorithm proved to be very effective, particularly on small updates.

In our future work, we shall aim to address the issues we identified in Section 4. For example, to optimise the check in line 40, we shall investigate ways of keeping track of how explicit facts are merged so that we can implement the test by iterating over the appropriate subset of E rather than over F π . Moreover, we believe we can considerably improve the efficiency of both the initial materialisation and the incremental updates by using specialised algorithms for rules that produce large cliques; hence, we shall identify common classes of 'hard' rules and then develop such specialised algorithms.

Acknowledgments

This work was funded by the EPSRC projects MaSI3 , Score!, and DBOnto, and the FP7 project Optique.