We consider the existential rule framework, which generalizes Horn description logics. We study and compare several boundedness notions in this framework. Our main result states that (strongly-) bounded rules are exactly those at the intersection of two well-known abstract classes of existential rules, namely fes (finite expansion sets, which ensure the finiteness of the core chase) and fus (finite unification sets, which correspond to UCQ-rewritable rules).
Existential rules [
As OMQA can be directly implemented on top of relational database systems, many research efforts have been devoted to make the paradigm efficient. At the core of the techniques developed for existential rules, and to some extent for Horn description logics, we find the two classical paradigms for processing rules, namely forward chaining and backward chaining. In the OMQA setting, both approaches are recast as ways of reducing the problem to a classical database query answering problem, by embedding the rules into the facts or into the query. Forward chaining is decomposed into a materialization step (applying the rules to the data, hence materializing inferences into the data) followed by the evaluation of the query against the enriched database. Backward chaining is decomposed into a query rewriting step (rewriting the query using the rules) followed by the evaluation of the rewritten query against the database, thereby leaving the data untouched.
Both approaches rely on a fixpoint operator to cope with rule semantics. Indeed,
materialization should continue until the point where only redundant facts are added
to the dataset, while rewriting should continue until the point where only redundant
queries are added to the rewriting set. It is understood that both processes may not
terminate since entailment with existential rules is undecidable (e.g., [
To fes (resp. fus) rules is naturally associated a finite breadth-first materialization (resp. query rewriting) process, whose maximal number of steps generally depends not only on the set of rules but also on the data (resp. on the input query). In contrast, bounded rules are exactly those rules that can be evaluated without a fixpoint operator. A set of rules is said to be bounded if breadth-first materialization computes all consequences from a knowledge base (composed of a fact base and the rules) in a predefined number of steps k. More precisely, there is k independent from any fact base, such that the materialization of any fact base at step k0 > k is equivalent to that obtained at step k. As relational database systems may lack a fixpoint operator (see for example MySQL), bounded rules form an interesting intersection point between databases and ontologies, because they can be seamlessly evaluated on any relational system, which is not the case in general.
The goal of this work is to further investigate the properties of bounded existential rules, in particular the precise relationships between fes, fus and bounded sets of rules.
Our contributions are more precisely the following:
1. We first define a breadth-first query rewriting technique which is precisely the dual
of breadth-first materialization. Let K = (F; R) be any knowledge base, where F
is a fact base and R a set of existential rules, and let q be a (Boolean) conjunctive
query. From earlier work on existential rules, we know that K entails q iff there is k
(depending on R and F ) such that F k, the saturation of F at step k, entails q (e.g.,
[
We consider a first-order setting with constants but no other function symbols. A term is either a constant or a variable. In the examples we will denote constants by letters at the beginning of the alphabet (a, b, ...,) and variables by letters at the end of the alphabet (v, w, x, y, z). An atom is of the form p(t1; : : : ; tk) where p is a predicate of arity k and the ti are terms. Given an atom or set of atoms A, vars(A), consts(A) and terms(A) denote its set of variables, constants and terms, respectively. We denote by j= the classical logical consequence and by the logical equivalence. Given two sets of atoms A and A0, a homomorphism h from A to A0 is a substitution of vars(A) by terms(A0) such that h(A) A0. If there is a homomorphism h from A to A0, we say that A maps to A0 (by h), which is also denoted by A A0. It is convenient to extend any substitution s to unchanged terms (we set s(t) = t for all considered constants and unchanged variables).
A fact is an existentially closed conjunctions of atoms. We denote by F a fact base, that is a set of facts. Since a conjunction of facts is equivalent to a single fact, we also see a fact base as an existentially closed conjunction of atoms. A Boolean conjunctive query (in short CQ) is also an existentially closed conjunction of atoms. Next, fact bases and conjunctive queries will be seen as sets of atoms. The answer to a CQ q in a fact base F is true iff F j= q. It is well known that F j= q iff q F . A union of conjunctive queries (UCQ) Q = q1 _ q2 : : : _ qn is seen as a set of CQs Q = fq1; : : : ; qng. The answer to Q in F is true iff F j= Q, i.e., F j= qi for some qi 2 Q.
An existential rule r = 8x; y(B [x; y] ! 9z H [x; z]) is a closed formula where
B is a conjunction of atoms constituting the body of the rule, H is a conjunction of
atoms for the head of the rule, x and y are sets of universally quantified variables, and
z is the set of existentially quantified variables of the rule. The variables in x, i.e., those
shared by B and H , are called the frontier variables of the rule. In the following we will
refer to a rule as a pair of sets of atoms (B ; H ), interpreting their common variables as
the frontier. In the examples, we will use the simplified notation B ! H , for instance
the rule 8x(q(x) ! 9y (p(x; y) ^ q(y))) will be written q(x) ! p(x; y); q(y). A set
of rules is denoted by R. We implicitly assume that all rules employ disjoint sets of
variables. A knowledge base (KB) K = (F; R) is a pair where F is a fact base and R is
a set of rules. The conjunctive query entailment problem consists in deciding for given
KB K and CQ q whether K j= q (where K is seen as the first order theory associated
with F [ R). It has long been shown that this problem is undecidable (this follows e.g.,
from [
A rule r = (B ; H ) is applicable to a fact base F if there is a homomorphism h such that h(B ) F . The application of r to F with respect to a homomorphism h is denoted by (F; r; h) and defined as (F; r; h) = F [ hsafe(H ) where hsafe is a safe extension of h to H , i.e., it substitutes existential variables from H with fresh variables (not used elsewhere). It holds that F; R j= q iff there is a fact base F 0 derived from F with rules in R, 1 such that F 0 j= q. 1 i.e., F 0 is obtained by a sequence of fact bases F (= F0); F1; : : : ; Fk(= F 0) such that, for all i > 0, Fi = (Fi 1; ri; h) with ri 2 R and h a homomorphism from the body of ri to Fi 1.
We now define fact materialization by (breadth-first) forward chaining, a useful tool, also known as saturation or (breadth-first) chase. 2 The one-step saturation of F with R, denoted by (F; R), is defined as (F; R) = F [(r;h) hsafe(H) for all r = (B; H) 2 R and h homomorphism from B to F . The k-saturation of F with R, denoted by k(F; R), is inductively defined as follows: 0(F; R) = F and, for any k > 0, k(F; R) = ( k 1(F; R); R).
Next, when R is fixed, we will denote the set k(F; R) by F k. Saturation is sound
and complete, i.e., for all F , R and Q, F; R j= Q iff F k j= Q for some positive
integer k (see e.g., [
Example 1 (fes). Let K = (F; R) with F = fp(a; b)g and R = fr : p(x; y) ! p(y; z); p(z; y)g. Then F 0 = F , F 1 = F [ fp(b; z0); p(z0; b)g, F 2 = F 1 [ fp(z0; z1); p(z1; z0) ; p(b; z2); p(z2; b) ; p(b; z00); p(z00; b)g (the rule applications corresponding to homomorphisms already found at the preceding step are written in gray font, next we will omit them). We have F 2 F 1 (note that there is no k such that F k = F k+1, even by considering only new homomorphisms at each step, which shows the importance of checking equivalence and not only equality). Actually it holds that F 2 F 1 for any F , hence R is fes (and even bounded, see Sect. 4). Let us consider R0 = fr : p(x; y) ! p(y; z)g. Then F 0 = F , F 1 = F [ fp(b; z0)g, F 2 = F 1 [ fp(z0; z1); p(b; z2)g and so on. There is no k such that F k F k+1, hence R0 is not fes.
Backward chaining is a dual approach to deciding conjunctive query entailment,
which involves rewriting the input query using the rules. The key operation is
unification between (a subset of) a query and (a subset of) a rule head, which requires particular
care due to the presence of existential variables in the rules. For this reason, we use the
notion of a piece-unifier (introduced in [
Definition 1 (Piece Unifier) Let q be a query and r = (B ; H ) a rule. A piece-unifier of q with r is a triple = (q0; H 0; u) where q0 6= ;, q0 q, H 0 H , and u is a substitution of T = terms(q0 [ H 0) by T such that (i) u(q0) = u(H 0) and (ii) for all existential variable x 2 vars(H 0) and t 2 T , with t 6= x, if u(x) = u(t), then t is a non-separating variable from q0.
Given a CQ q, a rule r = (B ; H ) and a piece-unifier = (q0; H 0; u) the direct rewriting of q with r and , denoted by (q; r; ), is the CQ usafe(B ) [ u(q n q0), where usafe is a safe extension of u to B substituting variables in vars(B ) n vars(H0) with fresh variables. 2 Several chase variants have been defined, see the last section. Example 2 (Piece Unifier). Let r = r(x) ! p(x; y) and q1 = fp(w; v); s(v)g. There is no piece-unifier of q1 with r since, with q10 = fp(w; v)g, v is a separating variable of q10, hence cannot be unified with the existential variable y. Let q2 = fs(z); p(z; v); p(w; v); t(w)g. The triple = (q0; H0; u) with q0 = fp(z; v); p(w; v)g, H0 = fp(x; y)g and u = fx 7! z; y 7! v; w 7! zg is a piece-unifier of q2 with r, which yields the direct rewriting fr(z); s(z); t(z)g.
It holds that F; R j= q iff there is a rewriting q0 of q with rules in R, 3 such that
F j= q0. A set of rewritings Q of q (with R) is said to be sound and complete if for any
F it holds that F; R j= q iff there is q0 2 Q such that F j= q0. When Q is finite it can be
seen as a UCQ, hence the previous condition can then be recast as follows: F; R j= q
iff F j= Q. The set R is said to be fus (finite unification set) if for any q, there is a finite
sound and complete set of rewritings of q with R [
Similarly in spirit to saturation, one can consider breadth-first query rewriting: starting from the UCQ Q = fqg, at each step we compute all the direct rewritings of CQs in the current UCQ. Formally: the one-step rewriting of a UCQ Q with R is (Q; R) = Q [(q;r; ) f (q; r; )g where q 2 Q, r 2 R and is a piece-unifier of q with r. Then, the (breadth-first) k-rewriting of Q with R, denoted by k(Q; R), is inductively defined as follows: 0(Q; R) = Q, and for all k > 0, k(Q; R) = ( k 1(Q; R); R).
It holds that F; R j= q iff F j= k(fqg; R) for some positive integer k (follows
from [
Let r = p(x; y); p(y; z) ! p(z; t). Let q0 = fp(v; a)g, where a is a constant: since t is an existential variable, there is no piece-unifier of q0 with r.
Let q00 = fp(a; v)g.
1(fq00g; frg) = fq00g [ ffp(x0; y0); p(y0; a)gg; 2(fq00g; frg) = 1(fq00g; frg) [ ffp(x00; y00); p(y00; a)gg, where the last CQ corresponds to the piece-unifier already found in the preceding step. Hence, 2(fq00g; frg) = 1(fq00g; frg) if we restrict the computation to new piece-unifiers.
Finally, let q = fp(v; w)g.
1(fqg; frg) = fqg [ fq1 = fp(x0; y0); p(y0; v)gg.
2(fqg; frg) = 1(fqg; frg) [ ffp(x1; y1); p(y1; y0); p(x0; y0)gg (we consider only new piece-unifiers). Since existential variables can only be unified with non-separating variables, there is only one new piece-unifier (fp(x0; v)g; fp(z; t)g; fz 7! y0; t 7! vg), which yields q1.
3(fqg; frg) = 2(fqg; frg) [ ffp(x2; y2); p(y2; y1); p(x1; y1)gg, where the new the
piece-unifier is (fp(x0; y0); p(y1; y0)g; fp(z; t)g; fz 7! y1; x0 7! y1; t 7! y0g). And
so on. There is no k such that k = k+1 (up to bijective variable renaming), however
any UCQ i is equivalent to q. As these examples suggest it, frg is indeed fus.
3 i.e., q0 is obtained by a sequence of direct rewritings q(= q0); q1; : : : ; qk(= q0) such that, for
all i > 0, qi = (qi 1; ri; ) with ri 2 R and a piece-unifier of qi 1 with ri.
4 The breadth-first rewriting algorithm in [
Note that there is k such that F j= k(fqg; R) if and only if there is k0 such that k0 (F; R) j= q. However, the above breadth-first rewriting is not exactly the dual of breadth-first saturation, in the sense that (F; R) j= q does not imply F j= (fqg; R). In other words, a single step of breadth-first rewriting is not able to “simulate” a step of saturation. Let us illustrate this observation with a simple example.
Example 4 (Saturation vs rewriting step). Let K = (F; R) with F = fp0(a); q0(a)g and R = frp : p0(x) ! p1(x); rq : q0(x) ! q1(x)g. Let q = fp1(u); q1(u)g. A single saturation step (F; R) = fp0(a); q0(a); p1(a); q1(a)g allows to entail q. However, a single rewriting step 1(fqg; R) = ffp1(u); q1(u)g; fp0(u); q1(u)g; fp1(u); q0(u)gg does not allow to prove that K j= q, i.e., F 6j= 1(fqg; R). The trouble is that each direct rewriting is performed with respect to a single rule, hence the desired CQ fp0(u); q0(u)g, which requires to rewrite q with both rp and rq, is obtained only at the second rewriting step (from fp0(u); q1(u)g or from fp1(u); q0(u)g). 3
In order to obtain the precise dual of saturation, we define another breadth-first
rewriting mechanism able to unify a CQ with several rules from R at once. Instead of a
piece-unifier, we consider an “aggregated unifier” (as introduced in [
Let R0 = fr1; : : : ; rlg be a set of rules with each ri = (Bi; Hi). We recall that distinct rules have disjoint sets of variables. The aggregated rule assigned to R0, denoted by r1 : : : rl, is defined as B1 ^ : : : ^ Bl ! H1 ^ : : : Hl. Let R be the (infinite) set of aggregated rules assigned to multisubsets of R (i.e., an aggregated rule may involve several “copies” of the same rule from R, with a safe renaming of variables in each copy).
Then, for any UCQ Q, (Q; R) = Q [(q;r; ) f (q; r; )g, where q 2 Q, r = r1 : : : rl 2 R with l jqj, and is a piece-unifier of q with r. We denote by k (Q; R) the associated breadth-first k-rewriting. 5 Example 5. Consider again Ex. 4. We have 1 (fqg; R) = 1(fqg; R)[ffp0(u); q0(u)gg, where the additional query is obtained by unifying q with the aggregated rule r1 r2 = p0(x0); q0(x1) ! p1(x0); q1(x1).
We now prove that the new breadth-first rewriting fulfills the desired properties. Lemma 1 For all F; R and q, it holds that (F; R)j= q iff F j= (fqg; R). 5 We could state (Q; R) = (Q; R ), however it must be clear that, for each CQ, only a finite subset of R needs to be considered. Proof:(Sketch) ()) Let F 1 = (F; R). As F 1 j= q there is h such that h(q) F 1. Let q0 be the largest subset of q such that h(q0) F and fq1; : : : ; qlg be the partition of q n q0 such that each qi (0 < i l) maps to the atoms produced by the application of a rule ri = (Bi; Hi) 2 R to F with a homomorphism hi, i.e., h(qi) hisafe(Hi) (and F [ hs1afe(H1) [ : : : [ hlsafe(Hl) F 1). For each i > 0, let Hi0 Hi denote the useful part of Hi, i.e., h(qi) = hisafe(Hi0). If q0 = q, i.e., F j= q, then F j= (fqg; R) since q 2 (fqg; R). Otherwise, let r = r1 : : : rl and be the piece-unifier of q with r naturally associated with the homomorphisms h and h1 [ : : : [ hl (i.e., = (q1 [ : : : [ ql; H10 [ : : : [ Hl0; u) where for all terms e and e0 in the domain of u, u(e) = u(e0) iff (h [ hs1afe [ : : : [ hlsafe)(e) = (h [ hs1afe [ : : : [ hlsafe)(e0)). We easily check that F j= (q; r ; ). Since (q; r ; ) 2 (fqg; R), we obtain that F j= (fqg; R).
(() If F j= q then (F; R) j= q. Otherwise, we know there is q1 6= q in 1 (fqg; R) s.t. F j= q1 where q1 is obtained by rewriting q0 q with an aggregated rule r = r1 : : : rl and a piece-unifier (q0; H10 [ : : : [ Hl0; u). Let h0 be a homomorphism from q1 to F . For each ri = (Bi; Hi) composing r , h0 usafe is a homomorphism from Bi to F . Hence, (h0 u)safe(Hi) (F; R). We build the following homomorphism h from q to (F; R): for all x 2 vars(q), if x 2 vars(q) n vars(q0) then h(x) = h0(x), otherwise, let any e 2 Hi0 such that u(x) = u(e), then h(x) = (h0 usafe)safe(e).
0, it holds that k(F; R)j= q iff F j= k (fqg; R) Proof: The proof is by induction on k. For k = 0, the property is trivially true. Assume the property holds for any k < n. First note that, for any i 1, i(F; R) = i 1( (F; R); R) and i (fqg; R) = i 1( (fqg; R); R), which directly follows from the definitions. We have n(F; R)j= q iff n 1( (F; R); R)j= q iff (F; R)j= n 1(fqg; R) (by induction hypothesis) iff F j= ( n 1(fqg; R); R) (by Lemma 1) iff F j= n(fqg; R).
Hence, k(F; R)j= q iff F j= k (fqg; R) holds for any k 0.
This correspondence between k and k allows us to rely on the soundness and completeness of breadth-first forward chaining to establish the soundness and completeness of breadth-first rewriting: Corollary 1. It holds that F; R j= q iff F j= k (fqg; R) for some positive integer k.
Breadth-first rewriting yields an alternative definition of fus.
From now on, for a UCQ Q and a fixed set of rules R, we will denote the set k (Q; R) simply by Qk.
We now define bounded rules and clarify their relationships with other properties found in the literature. Two meaningful notions of boundedness can be provided, with the bound being based on fact saturation or on query rewriting.
(saturation-bounded) if there exists k 2 N such that for all F , F k (rewriting-bounded) if there exists k 2 N such that for all Q, Qk F k+1.
Qk+1.
We first show that these two notions precisely coincide.
bounded. Moreover, the bound is the same, i.e., for all F and all Q, for all k, F k F k+1 iff Qk Qk+1.
Proof: ()) Assume that R is saturation-bounded and let k be the bound. Then for all Q and F it holds that F; R j= Q iff F k j= Q. Let q be any query in Qk+1. Since q j= Qk+1, by soundness of rewriting, it holds that q; R j= Q; since R is saturationbounded, fqgk j= Q hence, by Th. 1, q j= Qk. Since this holds for any query q 2 Qk+1, we have Qk+1 j= Qk. Furthermore, by definition, Qk j= Qk+1. Thus Qk Qk+1.
(() Assume that R is rewriting-bounded and let k be the bound. Then for all Q and F it holds that F; R j= Q iff F j= Qk. By soundness of forward chaining, it holds that F; R j= F k+1; since R is rewriting-bounded, F j= (F k+1)k hence, by Th. 1, F k j= F k+1. Furthermore, by definition, F k+1 j= F k. Thus F k F k+1.
In light of this, next we will simply say bounded rules. In [
Definition 3 (Bounded-Derivation Properties) Let R be a set of existential rules. Then,
(F-BDD) if for all F there is k 2 N such that for all Q: F; R j= Q iff F k j= Q (Q-BDD) if for all Q there is k 2 N such that for all F : F; R j= Q iff F k j= Q (strong BDD) if there is k 2 N such that for all F and Q: F; R j= Q iff F k j= Q. We now show that these notions respectively correspond to fes, fus and boundedness. 6
6 The three following propositions were first proven by J.-F. Baget and M.-L. Mugnier and presented in a seminar at Oxford University in December 2012. Proof: ()) Let R be fes: for all F , there is k such that F k F k+1. By soundness and completeness of forward chaining, for any Q we have F; R j= Q iff there is n such that F n j= Q. For any F and such n, it holds that F k j= F n. Hence, F k j= Q.
(() Assume R has the F-BDD Property and set Q = fF k+1g (where k is the bound of the F-BDD Property). We thus have F; R j= F k+1 iff F k j= F k+1. Forward chaining is sound, so F; R j= F k+1. Hence F k j= F k+1. By definition, F k+1 j= F k. Therefore, F k F k+1.
Proof: ()) Let R be fus: for all Q, there is k such that Qk Qk+1. By soundness and completeness of breadth-first rewriting (Corollary 1), for any F , we have F; R j= Q iff F j= Qk. Equivalently, by Th. 1, F k j= Q. (() Assume R has the Q-BDD Property. For any q 2 Qk+1 (where k is the bound of the Q-BDD Property), let us set F = q: we have q; R j= Q iff (q)k j= Q. Breadth-first rewriting is sound, so q; R j= Q. Hence q j= Qk. Since this holds for any q 2 Qk+1, we have Qk+1 j= Qk. Since Qk is included in Qk+1, we also have Qk j= Qk+1. Therefore, Qk Qk+1.
Proof: The proof goes like that of Prop. 2.
()) Let R be saturation-bounded and let k such that for all F , F k F k+1. By soundness and completeness of forward chaining, for any F and Q, we have F; R j= Q iff F k j= Q.
(() Assume R has the strong BDD Property and set Q = fF k+1g (where k is the bound of the strong BDD Property). We thus have F; R j= F k+1 iff F k j= F k+1. Forward chaining is sound, so F; R j= F k+1. Hence F k j= F k+1. By definition, F k+1 j= F k. Therefore, F k F k+1. 5
Boundedness = fes \ fus We now prove that bounded rules are exactly those at the intersection of fes and fus classes.
One direction of the proof (() is straightforward, and follows by Prop.s 2 and 3, simply picking the k of the bound. We dedicate the remaining of this section to the formal development of the other direction. We first consider the set of all objects of the form (B ; H ) where B is a rewriting of a rule body in R and H is the saturation of B with R. When R is fes, such objects correspond to rules (i.e., each H can be made finite). When moreover R is fus, the set of all rewritings to be considered is finite, hence the set of all rules of interest is finite.
Definition 4 (Rule Completion) Let R = fr1; : : : ; rng be a fes and fus set of rules of the form ri = (Bi; Hi). We define the set CR as follows: 2. For any qij 2
kij +1(qij ; R) (such a kij exists since R is fes). 1. For any ri = (Bi; Hi), let ki be the smallest integer such that ki (Bi; R) ki+1(Bi; R) (such a ki exists since R is fus).
ki (Bi; R), let kij be the smallest integer such that kij (qij ; R) 3. Then:
CR = f(B ; H ) j ri = (Bi; Hi) 2 R; B 2 ki (Bi; R); H = kij (B ; R) g The bound associated with R is dR = maxri2R;qij 2 ki (Bi;R)(kij ).
Note that CR is finite and unique (up to bijective variable renaming). Most importantly, its size depends solely on R.
R.
Proof: The direction CR j= R holds since, for each rule ri = (Bi; Hi) 2 R, Bi 2 ki (Bi; R), hence there is a rule r = (B ; H ) 2 CR with Bi = B and Hi H . Direction R j=CR follows from the soundness and completeness of saturation. Indeed, for each rule (B ; H ) 2 CR, let (B 0; H 0) be obtained by replacing each frontier variable with a distinct fresh constant (i.e., that does not occur in R). By definition of CR, we have B 0; R j= H 0, and equivalently R j= B ! H .
We now show that each saturation step with CR can be computed by a bounded number of saturation steps with R (again with a bound independent from any fact base, Prop. 6). Next, we will show that a single saturation step with CR is actually sufficient to saturate any fact base (Prop. 7), therefore it is equivalent to a bounded number of saturation steps with R.
any fact base F , dR (F; R) j= (F; CR) (where dR is the bound introduced in Def. 4). Proof: (Sketch) Let F 0 = dR (F; R). We show that for each rule r = (B ; H ) 2 CR and each homomorphism h from B to F , F 0 j= (F; r; h) holds, which suffices to prove that F 0 j= (F; CR) since all rules are applied “in parallel” in a single saturation step. Consider the sequence S of rule applications leading from B to H . The choice of dR implies that dR (B ; R) H . Let h from B to F . The sequence S can be applied “similarly” to F (i.e., each homomorphism hi associated with a rule application is replaced by h hi), yielding S(F ) with S(F ) j= h(H ). Since H is obtained in at most dR breadth-first steps, this is also true for S(F ), hence F 0 j= S(F ). Since F F 0, we obtain F 0 j= F [ hsafe(H ) = (F; r; h).
that (F; CR) k(F; CR) for all k 1.
Proof: (Sketch) We focus on proving that (F; CR) j= ( (F; CR); R) which suffices to derive the thesis. Indeed, we know that for any F 0 and R0 if F 0 j= (F 0; R0) then F 0 j= k(F 0; R0), for all k 2 N. Hence (F; CR) k( (F; CR); R), in particular for k = dR. Moreover, as R is both fes and fus by Prop. 6 we have that (F; CR) j= ( (F; CR); CR).
Let r = (B ; H ) be any rule of R. If r is applicable to (F; CR) with a homomorphism h, then h(B ) (F; CR). By Prop. 6 we thus have dR (F; R) j= h(B ). By sTuhc.h1,thwaet Fgetj=thaht(FB )j=rew.dARn(fyhr(eBw)rgit;inRg)s,esqoutehnecree efrxoismtshh((BB))rtoewh2(B )drRew(fcha(nBb)eg;pRer)formed “similarly” from B yielding Brew 2 dR (fB g; R) with Brew h(B )rew. Besides, by definition of CR, we know there exists r = (B ; H ) 2 CR with B = Brew and H dR (Brew; R). We show that any derivation sequence from B to H can be applied to h(B )rew to entail h(B ). Since r = (B ; H ) 2 R and this sequence is applied until saturation, h(H ) is also entailed. We conclude that (F; CR) j= h(H ). Proof: [Proof of Th. 3] We now prove that if R is fes and fus then it is bounded.
For any fact base F and any CQ q, F; R j= q iff F; CR j= q (Prop. 5). From Prop. 7, F; CR j= q iff (F; CR) j= q. Hence, F; R j= q iff (F; CR) j= q. It remains to show that there is k independent from F and q such that k(F; R) (F; CR). From Prop. 6, we have a constant k (k = dR) independent from F and q such that k(F; R) j= (F; CR); moreover, since F; R j= k(F; R) for any k, we have (F; CR) j= k(F; R). We conclude that R is bounded. 6
In this paper, we provide several results that clarify the relationships between fundamental properties of existential rule sets, namely fes, fus and boundedness. The main result is that bounded rule sets are exactly those that are both fes and fus.
Recognizing if a set of rules is bounded is a difficult problem, which is already
undecidable for plain datalog [
Besides, the halting condition for the saturation process considered here relies on
logical equivalence (i.e., F k F k+1). This condition corresponds exactly to the
halting of the chase variant known as the core chase [
Acknowledgments. This work was partially supported by project PAGODA (ANR-12JS02-007-01).