Combining Existential Rules and Transitivity: Next Steps

1 Introduction

Ontology-based data access (OBDA) is a new paradigm in data management, which exploits the semantic information provided by ontologies when querying data. Briefly, the notion of a database is replaced by that of a knowledge base (KB), composed of a dataset and an ontology. Existential rules, aka Datalog±, have been proposed to represent ontological knowledge in this context [Cal`ı et al., 2009; Baget et al., 2009; 2011b; Kr¨otzsch and Rudolph, 2011]. These rules are an extension of function-free first-order Horn rules (aka Datalog), that allows for existentially quantified variables in rule heads. The addition of existential quantification allows one to assert the existence of yet unknown entities and to reason about them, an essential feature of ontological languages, which is also at the core of description logics (DLs). Existential rules generalize the DLs most often considered in the OBDA setting, like the DL- Marie-Laure Mugnier Univ. Montpellier, Inria, CNRS Montpellier, France Swan Rocher Univ. Montpellier, Inria, CNRS Montpellier, France Lite and EL families [Calvanese et al., 2007; Baader, 2003; Lutz et al., 2009] and Horn DLs [Kr¨otzsch et al., 2007].

The fundamental decision problem related to OBDA is the following: is a Boolean conjunctive query (CQ) entailed from a KB? This problem has long been known to be undecidable for general existential rules (this follows e.g., from [Beeri and Vardi, 1981]). Consequently, a significant amount of research has been devoted to the issue of finding decidable subclasses with a good expressivity / tractability tradeoff. It has been observed that most exhibited decidable classes fulfill one of the three following properties [Baget et al., 2011a]: finiteness of a forward chaining mechanism known as the chase, which allows inferences to be materialized in the data (we call such rule sets finite expansion sets, fes); finiteness of query rewriting into a union of CQs, which allows to the rules to be compiled into the query (finite unification sets, fus); treelike shape of the possibly infinite chase, which allows one to finitely encode the result (bounded-treewidth sets, bts). The class of guarded rules [Cal`ı et al., 2008] is a well-known class satisfying the latter property.

Known decidable classes are able to express many useful properties of binary relations (e.g., inverses / symmetry) but most of them lack the ability to define a frequently required property, namely transitivity. This limits their applicability in key application areas like biology and medicine, for which transitivity of binary relations (especially the ubiquitous 'part of' relation) is an essential modelling construct. The importance of transitivity has long been acknowledged in the DL community [Horrocks and Sattler, 1999; Sattler, 2000], and many DLs support transitive binary relations. While adding transitivity to a DL often does not increase the complexity of CQ entailment (see [Eiter et al., 2009] for some exceptions), it is known to complicate the design of query answering procedures [Glimm et al., 2008; Eiter et al., 2012], due to the fact that it destroys the tree structure of the chase upon which DL reasoning algorithms typically rely. In contrast to the extensive literature on transitivity in DLs, rather little is known about the compatibility of transitivity with decidable classes of existential rules. A notable exception is the recent result of [Gottlob et al., 2013] on the incompatibility of transitivity with guarded rules, which holds even under strong syntactic restrictions (see Section 3).

In this paper, we investigate the issue of whether transitivity can be safely added to some well-known rule classes and provide three main contributions. First, we show that adding transitivity to one of the simplest fes and fus classes (namely aGRD) makes atomic CQ entailment undecidable, which clarifies the issue for fes classes (Theorem 1). Second, we investigate the impact of adding transitivity to linear rules, a natural subclass of guarded rules which generalizes the well-known description logic DL-LiteR. We introduce a query rewriting procedure that is sound and complete for all rule sets consisting of linear and transitivity rules (Theorem 2), and which is guaranteed to terminate for atomic CQs, and for arbitrary CQs if the rule set contains only unary and binary predicates or satisfies a certain safety condition, yielding decidability for these cases (Theorem 3). Third, based on a careful analysis of our algorithm, we establish tight bounds on the combined and data complexities of query entailment for the identified decidable cases. The obtained complexities are the lowest that could be expected, namely, NL in data complexity and PSPACE in combined.

Detailed proofs can be found in the accompanying technical report [Baget et al., 2015].

2 Preliminaries

A term is a variable or a constant. An atom is of the form p(t1, . . . , tk) where p is a predicate of arity k, and the ti are terms. We consider (unions of) Boolean conjunctive queries ((U)CQs), which are (disjunctions of) existentially closed conjunctions of atoms. Note however that all results can be extended to non-Boolean queries. A CQ is often viewed as the set of atoms. An atomic CQ is a CQ consisting of a single atom. A fact is an atom without variables. A fact base is a finite set of facts.

