Extending Decidable Cases for Rules with Existential Variables

1 Introduction

Rules have long been considered as an essential component of knowledge-based systems. In this paper, we deal with rules which extend the rules usually considered in logic programming or deductive databases: they are in the form H → C, where H and C are conjunctions of atoms, respectively called the hypothesis and conclusion of the rule, and there might be variables in the conclusion which are existentially quantified. E.g. the rule R = Human(x) → Parent(y, x) ∧ Human(y) stands for the formula ∀x(Human(x) → ∃y(Parent(y, x) ∧ Human(y))). This kind of rule, that we call ∀∃-rule, has the same logical form as a very general kind of dependencies studied in databases called tuple generating dependencies (TGD) [AHV95] and as conceptual graph (CG) rules [Sow84; BM02]. They can also be seen as an abstraction for ontological knowledge expressed in specific KR languages, e.g. the RDFS rules [Hay04], constraints in F-logic-Lite [CK06; CGK08], as well as some kinds of inclusions in description logics [BCM+03; CGL+07].

Let us consider knowledge bases (KB) composed of a set of facts (existentially closed conjunctions of atoms) and a set of ∀∃-rules. Several fundamental problems on these KB are equivalent (and very simple reductions allow us to go from one problem to another), namely fact deduction (is a fact deducible from a KB?), rule deduction (is a rule deducible from a KB?) and boolean conjunctive query answering in the presence of incomplete knowledge (is a boolean conjunctive query deducible from a KB?). The database versions of these problems are conjunctive query containment w.r.t. a set

Marie-Laure Mugnier

LIRMM

Univ. Montpellier - CNRS

mugnier@lirmm.fr

´Eric Salvat

IMERIR

LIRMM

salvat@imerir.com

of TGD, TGD implication and boolean conjunctive query answering under constraints expressed by TGD. In this paper, we have chosen fact deduction to represent this family. All results obtained regarding this problem can be immediately recast in terms of the other problems.

Deduction is not decidable ([Var84] for TGD, [BM02] for CG rules), which is due to the existential variables in the conclusion. Finding expressive decidable cases is thus extremely important. Until now, there were only decidable cases based on the forward chaining scheme (called the chase in databases). With the previous rule R, forward chaining does not halt: once R has been applied, it can be applied again indefinitely and each application produces a fact which is not equivalent to any of the previous ones. Most exhibited decidable classes of rules correspond to cases where forward chaining halts (with the notable exceptions of the results in [JK84; CGK08], cf. Sect. 5).

We propose a new approach, which allows us to extend the map of decidable cases. Briefly, we combine backward and forward chaining schemes in association with a graph that captures exactly the notion of dependency between rules; this graph is used to define a combination of both schemes preserving completeness and decidability. The key notion, in the definitions of our backward chaining mechanism and our dependecy criteria, is that of a piece, which can be seen as a "unit of knowledge" brought by a rule application. It allows us to keep accounting for the complex structure of a rule conclusion induced by existential variables, by characterizing sets of atoms which should not be processed separately (e.g. in the above rule R, {Parent(y, x), Human(y)} is a piece).

The main contributions of this paper are as follows:

• newdecidable classes based on finite backward chaining (Sect. 3.2: Th. 2, Prop. 2 and 3);
• the effective characterization of the notion of dependency between rules, allowing one to build an optimal graph of rule dependencies (GRD) (Sect. 4.1: Th. 3);
• new decidable classes obtained by combining the structure of the GRD and classes of rules for which forward or backward chaining are finite (Sect. 4.2: Th. 4, 5, 6);
• a map of known decidable cases, ordered by inclusion, including an extension obtained by combining our results with the results in [CGK08] (Sect. 5: Th. 7, 8).

2 Preliminaries

