Extending Decidable Existential Rules by Joining Acyclicity and Guardedness

1 Introduction

Rule-based knowledge representation has a long-standing history in AI and related areas such as databases and information systems. Function-free first-order Horn logic (also referred to as Datalog) as one of the central paradigms, however, has been criticised for its inability of stating or inferring the existence of domain entities not previously introduced as constants [Patel-Schneider and Horrocks, 2007]. Existential rules, i.e. Datalog extended by value invention capabilities realised by existential quantifiers in rule heads, overcome this restriction and are currently studied under a variety of names such as Datalog+/-, ∀∃-rules, and - primarily in the database community - tuple-generating dependencies (TGDs) [Baget et al., 2010; 2009; Calì et al., 2010a; 2010b; 2009; 2008; Fagin et al., 2005; Deutsch and Tannen, 2003]. The recent interest in this formalism marks the convergence of two paradigms of knowledge representation research that used to be rather separated: rule-based approaches and ontology languages.

This new ground was found to be very fertile, as witnessed by the above works' discoveries of many new rule languages for which query answering is decidable. Widely varying data and combined complexities underline the richness of the field.

Sebastian Rudolph

Karlsruhe Institute of Technology, Germany sebastian.rudolph@kit.edu

Examples of application areas for this new family of knowledge representation languages range from data exchange and data integration [Fagin et al., 2005] to ontological data access in the spirit of the ontology languages of the DL-Lite family [Calì et al., 2009; Calvanese et al., 2007]. The wealth of recent contributions supports the development of such applications, but also calls for a more unified view on the existing proposals, their exact relationships, and formal properties. This is the general incentive for this work.

Concretely, we extend and consolidate two of the main notions commonly employed to ensure decidability: acyclicity and guardedness. The main contributions are as follows.

1. We extend weak acyclicity and weak (frontier-) guardedness to obtain joint acyclicity and joint (frontier-) guardedness. Both extensions use the observation that the existing notions over-estimate how far values can be passed on within a rule set, and that there is a refined criterion that still can be checked in polynomial time.
2. We present a new method of eliminating existential quantifiers from jointly acyclic rule sets. The approach incurs an exponential blow-up but is still worst-case optimal. The relevance of the method stems from the insight that a partial application of the procedure can also simplify rule sets that are not jointly acyclic.
3. We apply this observation to combine guardedness and acyclicity in the language of glut-(frontier-)guarded rules, based on identifying glut variables that may represent an overabundance of "existentially invented" values. Only glut variables remain affected by existential quantifiers after applying the elimination method introduced for jointly acyclic rules.

An important insight of this work therefore is that a very general notion of acyclicity can be combined "modularly" with existing rule languages without losing decidability. Jointly frontier-guarded rules serve us as an example for this construction, and illustrate that further studies are needed to determine the exact complexity of reasoning in each case. We determine exact combined worst-case complexities for all rule languages introduced herein.

Section 2 provides the preliminaries and reviews the existing results in the field. We then motivate and introduce the notion of joint acyclicity in Section 3, and present a generic way of eliminating jointly acyclic variables in Section 4. Section 5 introduces jointly frontier-guarded rules, and Section 6 combines all previous ideas to obtain glut-(frontier-)guarded rules for which the combined complexity of query answering is shown to be 3ExpTime-complete. Section 7 concludes. An extended version of this paper that contains detailed proofs is available as technical report [Krötzsch and Rudolph, 2011].

2 Existential Rules

We now provide the basic notions of the logical framework we consider, followed by an overview of a number of important approaches in this area.

Definition 1 Consider a signature 〈C, P,V〉 consisting of a finite set of constant symbols C, a finite set of predicates P, and an infinite set of variables V, all of which are mutually disjoint. A function ar : P → N associates a natural number ar(r) with each predicate r ∈ P that defines the arity of r. The set of positions of a predicate r is the set Πr = {〈r, 1〉, . . . , 〈r, ar(r)〉}.

• A term is a variable x ∈ V or a constant c ∈ C.
• An atom is a formula of the form r(t1, . . . , tn) if t1, . . . , tn are terms, and r ∈ P is a predicate with ar(r) = n.
• An existential rule (or simply rule in the context of this paper) is a formula of the form

where B1, . . . , Bk, H1, . . . , Hl are atoms all of whose variables are in the scope of some quantifier, and where no variable occurs more than once in x, y. 1 We use sets of atoms as a convenient notation for conjunctions of atoms. A Datalog rule is a rule with no existential quantifiers. A rule with k = 0 is called a fact (a conclusion that is unconditionally true), and a rule with l = 0 is called a constraint (a premise that must never be true).