An existential rule (hereafter abbreviated to rule) R is a formula ∀⃗x∀⃗y(B[⃗x, ⃗y] → ∃⃗z H[⃗x, ⃗z]) where B and H are conjunctions of atoms, resp. called the body and the head of R. The variables ⃗z (resp. ⃗x), which occur only in H (resp. in B and in H) are called existential variables (resp. frontier variables). Hereafter, we omit quantifiers in rules and simply denote a rule by B → H. For example, p(x, y) → p(x, z) stands for ∀x∀y(p(x, y) → ∃z(p(x, z))). A knowledge base (KB) K = (F,R) consists of a fact base F and a finite set of rules R. The (atomic) CQ entailment problem consists in deciding whether K |= Q, where K is a KB viewed as a firstorder theory, Q is an (atomic) CQ, and |= denotes standard logical entailment.

Query rewriting relies on a unification operation between the query and a rule head. Care must be taken when handling existential variables: when a term t of the query is unified with an existential variable in a rule head, all atoms in which t occurs must also be part of the unification, otherwise the result is unsound. Thus, instead of unifying one query atom at a time, we have to unify subsets ("pieces") of the query, hence the notion of a piece-unifier defined next. A partition P of a set of terms is said to be admissible if no class of P contains two constants; a substitution σ can be obtained from P by selecting an element ei in each class Ci of P, with priority given to constants, and setting σ(t) = ei for all t ∈ Ci. A piece-unifier of a CQ Q with a rule R = B → H is a triple µ = (Q′ , H′ , Pµ), where Q′ ⊆ Q, H′ ⊆ H and Pµ

is an admissible partition on the terms of Q′ ∪H′ such that:

1. σ(H′ ) = σ(Q′ ), where σ is any substitution obtained from Pµ;
2. if a class Ci in Pµ contains an existential variable, then the other terms in Ci are variables from Q′ that do not occur in (Q\Q′ ).

We say that Q′ is a piece (and µ is a single-piece unifier) if there is no non-empty subset Q′′ of Q′ such that Pµ restricted to Q′′ satisfies Condition 2. From now on, we consider only single-piece unifiers, which we simply call unifiers. The (direct) rewriting of Q with R w.r.t. µ is σ(Q \ Q′ ) ∪ σ(B) where σ is a substitution obtained from Pµ. A rewriting of Q w.r.t. a set of rules R is a CQ obtained by a sequence Q = Q0, . . . ,Qn (n ≥ 0) where for all i > 0, Qi is a direct rewriting of Qi-1 with a rule fromR. For any fact base F, we have that F,R |= Q iff there is a rewriting Qn of Q w.r.t. R such that F |= Qn [K¨onig et al., 2013].