Basic definitions. We consider a first-order logical language with constants but no other function symbols. For space saving, we also do not consider equality in this short paper. Hence, an atom is of form p(t1 . . . tk), where p is a predicate of arity k and the ti are variables or constants. A fact is a set of atoms. A rule is a couple R = (H,C) of facts where H is called the hypothesis of R and C its conclusion. We note that term(X), var(X) and const(X) are respectively the sets of terms, variables and constants occurring in the atoms of a fact or a rule X. The frontier of a rule R (notation fr(R)) is the set of variables occurring both in H and C. Let F ∧ be the conjunction of atoms in a fact F; the logical translation of F is the existential closure of F ∧. A rule R = (H,C) is logically translated into the formula ∀h1 . . . ∀hk(H∧ → (∃c1 . . . ∃cqC∧)) where {h1, . . . , hk} = var(H) and {c1, . . . , cq} = var(C) \ fr(R). In the examples, we use the form H∧ → C∧, with the quantification of variables being implicit. A knowledge base (KB) is composed of a set of facts and a set of rules. As the union of two facts is a fact, we consider the set of facts as a single fact. We thus note (F,R) a KB, where F is a fact and R is a set of rules. The same notation is used for facts (resp. rules) and their logical translation. We use the classical notions of semantic consequence, noted |=, and equivalence, noted ≡.

We address the following deduction problem, called FRDEDUCTION: "given aKBK = (F, R) and a fact Q, is Q deducible fromK, i.e. does {F}∪R |= Q hold?". As explained in the introduction, this problem can be seen as a representative of several equivalent problems. It is semi-decidable (several proofs mentioned in [BM02]). Since Q and F are both facts, only their role in the deduction problem distinguishes them. When we need to distinguish between them, we call F the assertion and Q the query; Q is also called a goal in backward chaining.

Substitution and homomorphism. Given a set of variables V and a set of terms T , a substitution of V by T is a mapping from V to T. Let σ : V → T be a substitution, and F be a fact. σ(F) denotes the fact obtained from F by replacing each occurrence of x ∈ V ∩term(F ) by σ(x). If R = (H, C) is a rule, σ(R) = (σ(H), σ(C)). A safe substitution is a bijection from V to a set of new variables (i.e. that do not appear in the formulas involved in the reasoning). Given two facts F and Q, a homomorphism from Q to F is a substitution σ from var(Q) to term(F) such that σ(Q) ⊆ F. If there is a homomorphism from Q to F, we say that Q maps to F. Homomorphism checking is sound and complete w.r.t. logical deduction in the fragment of facts: given F and Q two facts, F |= Q iff Q maps to F (several proofs of this result in KR and databases).

Forward Chaining. We assume in this paper that the reader is familiar with forward and backward chaining paradigms. We recall here some definitions and results about forward chaining. A rule R = (H, C) is applicable to a fact F if there is a homomorphism σ from H to F . The application of R to F according to σ produces a fact α(F, R, σ) = F ∪σ(σ′ (C)), where σ′ is a safe substitution of var(C) \ fr(R). This application is said to be redundant if α(F,R, σ) ≡ F (it suffices to check that α(F, R, σ) maps to F ). A fact F ′ is called an R-derivation of F if there is a finite sequence (called the derivation sequence) F = F0, F1, . . . , Fk = F ′ such that for all 1 ≤ i ≤ k, there is a rule R = (H, C) ∈ R and a homomorphism σ from H to Fi-1 with Fi = α(Fi-1, R, σ). Such a derivation yields a sound and complete mechanism: given a KB K = (F,R) and a fact Q, Q is deducible from K iff Q maps to an R-derivation of F [SM96]. The following definition of a finite expansion set and associated concrete cases are from [BM02]. A set of rules is called a finite expansion set if it is guaranteed, for any fact, that after a finite number of rule applications, all further rule applications will become redundant, i.e. produce facts equivalent to the current fact. More precisely:

Definition 1 (Finite expansion set and full derivation) A set of rules R is called a finite expansion set (f.e.s.) if for any fact F, there is an R-derivation F ′ of F such that for every rule R = (H,C) ∈ R, for every homomorphism σ from H to F ′ , α(F ′ ,R, σ) maps to F ′ (i.e. all rule applications on F ′ are redundant). F ′ is called a full R-derivation of F.

If R is a f.e.s., any forward chaining algorithm that builds a derivation sequence and stops when all rule applications are redundant then checks if Qmaps to the fact obtained, is complete and halts in finite time. The f.e.s. notion is an abstract characterization of sets of rules allowing for a finite forward chaining mechanism, but it does not help to predict that the mechanism will actually stop on a given set of rules (note, moreover, that all decidable cases of the problem do not rely upon f.e.s.). As concrete classes of f.e.s., let us cite the range restricted rules (r.r.) in positive Datalog, which do not have existentially quantified variables (i.e. var(C) ⊆ var(H)) and disconnected rules, whose frontier is empty. The backward chaining paradigm that we present now allows one for new decidable classes, namely by finite unification sets.

3 Backward Chaining Revisited

The key operation in a backward chaining mechanism is the unification between part of a current goal (a fact in our framework) and a rule conclusion. This mechanism is typically used in logic programming, with rules having a single atom in the conclusion, which is unified with an atom of the current goal. Since the conclusion of a ∀∃-rule has a more complex structure (it may contain several atoms and possibly existentially quantified variables), the associated unification operation is also more complex. It allows one to process conclusions and goals without decomposing them into atoms, and we will show that it is worthwhile to do so. We will rely on the notion of a piece, which stems from a graph vision of rules and was introduced in [SM96] for CG rules. We reformulate it, as well as the associated unification notion, in a logical framework. As shown in Sect. 4.1, we will also use unification in a new perspective.

3.1 Piece-based rewriting

Given a subset T of its terms, a fact can be partitioned into pieces according to T. The piece notion is easier to grasp if we see a fact as an undirected bipartite graph, with two kinds of nodes, representing respectively terms and atoms, and such that there is an edge between a term node t and an atom node A if t occurs in A. Then, given a set of term nodes T, two atom nodes A1 and A2 are in the same piece if there is a path between them that does not go through a node of T . If T = ∅, each connected component of T is a piece.

Definition 2 (Pieces, Cutpoints) Let F be a fact and T ⊆ term(F). A piece of F according to T is a non-empty subset of F recursively defined as follows: each atom is in a piece; two distinct atoms A1 and A2 are in the same piece iff either (var(A1) ∩ var(A2)) \ T ̸= ∅, or there is an atom A3 ∈ F such that A1 and A3 are in the same piece and A3 and A2 are in the same piece. Let R = (H, C) be a rule. The cutpoints of R are the set of terms cutp(R) = fr(R) ∪ const(C). A piece of R is a piece of C according to cutp(R).

Example 1 (Pieces) R = p(x, y) → p(x, z) ∧ p(z, t) ∧ p(t, x) ∧ p(x, u) has one cutpoint, which is x, hence two pieces {p(x, z), p(z, t), p(t, x)} and {p(x, u)}.

A piece can be seen as a "unit" of knowledge brought by a rule application in forward chaining. Indeed, a rule R can be decomposed into an equivalent set of rules with the same hypothesis and exactly one piece in the conclusion. More precisely, any rule R = (H,C), such that C contains k pieces C1, . . . ,Ck, is semantically equivalent to the set of rules {(H,Ci)}1≤i≤k. Moreover, the conclusions of these rules cannot be further decomposed while keeping a set of ∀∃-rules with the same semantics as R (provided that H is not modified, see another decomposition later).