The premise of a rule is called the body while the conclusion is called the head. Since all variables in rules are quantified, we will often omit the explicit preceding universal quantifier. A rule set Σ is renamed apart if each variable name is bound in at most one quantifier in Σ.

The rule language hereby introduced is a syntactic fragment of first-order predicate logic, and we consider it under the according semantics. This also means that every rule set is semantically equivalent to one that is renamed apart. Moreover, note that we do not exclude non-safe rules, i.e. rules with universally quantified variables that occur in the head but not in the body; all of our results apply in any case.

Definition 2 Let Σ be a set of rules. We call Σ satisfiable if it has a model according to the standard semantics of first-order logic. Two rule sets Σ and Σ ′ are equisatisfiable if either both or none of them is satisfiable. A boolean conjunctive query (BCQ) is a formula ∃v.Q where Q is a conjunction of atoms and v contains all variables in Q. A BCQ ∃v.Q is entailed by Σ if it is entailed under standard first-order logic semantics.

1 We freely use x, t, etc. to denote vectors of the form 〈x1, . . . , xn〉, 〈t1, . . . , tn〉, etc. throughout this paper.

Checking satisfiability and BCQ entailment for unrestricted existential rules is undecidable [Chandra et al., 1981b; Beeri and Vardi, 1981] even with very strong restrictions on the vocabulary or the number of rules [Baget et al., 2010]. Therefore, a large body of work has been devoted to the identification of restricted rule languages which retain decidability and still allow for sufficient expressiveness. A generic tool for establishing decidability results is the chase introduced by Maier et al. [1979] and extended to query containment by Johnson and Klug [1982]. Intuitively the chase procedure starts with a given set of factual data (ground facts) and "applies" rules in a production rule style by introducing new domain elements whenever required by an existentially quantified variable in a rule head. In general, termination of this procedure cannot be guaranteed, and an infinite set of new domain elements and facts may be created.

Many of the decidable rule classes come about by establishing properties about the chase they create. Finiteness of the chase is a straightforward criterion for ensuring decidability, and rule sets with this property are called finite extension sets [Baget et al., 2010]. This criterion is undecidable in general, but several sufficient conditions on rule sets for chasefiniteness have been identified. Pure Datalog (also known as full implicational dependencies [Chandra et al., 1981b] or total TGDs [Beeri and Vardi, 1981]) is an immediate case, as no new domain elements are created at all. A more elaborate concept is (weak) acyclicity [Deutsch and Tannen, 2003; Fagin et al., 2005] which we review and extend in Section 3. Another approach that pursues a similar goal by different means is to require acyclicity of the graph of rule dependencies introduced by Baget et al. [2009].

An even more relaxed condition than finiteness of the chase is that the (possibly infinite) chase enjoys a variant of the bounded treewidth property, leading to bounded treewidth sets [Baget et al., 2010]. Decidability of BCQ entailment follows from known decidability results for first-order logic theories with the bounded treewidth model property [Courcelle, 1990]. Again rules with this property are not recognisable in general, but a variety of sufficient conditions has been established. The most prominent examples are a number of guardedness conditions that we review and extend in Section 5.

Independently of the chase, other decidability criteria can be established by considering rewritings of the query in a backward-chaining manner. In analogy to the finite chase condition, one can define finite unification sets where this rewriting procedure terminates and yields a finite set of rewritten queries [Baget et al., 2010]. First-order rewritability also implies a sub-polynomial AC0 data complexity for BCQ entailment checking. Again, recognising finite unification sets is undecidable, and various decidable sublanguages are known. Examples include atomic-hypothesis rules and domain restricted rules [Baget et al., 2010], linear Datalog+/- [Calì et al., 2009], sticky sets of TGDs, and sticky-join sets of TGDs [Calì et al., 2010a; 2010b].

3 Joint Acyclicity

This section introduces joint acyclicity, which is a proper generalisation of the following notion of weak acyclicity

[Deutsch and Tannen, 2003; Fagin et al., 2005].

Definition 3 For a set of rules Σ, the dependency graph is a directed graph that has the positions of predicates in Σ as its nodes. For every rule ρ ∈ Σ, and every variable x at position 〈r, p〉 in the head of ρ, the graph contains edges as follows:

• If x is universally quantified, and x occurs in a body atom at position 〈s, q〉, there is an edge from 〈s, q〉 to 〈r, p〉.
• If x is existentially quantified, and the body of ρ contains a (necessarily universally quantified) variable y at 〈s, q〉, then there is a special edge from 〈s, q〉 to 〈r, p〉. 2

Σ is weakly acyclic if its dependency graph has no cycle going through a special edge.

Intuitively, non-special edges encode the possible passing of values in bottom-up reasoning, whereas special edges encode the dependency between the premise that a rule was applied to and the new individuals that the application of this rule entails. A cycle over special edges may indicate that newly invented values can recursively be used in premises which require the invention of further values ad infinitum. For instance, the rule

may lead to the construction of an infinite r-chain of new elements, and indeed the dependency graph has a special edge from 〈r, 2〉 to itself. But weak acyclicity also excludes cases where no infinite recursion would occur:

The dependency graph contains the same cycle as before, yet the rule cannot be applied recursively since invented values are not required to belong to c. Note that this remains true even if there are other rules with existentially quantified variables at 〈c, 1〉. We capture this by shifting our focus from positions to variables (which can occur in multiple positions):

Definition 4 Consider a renamed apart set of rules Σ. For a variable x, let Π B x (Π H x ) be the set of all positions where x occurs in the body (head) of a - necessarily unique - rule. Now for any existentially quantified variable, let Ωx be the smallest set of positions such that (1) Π H x ⊆ Ωx, and (2) Π H y ⊆ Ωx for every universally quantified variable y with Π B y ⊆ Ωx.

The existential dependency graph of Σ has the existentially quantified variables of Σ as its nodes. There is an edge from x to y if the rule where y occurs contains a universally quantified (body) variable z with Π B z ⊆ Ωx. Σ is jointly acyclic if its existential dependency graph is acyclic.

Thus Ωx contains the positions in which values invented for x may appear. This captures the effect of non-special edges in Definition 3, whereas special edges correspond to edges in the existential dependency graph. Definition 3 is obtained by modifying condition (2) in Definition 4 to require Π B y ∩Ωx nequal ∅ instead of Π B y ⊆ Ωx. This states that a value is propagated by a rule if it satisfies some - instead of all - of the rule's premises. Joint acyclicity therefore appears to be more natural.

2 The definition of Fagin et al. [2005] is slightly more general by requiring y to also occur in the head. Here we want to focus on the main idea of acyclicity. Our glut-frontier-guarded rules in Section 6 then properly generalise the original form of weak acyclicity.

The following rule is jointly acyclic (as a singleton set) but not weakly acyclic: its existential dependency graph has no edges while its dependency graph is a clique of special edges.

In spite of this generalisation, joint acyclicity is easy to recognise. Detecting cycles in a directed graph and checking inclusion of a position in Ωx is possible in polynomial time. The latter problem is also hard for P since propositional Horn logic entailment can be expressed using unary predicates with a single variable to encode propositions.

Another generalisation of weak acyclicity, called Superweak acyclicity (SwA), has been proposed in [Marnette, 2009]. SwA is more general than joint acyclicity as it uses function symbols and unification to exclude some additional cases of value propagation. It remains open how our results can be extended to SwA.

4 Reducing Jointly Acyclic Variables

We now present a method for eliminating existential quantifiers from rule sets. Applied iteratively to jointly acyclic rules, this procedure yields a Datalog program that faithfully represents all consequences of the original rule set. This establishes decidability and optimal complexity bounds for jointly acyclic rules. For the general case, the procedure still allows semantically faithful simplifications of rules that can be used to extend other decidable rule languages as in Section 6.

Our transformation simulates Skolemisation, the replacement of existentially quantified variables with Skolem terms, where we "flatten" function terms to represent them in Datalog. For example, Skolemising the rule r(x, y) → ∃v.s(x, v) yields r(x, y) → s(x, f (x, y)) where f is a fresh function symbol. We express this without functions by considering f as a constant and replacing s by a predicate s ′ of higher arity: r(x, y) → s ′ (x, f, x, y). Other predicates may need to be extended analogously in positions where the Skolem term might be relevant; those are exactly the positions in Ωv. Conversely, some uses of s may not require all the new positions, and we use a special symbol □ as a filler. For example, a fact s(a, b) is represented as s ′ (a, b, □, □).

Definition 5 Consider a renamed apart rule set Σ, such that there is an existentially quantified variable x that does not have incoming edges in the existential dependency graph.