Example 1 Consider the rule R = h(x) → p(x, y) and CQ Q = q(u) ∧ p(u, v) ∧ p(w, v) ∧ r(w). If p(u, v) is unified with p(x, y), then v is unified with the existential variable y, hence p(w, v) has to be part of the unifier. The triple µ = ({p(u, v), p(w, v)}, {p(x, y)}, {{x, u, w}{v, y}} is a unifier. The direct rewriting of Q associated with the substitution σ = {x ↦→ u, w ↦→ u, y ↦→ v} is h(u) ∧ q(u) ∧ r(u).

We now define some important kinds of rule sets (see e.g., [Mugnier, 2011] for an overview). A model M of a KB K is called universal if for any CQ Q, M is a model of Q iff K |= Q. A rule set R is a finite expansion set (fes) if any KB (F, R) has a finite universal model. It is a bounded-treewidth set (bts) if any KB (F,R) has a (possibly infinite) universal model of bounded treewidth. It is a finite unification set (fus) if, for any CQ Q, there is a finite set S of rewritings of Q w.r.t. R such that for any fact base F, we have F, R |= Q iff there is Q′ ∈ S such that F |= Q′ .

A Datalog rule has no existential variables, hence Datalog rule sets are fes. Other kinds of fes rules are considered in the next section. A rule B → H is guarded if there is an atom in B that contains all the variables occurring in B. Guarded rules are bts. A linear rule has a body composed of a single atom and does not contain any constant. Linear rules are guarded, hence bts, moreover they are fus.

As a special case of Datalog rules, we have transitivity rules, of the form p(x, y) ∧ p(y, z) → p(x, z), which are not fus. A predicate is called transitive if it appears in a transitivity rule. If C is a class of rule sets, C+trans denotes the class obtained by adding transitivity rules to rule sets from C.

3 Combining fes / fus and Transitivity

A large hierarchy of fes classes is known (see e.g., [Cuenca Grau et al., 2013] for an overview). Beside Datalog, the simplest classes are weakly-acyclic (wa) sets, which prevent cyclic propagation of existential variables along predicate positions, and aGRD (acyclic Graph of Rule Dependencies) sets, which prevent cyclic dependencies between rules. Datalog is generalized by wa, while wa and aGRD are incomparable. Some classes generalize wa by a finer analysis of variable propagation (up to super-weakly acyclic (swa) sets). Most other fes classes generalize both wa and aGRD.

We show that aGRD+trans is undecidable even for atomic CQs. Since aGRD is both fes and fus, this negative result also transfers to fes+trans and fus+trans.

Theorem 1 Atomic CQ entailment over aGRD+trans KBs is undecidable, even with a single transitivity rule.

Proof: The proof is by reduction from atomic CQ entailment with general existential rules (which is known to be undecidable). Let R be a set of rules. We first translate R into an aGRD set of rules Ra . We consider the following new predicates: p (which will be the transitive predicate) and, for each rule Ri ∈ R, predicates ai and bi. Each rule Ri = Bi → Hi is translated into the two following rules:

• R1 i = Bi → ai(⃗x, z1) ∧ p(z1, z2) ∧ p(z2, z3) ∧ bi(z3)
• R2 i = ai(⃗x, z1) ∧ p(z1, z2) ∧ bi(z2) → Hi

where z1,z2 and z3 are existential variables and ⃗x are the variables in Bi.

Let Ra = {R1 i , R2 i | Ri ∈ R}, and let GRD(Ra ) be the graph of rule dependencies of Ra , defined as follows: the nodes of GRD(Ra ) are in bijection with Ra , and there is an edge from a node R1 to a node R2 if the rule R2 depends on the rule R1, i.e., if there is a piece-unifier of the body of R2 (seen as a CQ) with the head of R1.

We check that for any Ri ∈ R, R1 i has no outgoing edge and R2 i has no incoming edge (indeed the zj are existential variables). Hence, in GRD(Ra ) all (directed) paths are of length less or equal to one. It follows that GRD(Ra ) has no cycle, i.e., Ra is aGRD.

Let Rt be the rule stating that p is transitive. Let R′ = Ra ∪ {Rt}. The idea is that Rt allows to "connect" rules in Ra that correspond to the same rule in R. For any fact base F (on the original vocabulary), for any sequence of rule applications from F using rules in R, one can build a sequence of rule applications from F using rules fromR′ , and reciprocally, such that both sequences produce the same fact base (restricted to atoms on the original vocabulary). Hence, for any F and Q (on the original vocabulary), we have that F,R |= Q iff F,R′ |= Q. ✷

Corollary 1 Atomic CQ entailment over fus+trans or fes+trans KBs is undecidable.

Most known fes classes that do not generalize aGRD range between Datalog and swa (inclusive). It can be easily checked that any swa set of rules remains swa when transitivity rules are added (and this is actually true for all known classes between Datalog and swa).

Proposition 1 The classes swa and swa+trans coincide. Hence, swa+trans is decidable.

Proof: It suffices to note that the addition of transitivity rules does not create new edges in the 'SWA position graph' from [Cuenca Grau et al., 2013]. ✷

It follows that the effect of transitivity on the currently known fes landscape is now quite clear, which is not the case for fus classes. In the following, we focus on a well-known fus class, namely linear rules. We show by means of a query rewriting procedure that query entailment over linear+trans KBs is decidable in the case of atomic CQs, as well as for general CQs if we place a minor safety condition on the rule set. Such an outcome was not obvious in the light of existing results. Indeed, atomic CQ entailment over guarded+trans rules was recently shown undecidable, even when restricted to rule sets that belong to the two-variable fragment, use only unary and binary predicates, and contain only two transitive predicates [Gottlob et al., 2013]. Moreover, inclusion dependencies (a subclass of linear rules) and functional dependencies (a kind of rule known to destroy tree structures, as do transitivity rules) are known to be incompatible [Chandra and Vardi, 1985].

4 Linear Rules and Transitivity

To obtain finite representations of sets of rewritings involving transitive predicates, we define a framework based on the notion of pattern.

4.1 Framework

To each transitive predicate we assign a pattern name. Each pattern name has an associated pattern definition P := a1| . . . |ak, where each ai is an atom that contains the special variables #1 and #2. A pattern is either a standard pattern P [t1, t2] or a repeatable pattern P +[t1, t2], where P is a pattern name and t1 and t2 are terms. A union of patterned conjunctive queries (UPCQ) is a pair (Q, P), where Q is a disjunction of conjunctions of atoms and patterns, and P is a set of pattern definitions that gives a unique definition to each pattern name occurring in Q. A patterned conjunctive query (PCQ) Q is a UPCQ without disjunction. For the sake of simplicity, we will often denote a (U)PCQ by its first component Q, leaving the pattern definitions implicit.

An instantiation T of a UPCQ (Q, P) is a node-labelled tree that satisfies the following conditions:

• the root of T is labelled by Q ∈ Q;
• the children of the root are labelled by the patterns and atoms occurring in Q;
• each node that is labelled by a repeatable pattern P +[t1, t2] may be expanded into k ≥ 1 children labelled respectively by P[t1, x1], P[x1, x2], . . ., P[xk-1, t2], where the xi are fresh variables;
• each node labelled by a standard pattern P[t1, t2] may be expanded into a single child whose label is obtained from an atom a in the pattern definition of P in P by substituting #1 (resp. #2) by t1 (resp. t2), and freshly renaming the other variables.

For brevity, we will often refer to nodes in an instantiation using their labels.

The instance associated with an instantiation is the PCQ obtained by taking the conjunction of the labels of its leaves. An instance of a UPCQ is an instance associated with one of its instantiations. An instance is called full if it does not contain any pattern, and we denote by full(Q, P) the set of full instances of (Q, P).

Example 2 Let (Q, P) be a PCQ, where Q = P + 1 [a, z] ∧ P + 2 [z, b] ∧ s1(a, b) and P contains the pattern definitions: P1 := p1(#1,#2)|s2(#1, y,#2) and P2 := p2(#1,#2)| s2(#2, y, #1).

Two instantiations of Q are displayed in Figure 1. The smaller instantiation (within the dotted lines) gives rise to the (non-full) instance Q1 = P1[a, z] ∧ P2[z, x1] ∧ P2[x1, b] ∧ s1(a, b). By expanding the three nodes labelled by patterns according to the definitions in P, we may obtain the larger instantation (occupying the entire figure), whose associated instance Q2 = s2(a, y0, z)∧s2(x1, y1, z)∧p2(x1, b)∧s1(a, b) is a full instance for (Q, P).

A UPCQ (Q, P) can be translated into a set of Datalog rules ΠP and a UCQ QQ as follows. For each definition P := a1(⃗t1)| . . . |ak(⃗tk) in P, we create the transitivity rule p+(x, y) ∧ p+(y, z) → p+(x, z) and the rules ai(⃗ti) → p+(#1,#2) (1 ≤ i ≤ k). The UCQ QQ is obtained from Q by replacing each repeatable pattern P +[t1, t2] by the atom p+(t1, t2). Observe that ΠP is non-recursive except for the transitivity rules. The next proposition states that (ΠP,QQ) can be seen as a finite representation of the set of full instances of (Q, P).

Proposition 2 Let F be a fact base and (Q, P) be a UPCQ. Then F, ΠP |= QQ iff F |= Q for some Q ∈ full(Q, P).

A unifier µ = (Q′ ,H, Pu) of a PCQ is a unifier of one of its (possibly non-full) instances such that Q′ is a set of (usual) atoms. We distinguish two types of unifiers (internal and external), defined next.

Let T be an instantiation, Q be its associated instance, and µ = (Q′ ,H, Pu) be a unifier of Q. Assume T contains a repeatable pattern P +[t1, t2] that is expanded into P[u0, u1], . . . , P[uk, uk+1], where u0 = t1 and uk+1 = t2. We call P[ui, ui+1] relevant for µ if it is expanded into an atom from Q′ . Because we consider only single-piece unifiers (cf. Sec. 2), it follows that if such relevant patterns exist, they form a sequence P [ui, ui+1],P [ui+1, ui+2],. . . , P [uj-1, uj ]. Terms ui and uj are called external to P +[t1, t2] w.r.t. µ; the other terms occurring in the sequence are called internal. The unifier µ is said to be internal if all atoms fromQ′ are expanded from a single repeatable pattern, and no external terms are unified together or with an existential variable; otherwise µ is called external.

Example 3 Consider Q2 from Example 2 and the rules R1 = s1(x′ , y′ ) → p2(x′ , y′ ) and R2 = s1(x′ , y′ ) → s2(x′ , y′ , z′ ). The unifier of Q2 with R1 that unifies p2(x1, b)

with p2(x′ , y′ ) is internal. The unifier of Q2 with R2 that unifies {s2(a, y0, z), s2(x1, y1, z)} with s2(x′ , y′ , z′ ) is external because it involves two repeatable patterns.

4.2 Overview of the Algorithm

Our query rewriting algorithm takes as input a CQ Q and a set of rules R = RL ∪RT , with RL a set of linear rules and RT a set of transitivity rules, and produces a finite set of Datalog rules and a (possibly infinite) set of CQs. The main steps of the algorithm are outlined below.

Step 1 For each predicate p that appears in RT , create a pattern definition P := p(#1,#2), where P is a fresh pattern name. Call the resulting set of definitions P0.

Step 2 Let R+L be the result of considering all of the rule bodies in RL and replacing every body atom p(t1, t2) such that p is a transitive predicate by the repeatable pattern P +[t1, t2].

Step 3 (Internal rewriting) Initialize P to P0 and repeat the following operation until fixpoint: select a pattern definition P ∈ P and a rule R ∈ R+L and compute the direct rewriting of P w.r.t. P and R.

Step 4 Replace in Q all atoms p(t1, t2) such that p is a transitive predicate by the repeatable pattern P +[t1, t2], and denote the result by Q+.

Step 5 (External rewriting) Initialize Q to {Q+} and repeat the following operation until fixpoint: choose Qi ∈ Q, compute a direct rewriting of Qi w.r.t. P and a rule from R+L , and add the result to Q (except if it is isomorphic to some Qj ∈ Q).

Step 6 Let ΠP be the Datalog translation of P, and let QQ be the (possibly infinite) set of CQs obtained by replacing each repeatable pattern P +[t1, t2] in Q by p+(t1, t2).

The rewriting process in Step 3 is always guaranteed to terminate, and in Section 6, we propose a modification to Step 5 that ensures termination and formulate sufficient conditions that preserve completeness. When QQ is finite (i.e., it is a UCQ), it can be evaluated over the fact base saturated by ΠP, or alternatively, translated into a set of Datalog rules, which can be combined with ΠP and passed to a Datalog engine for evaluation. Observe that the construction of ΠP is queryindependent and can be executed as a preprocessing step.

5 Rewriting Steps in Detail

A PCQ that contains a repeatable pattern has an infinite number of instances. Instead of considering all instances of a PCQ, we consider a finite set of 'instances of interest' for a given rule. Such instances will be used for both the internal and external rewriting steps.

Instances of interest Consider a PCQ (Q, P) and a rule R ∈ R+L with head predicate p. The instantiations of interest of (Q, P) w.r.t. R are constructed as follows. For each repeatable pattern P + i [t1, t2] in Q, let ai1 , . . . , aini be the atoms in the definition of Pi with predicate p. If ni > 0, then expand P + i [t1, t2] into k standard patterns, where 0 < k ≤ min(arity(p), ni) + 2, and expand each of these standard patterns in turn into some aiℓ . An instance of interest is the instance associated with an instantiation of interest.

Example 4 Reconsider Q, Q2 and R2 from Examples 2 and 3. Q2 is not an instance of interest of Q w.r.t. R2 since P2[x1, b] is expanded into p(#1, #2) whereas the head predicate of R2 is s2. If we expand P2[x1, b] with s2(#2, y,#1) instead, we obtain the instance of interest Q3 = s2(a, y0, z)∧ s2(x1, y1, z) ∧ s2(b, y2, x1) ∧ s1(a, b).

We next show that the set of unifiers computed on the instances of interest of a PCQ 'captures' the set of unifiers computed on all of its instances.

Proposition 3 Let (Q, P) be a PCQ and R ∈ R+L . For every instance Q of (Q, P) and unifier µ of Q with R, there exist an instance of interest Q′ of (Q, P) w.r.t. R and a unifier µ′ of Q′ with R such that µ′ is more general 1 than µ.

5.1 Internal Rewriting

Rewriting w.r.t. internal unifiers is performed 'inside' a repeatable pattern, independently of the other patterns and atoms in the query. We will therefore handle this kind of rewriting in a query-independent manner by updating the pattern definitions.

To find all internal unifiers between instances under a repeatable pattern P +[t1, t2] and a rule head H = p(. . .), one may think that it is sufficient to consider each atom ai in P's definition and check if there is an internal unifier of ai with H. Indeed, this suffices when predicates are binary: in an internal unifier, t1 and t2 are unified with distinct variables, which cannot be existential; thus, the terms in H are frontier variables, and a piece must consist of a single atom. If the arity of p is greater than 2, the other variables can be existential, so it may be possible to unify a path of atoms from P's definition, but not a single such atom (see next example).

Example 5 Let R = s(x, y) → r(z1, x, z2, y) and P := r(#2,#1, x0, x1)| r(#1, x2,#2, x3)| r(x4, x5,#1,#2). There is no internal unifier of an atom in P's definition with H = r(z1, x, z2, y). However, if we expand P +[t1, t2] into a path P[t1, y0]P[y0, y1]P[y1, t2], then expand the ith pattern of this path into the ith atom in P's definition, the resulting instance can be unified with H by an internal unifier (with the partition {{z1, y0, x4}, {x, t1, x2, x5}, {z2, x0, y1}, {y, x1, x3, t2}}).

Fortunately, we can bound the length of paths to be considered using both the arity of p and the number of atoms with predicate p in P's definition, allowing us to use instances of interest introduced earlier.

A direct rewriting P′ of a set of pattern definitions P w.r.t. a pattern name P and a rule R = B → H ∈ R+L is the set of pattern definitions obtained from P by updating P's definition as follows. We consider the PCQ (Q = P +[x, y], P). We select an instance of interest Q of Q w.r.t. R, an internal unifier µ of Q with H, and a substitution σ associated with µ that preserves the external terms. Let B′ be obtained from

1 Consider unifiers µ = (Q, H, Pµ) and µ′ = (Q′ , H, Pµ′ ), and let σ (resp. σ′ ) be a substitution associated with Pµ (resp. Pµ′ ). We say that µ′ is more general than µ if there is a substitution h from σ′ (Q′ ) to σ(Q) such that h(σ′ (Q′ )) ⊆ σ(Q) (i.e., h is a homomorphism from σ′ (Q′ ) to σ(Q)), and for all terms x and y in Q′ ∪H, if σ′ (x) = σ′ (y) then σ(h(x)) = σ(h(y)).

σ(B) by substituting the first (resp. second) external term by #1 (resp. #2). If B′ is an atom, we add it to P's definition. Otherwise, B′ is a repeatable pattern of the form S+[#1, #2] or S+[#2,#1]. Let f be a bijection on {#1,#2}: if B′ is of the formS+[#1,#2], f is the identity, otherwise f permutes #1 and #2. For all si in the definition of S, we add f(si) to P 's definition.

Note that the addition of an atom to a pattern definition is up to isomorphism (with #1 and #2 treated as distinguished variables, i.e., #1 and #2 are mapped to themselves).

Example 6 Reconsider R, µ, and the definition of P from Example 5. Performing a direct rewriting w.r.t. P using R and µ results in adding the atom s(#1, #2) to P 's definition.

Proposition 4 Let (Q, P) be a PCQ where P +[t1, t2] occurs and R ∈ R+L . For any instance Q of (Q, P), any classical direct rewriting Q′ of Q with R w.r.t. to a unifier internal to P +[t1, t2], and any Q′ ∈ full(Q′ , P), there exists a direct rewriting P′ of P w.r.t. P and R such that (Q, P′ ) has a full instance that is isomorphic to Q′ .

5.2 External Rewriting

Let (Q, P) be a PCQ, R ∈ R+L , T be an instantiation of interest of (Q, P) w.r.t. R, Q be the instance associated with T, and µ = (Q′ ,H, P) be an external unifier of Q with R. From this, several direct rewritings of Q w.r.t. P and R can be built. First, we mark all leaves in T that either have the root as parent or are labelled by an atom in Q′ , and we restrict T to branches leading to a marked leaf. Then, we consider each instantiation Ti that can be obtained fromQ as follows. Replace each repeatable pattern P +[t1, t2] that has k > 0 children in T by one of the following:

where X[v1, v2] is a sequence P[v1, y1], P[y1, y2], . . . , P [yk-1, v2]. Let Qi be the instance associated with Ti.

If P[x′ , y′ ] in T has child a(⃗t), expand in Ti the corresponding P [x, y] into a(ρ(⃗t)) where ρ = {x′ ↦→ x, y′ ↦→ y}. If µ′ = (ρ(Q′ ),H, ρ(P)) is still a unifier of Qi with H, we say that Qi is a minimally-unifiable instance of Qw.r.t. µ. In this case, Q′i = µ′ (Qi) \ µ′ (H) ∪ µ′ (B) is a direct rewriting of Q w.r.t. P and R.

Example 7 Reconsider Q3 and R2, and let µ = ({s2(a, y0, z), s2(x1, y1, z)}, H2, {{a, x1, x′}, {y0, y1, y′}, {z, z′}}). First, we consider the instantiation that generated Q3, and we remove the node labelled P2[x1, b] and its child s2(b, y2, x1), since the latter atom is not involved in µ. Next will replace the repeatable pattern P + 1 [a, z] (resp. P + 2 [z, b]) using one of the four cases detailed above, and we check whether µ′ (obtained from µ) is still a unifier. We obtain in this manner the following minimally-unifiable instances: Q1 = P + 1 [a, x2]∧ s2(x2, y0, z)∧ s2(x1, y1, z)∧ P + 2 [x1, b]∧ s1(a, b), and Q2 = s2(a, y0, z) ∧ s2(x1, y1, z) ∧ P + 2 [x1, b] ∧ s1(a, b). Finally, we rewrite Q1 and Q2

into: Q′1 = P + 1 [a, x′ ] ∧ s1(x′ , y′ )∧ P + 2 [x′ , b]∧ s1(a, b) and Q′2 = s1(a, y′ )∧ P + 2 [a, b]∧ s1(a, b).

Proposition 5 Let (Q, P) be a PCQ and R ∈ R+L . For every Q ∈ full(Q, P) and every classical direct rewriting Q′ of Q with R w.r.t. an external unifier, there is a direct rewriting Q′ of Q w.r.t. P and R that has an instance isomorphic to Q′ .

6 Termination and Correctness

To establish the correctness of the query rewriting algorithm, we utilize Propositions 2, 4 and 5.

Theorem 2 Let Q be a CQ, (F,R) be a linear+trans KB, and (ΠP,QQ) be the (possibly infinite) output of the algorithm. Then: F,R |= Q iff F,ΠP |= Q′ for some Q′ ∈ QQ.

Regarding termination, we observe that Step 3 (internal rewriting) must halt since every direct rewriting step adds a new atom (using a predicate from R+L ) to a pattern definition, and there are finitely many such atoms, up to isomorphism.

By contrast, Step 5 (external rewriting) need not halt, as the rewritings may grow unboundedly in size. Thus, to ensure termination, we will modify Step 5 to exclude direct rewritings that increase rewriting size. Specifically, we identify the following 'problematic' minimally-unifiable instances:

• Q′ is composed of atoms expanded from a single pattern P +[t1, t2], µ′ (t1) = µ′ (t2), and P +[t1, t2] is replaced as in case (i), (ii) or (iii).
• Q′ is obtained from the expansion of repeatable patterns, a term t of Q is unified with an existential variable of the head of the rule, t appears only in repeatable patterns of form P + i [ti, t] (resp. P + i [t, ti]), and all these repeatable patterns are rewritten as in case (ii) P + i [ti, t′i ] ∧X[t′i , t] (resp. as in case (iii) X[t, t′i ] ∧ P + i [t′i , ti]).

We will call a direct rewriting excluded if it is based on such a minimally-unifiable instance; otherwise, it is non-excluded.

Example 8 The rewriting Q′1 from Example 7 is excluded because it is obtained from the minimally-unifiable instance Q1 in which the repeatable patterns P + 1 [a, z] is expanded as in case (ii) and P + 2 [z, b] as in case (iii), and z is unified with the existential variable z′ .

Proposition 6 Let (Q, P) be a PCQ and R ∈ R+L . If Q′ is a non-excluded direct rewriting of Q with R, then |Q′ | ≤ |Q|.

Let us consider the 'modified query rewriting algorithm' that is obtained by only performing non-excluded direct rewritings in Step 5. This modification ensures termination but may comprise completeness. However, we can show that the modified algorithm is complete in the following key cases: when the CQ is atomic, when there is no specialization of a transitive predicate, or when all predicates have arity at most two. By further analyzing the latter case, we can formulate a safety condition, defined next, that guarantees completeness for a much wider class of rule sets.

Safe rule sets We begin by defining a specialization relationship between predicates. A predicate q is a direct specialization of a binary predicate p on positions {⃗i,⃗j} (⃗i ̸= ∅,⃗j ̸= ∅) if there is a rule of the form q(⃗u) → p(x, y) such that ⃗i

(resp. ⃗j) contains those positions of ⃗u that contain the term x (resp. y). It is a specialization of p on positions {⃗i,⃗j} if (a) it is a direct specialization of p on positions {⃗i,⃗j}, or (b) there is a rule of the form q(⃗u) → r(⃗v) such that r(⃗v) is a specialization of p on positions {⃗k,⃗l} and the terms occurring in positions {⃗k,⃗l} of ⃗v occur in positions {⃗i,⃗j} of ⃗u with⃗i ̸= ∅ and⃗j ̸= ∅. We say that q is a pseudo-transitive predicate if it is a specialization of at least one transitive predicate.

We call a linear+trans rule set safe if it satisfies the following safety condition: for every pseudo-transitive predicate q, there exists a pair of positions {i, j} with i ̸= j such that for all transitive predicates p of which q is a specialization on positions {⃗i,⃗j}, either i ∈⃗i and j ∈⃗j, or i ∈⃗j and j ∈⃗i.

Note that if we consider binary predicates, the safety condition is always fulfilled. Then, specializations correspond exactly to the subroles considered in DLs.

Example 9 Let R1 = s1(x, x, y) → p1(x, y), R2 = s2(x, y, z) → p2(x, y), R3 = s1(x, y, z) → s2(z, x, y), and p1 and p2 be two transitive predicates.

The following specializations have to be considered: s1 is a direct specialization of p1 on positions {{1, 2}, {3}}, s2 is a direct specialization of p2 on positions {{1}, {2}}, s1 is a specialization of p2 on positions {{3}, {1}}. We then have two pseudo-transitive predicates: s1 and s2. By choosing the pair {1, 3} for s1 and {1, 2} for s2, we observe that {R1,R2,R3} satisfies the safety condition.

If we replace R3 by R4 = s1(x, y, z) → s2(x, y, z), s1 is a specialization of p2 on positions {{1}, {2}}, and {R1,R2,R4} is not safe.

Theorem 3 The modified query rewriting algorithm halts. Moreover, Theorem 2 (soundness and completeness) holds for the modified algorithm if either the input CQ is atomic, or the input rule set is safe.

7 Complexity

A careful analysis of our query rewriting algorithm allows us to pinpoint the worst-case complexity of atomic CQ entailment over linear+trans KBs, and general CQ entailment over safe linear+trans KBs. As usual, we consider two complexity measures: combined complexity (measured in terms of the size of the whole input), and data complexity (measured in terms of the size of the fact base). The latter is often considered more relevant since the fact base is typically significantly larger than the rest of the input.

With regards to data complexity, we show completeness for NL (non-deterministic logarithmic space), which is the same complexity as in the presence of transitivity rules alone.

Theorem 4 Both (i) atomic CQ entailment over linear+trans KBs and (ii) CQ entailment over safe linear+trans KBs are NL-complete in data complexity.

Regarding combined complexity, we show that the addition of transitivity rules does not increase the complexity of query entailment for the two considered cases.

Theorem 5 Both (i) atomic CQ entailment over linear+trans KBs and (ii) CQ entailment over safe linear+trans KBs are PSPACE-complete in combined complexity.

8 Conclusion

In this paper, we made some steps towards a better understanding of the interaction between transitivity and decidable classes of existential rules. We obtained an undecidability result for aGRD+trans, hence for fes+trans and fus+trans. More positively, we established decidability (with the lowest possible complexity) of atomic CQ entailment over linear+trans KBs and general CQ entailment for safe linear+trans rule sets. The safety condition was introduced to ensure termination of the rewriting mechanism when predicates of arity more than two are considered (rule sets which use only unary and binary predicates are trivially safe). We believe the condition can be removed with a much more involved termination proof.

In future work, we plan to explore the effect of transitivity on decidable rule classes that are incomparable with linear rules, namely frontier-one rules, a bts class that has close connections to Horn DLs, and two fus classes: domain-restricted and sticky rule sets [Baget et al., 2011a; Cal`ı et al., 2010].

Acknowledgements

This work was supported by ANR project PAGODA (contract ANR 12 JS02 007 01).