Backward chaining erases whole pieces of a goal Q. To explain the key ideas of the following unifier definition, let us present it as performing the inverse of a rule application to a potential fact. Given Q and a rule R = (H,C), assume that Q can be proven by an application of R to a fact F according to a homomorphism πR, i.e. there is a homomorphism πQ from Q to α(F,R, πR) and πQ(Q) is not included in F. Let σR be the substitution of fr(R) (extracted from πR) used to apply R to F . Q can then be partitioned into Q′ and Q′′ , such that πQ maps Q′ to σR(C) and Q′′ to F. Let TQ be the set of terms t in Q such that πQ(t) is in const(C) ∪ σR(fr(R)). TQ defines pieces of Q, which can be partitioned into pieces of Q′ and pieces of Q′′ . Each piece of Q′ is mapped by πQ to a piece of σR(C). Briefly said, the backward chaining step associated with σR erases from Q the pieces composing Q′ and adds σR(H) to it.

Definition 3 (Unifier) Let Q be a fact and R = (H, C) be a rule. A unifier of Q with R is a tuple μ = (TQ, Q′ , σQ, σR) where:

• TQ is a subset of term(Q), which thus defines pieces in Q (TQ is possibly empty);
• Q′ is the union of one or more pieces of Q (defined by TQ);
• σQ is a substitution from the variables of TQ to const(C) ∪ TQ and σR is a substitution from fr(R) to const(C) ∪ TQ;
• there is a homomorphism σ from σQ(Q′ ) to σR(C) such that for all t ∈ TQ, there is t′ ∈ cutp(R) with σ(σQ(t)) = σR(t′ ).

Definition 4 (Rewriting a fact) Let Q be a fact, R = (H,C) be a rule, and μ = (TQ,Q′ , σQ, σR) be a unifier of Q with R. A rewriting of Q according to R and μ produces a fact β(Q, R, μ) = σ′ (σR(H)) ∪ σQ(Q \ Q′ ), where σ′ is a safe substitution from var(H) \ fr(R).

Example 2 (Unification) Let R = h(x, y) → p(x, z) ∧ q(z, y) ∧ r(z, t). Let Q = p(u, v) ∧ q(v, u) ∧ s(u, w). Q is unifiable with R, with TQ = {u}, which defines two pieces Q1 = {p(u, v), q(v, u)} and Q2 = {s(u,w)}. Q′ = Q1, σQ = {(u, u)}, σR = {(x, u), (y, u)} (with σ = {(u, u), (v, z)}). The new fact is h(u, u) ∧s(u, w) (with σ′ = ∅).

Definition 5 (Rewriting sequence) Let Q and Q′ be two facts, and R be a set of rules. We say that Q′ is an Rrewriting of Q if there is a finite sequence (called the rewriting sequence) Q = Q0,Q1, . . . ,Qk = Q′ such that for all 1 ≤ i ≤ k, there is a rule R = (H, C) ∈ R and a unifier μ of Qi-1 with R such that Qi = β(Qi-1, R, μ).

The soundness and completeness of backward chaining (next theorem) relies on the following equivalence between R-rewriting and R-derivation:

Property 1 Let F and Q be two facts, and R be a set of rules. There is an R-rewriting of Q that maps to F iff there is an R-derivation F ′ of F such that Q maps to F ′ .

Theorem 1 Let K = (F, R) be a KB, and Q be a fact. Then F, R |= Q iff there is an R-rewriting of Q that maps to F .

Let us end with a remark about the piece notion. It might be argued that the unification operation would be much simpler if rule conclusions were decomposed, not only into single pieces (which would not fundamentally simplify the unification definition), but into single atoms. Indeed, a rule (H,C) can be equivalently encoded by a set of rules {H → R(t1, ..., tk), (R(t1, ..., tk) → Ac)Ac∈C)}, where R is a new predicate assigned to the rule and t1...tk are the terms of C. However, the rewriting mechanism would then build "nogood" unifications that would have been avoided with piecebased unification (see the example 3 below). Besides the loss of efficiency in backward chaining, this decomposition of rule conclusions beyond single pieces weakens the characterization of decidable cases, as shown in Sect. 4.1.