Let k be the number of universally quantified variables in the rule containing x. For a predicate r define nr to be the cardinality of the set {〈r, p〉 ∈ Ωx | 1 ≤ p ≤ ar(r)}. If nr > 0 let ˆ r denote a fresh predicate of arity ar(ˆ r) = ar(r) + nrk; if nr = 0 let ˆ r denote r. Let f and □ be fresh constant symbols.

Σx is the set of rules that contains, for each rule ρ ∈ Σ, the rule ρx that is obtained by replacing each atom r(t1, . . . , tar(r)) in ρ by the atom ˆ r(s1, . . . , sar(r)) where the term vectors si are defined as follows:

• If 〈r, i〉 nelement Ωx then si colonequal ti. For the remaining cases, assume that 〈r, i〉 ∈ Ωx.
• If ti = x then si colonequal 〈 f, y1, . . . , yk〉 where y1, . . . , yk are all universally quantified variables in the rule.

• If ti = y is universally quantified and occurs only in positions in Ωx, then si colonequal 〈y0, y1, . . . , yk〉 where the same fresh universally quantified variable names yj are used in all replacements of y but nowhere else.
• In all other cases, si colonequal 〈ti, □, . . . , □〉 where this is a vector of length k + 1.

Quantifiers for ρ are updated accordingly: new universal quantifiers are introduced for all variables of the form y j, and the existential quantifier for x is deleted.

For a boolean conjunctive query ∃v.Q over the signature of Σ, the BCQ ∃v.Qx is defined as the body of the rule Qx → obtained by applying the above transformation to the rule Q →.

Note that this definition is well. In particular, for each r we find that nr of the vectors si are of length k + 1, and all others are of length 1, yielding the required ar(r) + nrk arguments of ˆ r. Applying this transformation to v in rule (3), we have k = 2 and Ωv = {〈r, 2〉, 〈s, 1〉}, and so obtain:

Next, we state the main correctness result for this transformation. The respective proof in [Krötzsch and Rudolph, 2011] directly shows equisatisfiability using suitable model transformations. This is not hard to formalise after observing the correspondence of domain elements in models of Σ on the one hand, and vectors of such elements - corresponding to term vectors si in Definition 5 - in models of Σx on the other.

Theorem 1 Given a set of rules Σ and a variable x as in Definition 5, Σ is satisfiable if and only if Σx is satisfiable. Moreover, a BCQ ∃v.Q over the signature of Σ is entailed by Σ if and only if ∃v.Qx is entailed by Σx.

We can thus apply Definition 5 iteratively, where Theorem 1 ensures that correctness is preserved. It is important that the iterative reduction also preserves joint acyclicity:

Theorem 2 Consider a rule set Σ, and a variable x as in Definition 5. The variables y nequal x without incoming edges in the existential dependency graph of Σ do not have incoming edges in the existential dependency graph of Σx either. Moreover, Σ is jointly acyclic if and only if Σx is jointly acyclic.

The previous theorem ensures that the set of variables that can be eliminated by applying Definition 5 iteratively is not affected by the order in which variables are reduced in case there is more than one variable without incoming edges. Yet, iterative reductions may yield syntactically different results depending on the order of application. This non-determinism is inessential for our considerations, so we use ja(Σ) to denote an arbitrary but fixed rule set obtained by iteratively applying Definition 5 until it is no longer applicable.

Theorem 3 If Σ is a jointly acyclic, renamed apart set of rules Σ then ja(Σ) is a Datalog program.

Before stating the main complexity result of this section, we provide a more precise estimate of the increase in size that is caused by the transformation. Importantly, the exponential blow-up is caused by chains of dependencies in the existential dependency graph, not by the size of the rule set in general.

Theorem 4 Given a renamed apart rule set Σ, the set ja(Σ) contains the same number of rules as Σ, and the same number of head and body atoms in each rule. The number of variables per rule in ja(Σ) is bounded by a function that is exponential in the maximum directed path length in the existential dependency graph of Σ, and polynomial in the size of Σ.

Theorem 5 Deciding whether a BCQ is entailed by a jointly acyclic set of rules is 2ExpTime-complete for combined complexity, ExpTime-complete if the maximal length of a path in the existential dependency graph is bounded, and P-complete in data complexity.

5 Jointly Frontier-Guarded Rules