Example 3 (Atomic Decomposition) The rule R = h(x, y) → p(x, z) ∧ q(z, y), which has a single piece, could replaced by three rules: RA 1 = h(x, y) → R(x, y, z), RA 2 = R(x, y, z) → p(x, z) and RA 3 = R(x, y, z) → q(z, y). Let Q = s(u, v) ∧ q(v,w). Q is not unifiable with R, but it is with RA 3 , because the information that RA 2 and RA 3 cannot be considered independently has been lost.

3.2 Finite unification sets

Consider a backward chaining mechanism that builds Rrewritings of Q in a breadth-first way and maintains a set Q of the most general R-rewritings built (i.e. it does not add a new R-rewriting Q′′ to Q if there is Q′ ∈ Q with Q′′ |= Q′ ); it answers yes if it finds anR-rewritingQ′ s.t. F |= Q′ . This algorithm is sound and complete and halts on positive instances of the problem. Whereas finite expansion sets ensure that all information deducible from a fact in forward chaining can be encoded in a finite fact, the finite unification sets presented hereafter ensure that the above set Q of rewritings is finite.

Definition 6 (Finite unification set) A set of rules R is called a finite unification set (f.u.s.) if for every fact Q, there is a finite set Q of R-rewritings of Q such that for any Q′ ∈ Q, for any rule R ∈ R, for any unifier μ of Q′ with R, there is a fact in Q that maps to some β(Q′ ,R, μ). We say that Q is a full R-rewriting set of Q.

The above backward chaining mechanism halts in finite time if R is a f.u.s., hence:

Theorem 2 FR-DEDUCTION is decidable if R is a f.u.s.

Similarly to f.e.s., f.u.s. yield an abstract characterization, that should be instantiated with concrete examples. We provide two concrete cases of f.u.s. rules hereafter.

Definition 7 (Atomic hypothesis rule) A rule R = (H,C) is called an atomic hypothesis rule (a.h.) if H contains a single atom.

Property 2 A set of a.h. rules is a f.u.s.

A.h. rules are particularly well adapted to express necessary properties of concepts or relations in ontological languages, without any restriction on the form of the conclusion (i.e. rules of formC(x) → P or r(x1 . . . xk) → P , where C is a concept, r a k-ary relation and P any set of atoms). The second kind of rules does not put any restriction on the form of the hypothesis but constrains the form of the conclusion:

Definition 8 (Domain restricted rule) A rule R = (H,C) is called a domain restricted rule (d.r.) if each atom of C contains all or none of the variables in H.

Property 3 A set of d.r. rules is a f.u.s.

E.g. the set {R} with R = Human(x) → Parent(y, x) ∧ Human(y) is not a f.e.s. but it is a f.u.s. since R is a.h. (and d.r.). It is easy to check that the union of two f.e.s. (resp. f.u.s.) is not a f.e.s. (resp. f.u.s.). Moreover, combining a f.e.s. and a f.u.s. may lead to non-decidability. In the next section, we study conditions on the interaction between rules that keep decidability.

4 Compilation of the rule base

Generally speaking, compiling a knowledge base involves preprocessing it off-line, so that the compiled form obtained can be used on-line to accelerate reasoning tasks (e.g. query answering). Concerning rules, a classical compilation technique consists of precomputing a graph encoding dependencies between rules. Due to space limitations, we will not detail how this technique allows one to improve the efficiency of forward and backward chainings (as done for example in [Bag04]), but rather use it to extend decidable classes of rules.

4.1 The Optimal Graph of Rule Dependencies

A rule R′ is said to depend on a rule R if the application of R on a fact may trigger a new application of R′ :

Definition 9 (Dependency) A rule R′ = (H′ ,C′ ) depends on a rule R = (H,C) if there is a fact F, a homomorphism σ : H → F and a homomorphism σ′ : H′ → α(F, R, σ), such that σ′ (H′ ) ̸⊆ F.

It is easy to define necessary conditions for a rule to depend on another: e.g. if R′ depends on R then there is an atom in H′ that can be unified (classical meaning) with an atom in C. Characterizing dependency by actually computable necessary and sufficient conditions is less obvious. In the next definition of the graph of rule dependencies, we thus distinguish between graphs that are "complete" w.r.t. to dependency (i.e. all dependencies are encoded by their edges), and the only sound and complete graph, whose edges encode all dependencies and only dependencies.

Definition 10 (Graph of rule dependencies) Let R be a set of rules. A graph of rule dependencies (GRD) of R is a directed graph (R, E), where R is the set of nodes and E is the set of edges, such that, if R′ depends on R, then (R,R′ ) is an edge of E. The optimal GRD of R (notation GRD(R)) is the (only) GRD of R with the minimal number of edges.

Assertions (resp. queries) can be added to the GRD as rules with an empty hypothesis (resp. conclusion) and are thus sources (resp. sinks) in the GRD. The next theorem shows that our unifiers exactly capture the dependency notion:

Theorem 3 Let R be a set of rules. Then the GRD (R,E), where (R,R′ ) ∈ E iff there is a unifier of the hypothesis of R′ with R, is the optimal GRD of R.

Though all results presented hereafter in this paper remain valid when considering any GRD, building the optimal GRD is important both to optimize reasoning and provide wider decidable classes.

Example 4 (Dependency) Let R0 = p(x, y) ∧ p(y, x) → p(x, z) ∧ p(z, t) ∧ p(t, x). With a weak criterium, R0 could depend on itself. Using the criterium in Th. 3, it does not: C0 is a single piece, and since R0 has only one cutpoint (x), there should be a homomorphism from H0 to C0 (which would map x to x). Note that if z was replaced by y in C0, the rule obtained would have 2 cutpoints and 2 pieces, and would depend on itself.

Example 5 (GRD) Let R = {R0, R1, R2, R3}, where:

R0 is the rule in Example 4

R1 = q(x) ∧ p(x, y) → q(y)

R2 = p(x, y) → r(x, y, z) ∧ p(z, w)

R3 = s(x) ∧ t(x, y) → p(x, y)

GRD(R) has two loops (R1, R1) and (R2, R2) plus the edges (R0,R1), (R0,R2), (R3,R0), (R3,R1) and (R3,R2).

Let us point out that decomposing rule conclusions into single atoms (see Sect. 3.1) would weaken the GRD notion. Indeed, "fake" dependencies could be introduced. For instance, in Example 3 and inserting Q (as a rule with an empty conclusion): there are edges (RA 1 ,RA 2 ) and (RA 1 ,RA 3 ), and, which is the bad point, an edge (RA 3 ,Q), whereas there would be no edge (R, Q). Thus, even if the GRD obtained is optimal for {RA 1 ,RA 2 ,RA 3 ,Q}, it does not compute optimal dependencies w.r.t. {R,Q}.

4.2 Decidability results related to the GRD

Let us consider a basic forward chaining mechanism, that proceeds in a breadth-first way, i.e. at each step it computes all new (and non redundant) rule applications w.r.t. the current fact, then applies them to produce a new fact. If a subset of rules X ⊆ R has been non-redundantly applied at step i, then the only rules that have to be checked for applicability at step i + 1 are in the set {R′ ⊆ R|∃R ∈ X, (R, R′ ) ∈ E}. Similar arguments apply for backward chaining. The next theorem follows:

Theorem 4 Let R be a set of rules. If GRD(R) has no circuit, then R is both a f.e.s. and a f.u.s.

Note that a loop (a self-unifiable rule) in the GRD is sufficient to yield the non-decidability of the deduction problem. 1 One can however accept some kinds of circuits, as stated in the next theorem:

Theorem 5 Let R be a set of rules. If all strongly connected components 2 of GRD(R) are f.e.s. (resp. f.u.s.), then R is a f.e.s. (resp. f.u.s.).

Since forward and backward chainings do not stop on the same kinds of rules, the idea is to combine both mechanisms, not into a single mechanism (like some Datalog evaluation techniques [AHV95]), but rather use one after the other, provided that the interactions between rules obey some constraint preserving finiteness, thus decidability. This constraint is expressed on the GRD as follows:

Definition 11 (Finitely combined set) Let R be a set of rules. A partition (R1,R2) of R is said to be finitely combined if R1 is a f.e.s., R2 is a f.u.s., and there is no edge from a rule of R2 to a rule of R1 in GRD(R). R is a finitely combined set if it admits a finitely combined partition.

Example 5 (continued) Each rule forms its own connected component. {R1} is a f.e.s. since R1 is range restricted (r.r.), but it is not a f.u.s. {R2} is a f.u.s. since R2 is a.h. (and d.r.), but it is not a f.e.s. {R3} is a f.e.s. and a f.u.s. because R3 is r.r. and d.r. R0 does not belong to one of our concrete classes, but {R0} is a f.e.s. and a f.u.s. since its GRD has no edge. From Th. 5, we conclude that {R0,R1,R3} is a f.e.s. and {R0,R2,R3} is a f.u.s. A finitely combined partition necessarily considers R3 and R0 as f.e.s. because of their edges to R1. Thus, the only finitely combined partition is {{R0, R1, R3}, {R2}}.

The next theorem provides an effective decidable sound and complete mechanism for finitely combined sets of rules: given a finitely combined partition, first use forward chaining on the f.e.s. part to compute a full derivation of the facts, say F ′ , then use backward chaining on the f.u.s part to check if there is a rewriting of Q that maps to F ′ .

Theorem 6 Let (R1,R2) be a finitely combined partition of a set of rules R, and F and Q be two facts. Then F,R |= Q iff Q′ maps to F ′ , where F ′ is a full R1-derivation of F and Q′ belongs to a full R2-rewriting set of Q.

1 In the PhD thesis of one of the authors (2002), it is proven that a universal Turing machine can be encoded by a single self-dependent rule. The proof can be used to show that the union of two f.e.s./f.u.s. leads to non-decidability. Indeed, the rule can be split into two rules, with each rule forming a f.e.s. (and a f.u.s.).

2 Two nodes x and y are in the same strongly connected component if there are directed paths from x to y and from y to x. Any isolated node forms its own strongly connected component.

5 Novelty, Related works and Perspectives

Weak characterizations of rule "dependency" (also called "precedence") have been used in several algorithms involving ∀∃-rules, yielding non-optimal GRDs (e.g. in the Sesame reasoner which processes RDFS rules [BK03]). A precursor of our GRD is introduced in [Bag04]: this paper defines a criterium of dependency for CG rules, which, translated into ∀∃- rules, is optimal for rules without constants. Instead, we rely on unification, which has an additional advantage of connecting the notion of dependency to backward chaining. F.e.s. are introduced in [BM02] and a result equivalent to the f.e.s. part in Th. 5 is proven in [Bag04]. Our definition of unification is equivalent (but more compact and simpler) to that introduced in [SM96] for processing CG rules in backward chaining. The notions of f.u.s. and associated results (Th. 2, Prop. 2 and 3) as well as the combined use of the GRD structure with forward and backward chainings are totally new (Th. 4, 5, 6).

Concerning TGD, let us first cite the pioneer paper of [JK84] that showed that query containment on inclusion dependencies (ID) is decidable even if the forward chaining (i.e. the chase) may not halt. Note that, as ID are rules with a single atom in the hypothesis and in the conclusion, they are particular a.h. rules, thus we provide another (and simpler) proof of decidability, based on the finiteness of backward chaining.