A large class of existential rules for which query answering is decidable are based on the idea of guardedness [Andréka et al., 1998], the requirement that all or some of the universally quantified variables of a rule appear together in a single "guard" atom. Requiring guards only for variables that also appear in the head (the "frontier") yields frontier-guarded rules [Baget et al., 2010]. Both notions can be generalised by not requiring guards for variables that cannot possibly represent existentially introduced elements. This idea has been used to arrive at weakly guarded rules [Calì et al., 2008] and weakly frontier-guarded rules [Baget et al., 2010]. In this section, we generalise the latter to fit more naturally to our definitions in Section 3, and we establish basic complexity results.

Definition 6 Consider a set of rules Σ. A position 〈r, i〉 is affected if (1) Σ contains an existentially quantified variable on position 〈r, i〉, or (2) Σ contains a universally quantified variable x on position 〈r, i〉 in the head of a rule where x occurs on an affected position in its body. A position 〈r, i〉 is jointly affected if 〈r, i〉 ∈ Ωx for a variable x in Σ (see Definition 4).

A variable x in a rule ρ = ∀x.ϕ → ∃y.ψ ∈ Σ is universal if it occurs in x, affected if it occurs on some affected position in ϕ, jointly affected if it occurs only on jointly affected positions in ϕ, frontier if it occurs ϕ and in ψ. The sets of all such variables are denoted X u ρ , X a ρ , X ja ρ , X f ρ.

The rule ρ is X-guarded for a set X of variables, if all x ∈ X occur together in one atom in ϕ. Relevant notions are: guarded (X = X u ρ ), frontier-guarded (X = X f ρ), weakly guarded (X = X a ρ ), weakly frontier-guarded (X = X a ρ ∩ X f ρ), jointly guarded (X = X ja ρ ), jointly frontier-guarded (X = X ja ρ ∩ X f ρ). The set Σ is X-guarded if all rules ρ ∈ Σ are.

The relation of these notions follows from the observation that X u ρ ⊇ X f ρ and X u ρ ⊇ X a ρ ⊇ X ja ρ , e.g. every weakly guarded rule is also jointly frontier-guarded. The combined complexity of BCQ answering for guarded and weakly guarded rules is known to be 2ExpTime-complete [Calì et al., 2008]. Hardness carries over to the frontier-guarded cases, but upper complexity bounds for these languages have been open until very recently. We cite the following result from Baget et al. [2011].

Proposition 1 Deciding whether a BCQ is entailed by a frontier-guarded set of rules is 2ExpTime-complete for combined complexity.

Baget et al. [2011] further show that BCQ answering for weakly frontier-guarded rules is in 2ExpTime. Here, we extend this result to our new notion of jointly guarded and jointly frontier-guarded rules. We observe that variables that are not jointly affected may never represent elements that are introduced existentially. Hence, their assignments correspond to constant symbols that could be substituted instead. A naive use of this idea yields exponentially many partially grounded rules with constants used in all possible combinations.

A polynomial reduction is possible by extending the arguments of all predicates to contain parameters for all variables that are not jointly affected. These parameters then guard all such variables in rules. Bindings for the added parameters can only be inferred by auxiliary rules that allow arbitrary constants to be substituted for variables. These ideas are combined to the following definition.

Definition 7 For a renamed apart rule set Σ, let z = 〈z1, . . . , zn〉 be a list of all variables in Σ that are not jointly affected, and let ˜ r be a fresh predicate of arity ar(r) + n for each predicate r of Σ. The rule set guard(Σ) consists of:

1. for each rule ρ ∈ Σ with non-empty body, a rule ρ ′ ∈ guard(Σ) obtained by replacing each atom r(t1, . . . , tar(r)) (with terms ti) by ˜ r(t1, . . . , tar(r), z1, . . . , zn), where all variables zi are universally quantified,
2. for each rule ρ ∈ Σ with empty body (i.e. generalised fact), a rule ρ ′ ∈ guard(Σ) obtained by replacing each atom r(t1, . . . , tar(r)) (with terms ti) by ˜ r(t1, . . . , tar(r), c, . . . , c) where c is an arbitrary constant,
3. for each predicate r of Σ, each i ∈ {1, . . . , n}, and each constant symbol c, a rule

1. for each predicate r of Σ, a rule

where all variable names xi are fresh.

The next theorem shows the correctness of this transformation. The proof in [Krötzsch and Rudolph, 2011] directly transforms models of Σ into models of guard(Σ), and vice versa, restricting to minimal models in the latter case.

Theorem 6 A BCQ ∃v.Q is entailed by a renamed apart rule set Σ iff ∃v.Q is entailed by guard(Σ).