Let us now consider our results w.r.t. two very recent papers on TGD, [CGK08] and [DNR08]. [CGK08] presents decidability results going beyond f.e.s.: roughly summarized, it is shown that if a set of rules only generates facts having bounded treewidth when seen as graphs (we call such a set a bounded treewidth set, b.t.s. in short), the deduction problem becomes decidable. Intuitively, a b.t.s. generates a "treelike" graph, and even though this graph can be infinite, to answer a query of finite size, it is not needed to generate more than a finite number of different "tree patterns". A f.e.s. is a b.t.s., since the finite saturated graph generated by a f.e.s. has bounded treewidth. On the other hand, a f.u.s. is not a b.t.s. Two concrete decidable fragments are defined in [CGK08]. Guarded TGD (gTGD) are rules such that an atom of the hypothesis contains ("guards") all variables of the hypothesis; in weakly guarded TGD (wgTGD), only some variables of the hypothesis need to be guarded 3 . gTGD are a subset of wgTGD, and both are b.t.s. The following examples illustrate that the decidable classes in both papers are incomparable.

1. {g(x, y, z, t) ∧ p(x, y) ∧ p(y, z) ∧ p(z, t) → p(y, t)} contains a single rule that is both guarded (gTGD) and r.r., but it is not a f.u.s.
2. {p(x, y) → p(y, z)} contains a single ID (thus both guarded and a.h.), but it is not a f.e.s.
3. {t(x) → s(x, y) ∧ t(y) ; t(x) ∧ t(y) → r(x, y)} is a f.u.s. (indeed, its GRD satisfies the conditions of Th. 5), but it is not a b.t.s.
4. {t(v, x) → q(x, y) ∧ p(y, z) ∧ r(z, u) ; r(x, y) ∧ p(y, z) → s(z, u) ∧ s(x, v)} is both a f.e.s. and a f.u.s. (its GRD has no circuit), but it is not a set of wgTGD.

3 More precisely, these variables occur at an "affected" position in a predicate, i.e. a position in a predicate that may contain a new variable generated by forward chaining.

[DNR08] studies "sets of TGD with universal models", which are exactly f.e.s. The main decidable case is the "stratified chase graph", which can be seen as an instantiation of the f.e.s. part of Th. 5 with "weakly acyclic" (w.a.) TGD, this kind of TGD including the r.r. and disconnected rules of [BM02; Bag04]. The "chase graph" is equivalent to our GRD, but no constructive characterization of this graph is provided in [DNR08].

Since f.u.s. and b.t.s. form distinct decidable classes, one should explore how these sets interact with each other. The following theorems provide a first answer:

Theorem 7 Let R be a set of rules. If all strongly connected components of GRD(R) are b.t.s., then R is a b.t.s.

Since a single rule without self-dependency is a b.t.s., it follows that the latter example (point 4), though not a wgTGD, is a b.t.s.

Theorem 8 Let R be a set of rules admitting a partition (R1,R2) such that R1 is a b.t.s., R2 is a f.u.s. and there is no edge in GRD(R) from a rule of R2 to a rule of R1. Then the deduction problem is decidable.

Figure 1 synthetizes the inclusions between the decidable classes finally obtained. All these inclusions are strict. Decidable classes written in italics are abstract classes. Classes in boldface are generic classes: we provide an algorithm recognizing them, and the size of the recognized class is function of the number and the size of concrete classes (in standard font) considered as their input. Note that we have added a new concrete class: a set of rules with a frontier of size at most one (noted fr1), which is interesting because it is not a f.e.s., neither a f.u.s., but is a b.t.s. without being necessarily weakly guarded. We have highlighted (in gray) classes that form the contributions of this paper. Even if the notion of acyclic GRD is not new in itself, we have highlighted it because the optimal characterization of dependencies (Th.3) is a key contribution of this paper.

As for further work, our study of decidable cases will be continued through a study of their complexity, pursuing the work in [BM02], [CGK08] and [DNR08].