The following theorem is easily obtained by summing up the above results.

Theorem 7 Deciding whether a BCQ is entailed by a jointly guarded or jointly frontier-guarded set of rules is 2ExpTimecomplete for combined complexity.

6 Joining Acyclicity and Guardedness

The iterative reduction in Section 4 hints at a much wider applicability of the idea of joint acyclicity, since it allows for the elimination of some existential quantifiers even in rule sets that are not jointly acyclic. This is useful if the reduced rule set belongs to a rule language for which decidability of reasoning has been established on other grounds. In this section, we illustrate this idea by combining acyclicity with joint (frontier-)guardedness, and establish tight complexity bounds for related reasoning tasks.

Using the terminology of Section 5, we can say that Definition 5 eliminates jointly affected variables. To be more precise, we say that a variable in a renamed apart rule set Σ is a glut variable if it occurs in a set Ωx as in Definition 5 for a variable x that is part of a cycle in the existential dependency graph. Intuitively, glut variables may represent an overabundance of values, as opposed to the remaining, non-glut variables that can only represent finitely many values. Clearly, the iterative application of Definition 5 then turns non-glut variables into variables that are not jointly affected. This leads to a further generalisation of guardedness:

Definition 8 A renamed apart rule set Σ is glut-guarded (glut-frontier-guarded) if each rule of Σ has a body atom that contains all glut variables (that also occur in the head).

This definition is illustrated in the following example of a glut-frontier-guarded rule set, where c, intuitively speaking, marks persons that are "specifically important" for us:

• c(x) ∧ ancestor(x, ˙y) ∧ ancestor(˙y, ˙z) → ancestor(x, ˙z) (5)

Information about c, parent, and sibling would be given in facts, while the remaining predicates are derived only. The existential dependency graph has two edges v → w and w → w, where the latter cycle follows from (8). Glut variables thus are those occurring only on positions of Ωw; they are marked by a dot in the example. It is easy to verify that the example is glut-frontier-guarded. Note how c is used to make x in rule (5) non-glut, thus allowing a form of transitivity - a typical counter-example for all common types of guardedness. Furthermore, transitivity is not first-order rewritable, thus excluding the example from all types of finite unification sets reviewed in Section 2. Rule (10) is another illustration of the increased expressive power, since it is neither jointly frontierguarded nor glut-guarded. Indeed, since all positions other than those of sibling are in Ωv, almost all variables in the example are jointly affected.

Theorem 8 Deciding whether a BCQ is entailed by a glutguarded or glut-frontier-guarded set of rules Σ is 3ExpTimecomplete for combined complexity.

Inclusion is shown by applying Theorems 1 and 4 to obtain that ja(Σ) is an exponentially large rule set that can be used for BCQ entailment checking. Clearly, ja(Σ) is jointly frontierguarded, so the result follows from Theorem 7.

For hardness, one simulates an Alternating Turing Machine (ATM) with doubly exponential space. Such ATMs can accept all languages that a Turing Machine can accept given triply exponential time [Chandra et al., 1981a]. The ATM acceptance conditions as such can be formulated using frontierguarded rules, but the efficient encoding of a doubly exponential storage tape requires additional existential quantifiers. This leads to further variables being jointly affected, but not glut. The tape construction adapts a method for constructing doubly exponential chains proposed by Calì et al. [2010b]. Details are given in [Krötzsch and Rudolph, 2011].

7 Conclusion

We have extended the notions of weak acyclicity and weak (frontier-)guardedness, introduced a versatile new method for eliminating existential quantifiers, and applied these insights to define glut-frontier-guarded rules as one of the most expressive known existential rule languages for which query answering is decidable. Yet, a wide range of open issues still needs to be tackled for developing both the foundations of the field and applications to use these novel approaches.

Some immediate questions raised by this work concern the query complexity for fixed non-ground rules (data complexity) or for fixed signatures (bounded arity). A concurrent anonymous submission to this conference addresses these issues for previously defined rule languages, and it will be interesting to lift the respective methods to our cases.

More generally, further efforts are needed to continue the consolidation of rule languages that was started herein. To this end, modular reduction techniques for simplifying rule sets can be of great utility for advancing towards a unified theory of decidable existential rules.

Acknowledgements We thank Despoina Magka for helpful comments. Markus Krötzsch was supported by the EPSRC project ExODA (EP/H051511/1). Sebastian Rudolph was supported by the project ExpresST funded by the German Research Foundation (DFG).