--- title: "Chasing Sets: How to Use Existential Rules for Expressive Reasoning" authors: - "David Carral" - "Irina Dragoste" - "Markus Krötzsch" - "Christian Lewe" doi: "10.24963/ijcai.2019/225" url: "https://ijcai.org/proceedings/2019/225" pdf: "https://ijcai.org/proceedings/2019/0225.pdf" venue: "Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence" year: 2019 pages: "1624-1631" track: "Main track" keywords: - "Knowledge Representation and Reasoning: Computational Complexity of Reasoning" - "Knowledge Representation and Reasoning: Description Logics and Ontologies" - "Knowledge Representation and Reasoning: Logics for Knowledge Representation" - "Knowledge Representation and Reasoning: Knowledge Representation Languages" --- # Chasing Sets: How to Use Existential Rules for Expressive Reasoning David Carral, Irina Dragoste, Markus Krötzsch, Christian Lewe *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 1624-1631. DOI: [10.24963/ijcai.2019/225](https://doi.org/10.24963/ijcai.2019/225) ## Abstract We propose that modern existential rule reasoners can enable fully declarative implementations of rule-based inference methods in knowledge representation, in the sense that a particular calculus is captured by a fixed set of rules that can be evaluated on varying inputs (encoded as facts). We introduce Datalog(S) -- Datalog with support for sets -- as a surface language for such translations, and show that it can be captured in a decidable fragment of existential rules. We then implement several known inference methods in Datalog(S), and empirically show that an existing existential rule reasoner can thus be used to solve practical reasoning problems. ## Full text ## 1 Introduction Rules of inference are of fundamental importance in logical reasoning, and the central building block of many proof systems, including tableaux-based model constructions, resolution calculi, type-theoretic procedures [Ortiz et al., 2010], and "consequence-driven" approaches in ontological reasoning [Kazakov, 2009]. Indeed, rule-based calculi of logical deduction are as old as formal logic itself. More recently, rules have also seen much renewed interest as a declarative computing paradigm, and many rule-based reasoning systems have been presented [Benedikt et al., 2014; Geerts et al., 2014; Aref et al., 2015; Baget et al., 2015; Nenov et al., 2015; Urbani et al., 2016]. At the core of these implementations is the simple rule language Datalog, which is often extended with support for existential quantifiers or function terms in the consequences of rules. While this makes reasoning undecidable in general, there are many fast and scalable reasoners for cases where a finite model can be constructed using some variant of the chase procedure [Benedikt et al., 2017; Urbani et al., 2018]. It seems natural to exploit such systems to solve reasoning tasks in other areas of logic. This can be achieved by translating theories of a relevant logic into sets of rules that entail equivalent consequences. This idea has been applied, e.g., to description logics [Ortiz et al., 2010] and guarded logics [Ahmetaj et al., 2018]. Many such approaches do not play to the strengths of modern rule engines, though, since they create exponentially many (i.e., millions of) rules [Carral et al., 2018] or rules with linearly many (i.e., thousands of) variables [Ahmetaj et al., 2018]. A more promising approach might be to "implement" reasoning algorithms in a fixed (small) set of logical rules that operates on instances of logical reasoning tasks encoded as (large) sets of input facts. This is closer to the typical presentation of rule-based deduction calculi, and was already proposed for rule-based implementations of some logics [Kr¨otzsch, 2011]. Unfortunately, this approach is severely limited by the low data complexity of known rule languages, which is PTIME not just for Datalog, but for every previously proposed decidable existential rule language that guarantees the chase to be finite [Kr¨otzsch et al., 2019]. All of the aforementioned tools can only be used if the chase is finite; 1 otherwise reasoning will not terminate. We seem to be faced with a big dilemma: either to deal with large rule sets (in terms of rule number or size), or to be content with solving polynomial problems. Surprisingly, however, the limits of decidable criteria that guarantee chase termination do not apply to the chase algorithm as such: Kr¨otzsch et al. recently showed that, in theory, even current rule engines can perform complex computations based on a fixed "program" of rules while still being guaranteed to terminate with a finite chase [2019]. In this paper, we show that this theoretical insight can be turned into a practical approach for solving a wide range of logical reasoning tasks with existing rule engines. To unlock the necessary expressive power while guaranteeing termination, we need rather complex existential rule sets that would be difficult to adapt for implementing further reasoning tasks. We overcome this problem by proposing a more convenient intermediate language, Datalog(S), which extends Datalog with relationships over sets of constants (Section 3). This is inspired by the DatalogS language of Ortiz et al. [2010], but differs in that the available sets are not fixed as part of the schema, but can grow with the size of the input: Datalog(S) achieves EXPTIME-complete data complexity. We show that every Datalog(S) program can be translated polynomially into a set of existential rules for which a previously proposed (and implemented) variant of the standard chase algorithm terminates in exponential time (Section 4). Notably, the translated rule set does not fall into any known fragment that guarantees chase termination, and we believe that it would be difficult to design an appropriate new fragment that is nearly as easy to use as Datalog(S). 1 Even though weakly (frontier) guarded rules are a decidable existential rule fragment with EXPTIME-complete data complexity [Gottlob et al., 2014], the chase does not terminate for this language, and no reasoners have been implemented for this fragment. We illustrate the capabilities of this new approach by implementing two previously proposed reasoning algorithms in Datalog(S): a consequence-based algorithm for description logics (Section 5), and a type-based algorithm for guarded Horn logic (Section 6). Moreover, we demonstrate practical applicability for the former by executing it on an existing rule engine to classify several real-world ontologies (Section 7). Details we had to omit are found online [Carral et al., 2019]. ## 2 Preliminaries We consider a signature based on mutually disjoint, countably infinite sets of constants C, variables V, nulls N, and predicates P. We assign some arity ar(p) ≥ 0 to all p ∈ P. A term is an element in T = C∪V∪N. We abbreviate lists of terms t1, . . . , tn as ⃗t, and treat such lists as sets. An atom is a formula p(⃗t) with p ∈ P, ⃗t ⊆ T, and ar(p) = |⃗t|. We write ϕ[⃗x] to indicate that ⃗x is the set of all free variables in the formula ϕ. An (existential) rule is a null-free formula of the form ∀⃗x, ⃗z.β[⃗x, ⃗z] → ∃⃗y.η[⃗x, ⃗y] where ⃗x and ⃗y are disjoint lists of variables, β (the body) and η (the head) are conjunctions of atoms, and η contains at least one atom. Often, we omit universal quantifiers from rules. A fact is a variable-free rule with an empty body and a single atom in the head. A rule is generating if it contains existential variables, and non-generating (or Datalog) otherwise. For a formula ϕ and a substitution σ : V → C ∪ N, let ϕσ be the expression obtained by replacing all unbound occurrences of all x ∈ V in ϕ by σ(x) if σ is defined for x. Definition 1. Consider a rule ρ = β[⃗x, ⃗z] → ∃⃗y.η, an atom set A, and a substitution σ. The rule and substitution 〈ρ, σ〉 is applicable to A if (i) the domain of σ is ⃗x∪⃗z, (ii) βσ ⊆ A, and (iii) ησ′ ̸⊆ A for all σ′ ⊇ σ. Then, ρ(A) is the superset of A which, for all tuples 〈ρ, σ〉 applicable to A, contains the facts in ησ′ ⊆ ρ(A) with σ′ ⊇ σ a substitution mapping each y ∈ ⃗y to a fresh null. For a rule set R and an atom set A, let R(A) = ⋃ρ∈R ρ(A). Let R∀ and R∃ be the sets of all non-generating and generating rules in R, respectively; and let R∗∀ (A) be the superset of A with R∀(R∗∀ (A)) = R∗∀ (A). Definition 2 (Datalog-First Chase). For a rule set R, let R0 = ∅, R1, . . . be the sequence with Ri = R∃(R∗∀ (Ri-1)) for all i ≥ 1. The chase of R is the set chase(R) = ⋃i≥1 Ri. The chase of R terminates if Rk-1 = Rk for some k ≥ 1. Note that the Datalog-first chase is not a radically different chase method but simply a specific type of rule-application strategy for the standard chase (also referred to as restricted). Fact 1. A fact φ is entailed by a rule set R iff φ ∈ chase(R). This follows from the fact that the standard chase produces a universal model under all strategies [Deutsch et al., 2008]. ## 3 Datalog with Sets We now introduce the syntax and semantics of a language that extends Datalog with a set datatype that can represent collections of (non-set) elements. It is defined as a sorted logic with built-in set-related functions and predicates of the expected semantics. This approach is close in spirit to the extension of Datalog with complex values [Abiteboul et al., 1994] for the special case with only two sorts (called dom and {dom} by Abiteboul et al.), no negation, and a restricted choice of complex value operators. We consider two sorts: a sort of objects obj and a sort of sets set. A signature of Datalog(S) is based on countably infinite sets of object constants Cobj, object variables Vobj, set variables Vset, and predicate names P including special predicates {∈, ⊆} ⊆ P. The signature of a predicate symbol p is a tuple sig(p) = 〈S1, . . . , Sn〉 of sorts, with sig(∈) = 〈obj, set〉 and sig(⊆) = 〈set, set〉. An object term is any object constant or object variable. A set term is any set variable, the special constant ∅, an expression {t} where t is an object term, or, recursively, an expression (T1 U T2) where T1, T2 are set terms. We consider {t1, . . . , tn} an abbreviation for ({t1}U({t2}U. . .U{tn} . . .)) and omit parentheses for U. Unless otherwise stated, we use lower-case letters for object terms and upper-case letters for set terms. An atom is an expression p(t1, . . . , tn) where p ∈ P with sig(p) = 〈S1, . . . , Sn〉 and ti is a term of sort Si. We write ∈(t, S) as t ∈ S, and ⊆(S1, S2) as S1 ⊆ S2. A Datalog(S) rule is an expression of the form B1 ∧ . . . ∧Bℓ → H1 ∧ . . . ∧ Hk, with atoms B1, . . . ,Bℓ (the body) and H1, . . . ,Hk (the head), and where we require that: - every object variable in the head occurs in a body atom, - every set variable in the rule occurs in a body atom that uses some non-special predicate p ∈ P \ {∈, ⊆}, and - the head does not use a special predicate. A Datalog(S) program is a set of Datalog(S) rules. We admit rules with empty body for representing Datalog(S) facts. Example 1. Before defining Datalog(S) semantics formally, we give an example that can be understood with an intuitive reading of Datalog(S) rules. Consider input facts forming a chain succ(1, 2), succ(2, 3), . . . , succ(ℓ - 1, ℓ), starting at the constant 1 (the other constant names are immaterial). The following program entails facts for binary predicate n that form an n-chain of length 2ℓ : n(U, V ) ∧ parts(V, x, V ′ ) ∧ n(V ′ , W ′ ) Elements of the n-chain are represented by sets, ordered as if each input constant in the succ-chain defines one bit of a binary number. full(S) means that the represented number is of the form 0 · · · 01 · · · 1; parts(S, x, S′ ) means that the number S has its most significant bit at position x from the left, and that S = {x} ∪ S′ . The three facts (1) start the chain, and the two other rules define the next n-successor for when the most significant bit stays the same (2), or moves to the left (3), respectively. Using an exponentially long chain structure, it is easy to simulate exponential time deterministic Turing machine computations in Datalog [Dantsin et al., 2001]. Based on Example 1, we can apply a similar construction to Datalog(S) to obtain the following result, which should be contrasted to the polynomial data complexity of regular Datalog: Lemma 1. There is a fixed Datalog(S) program without special predicates ∈ and ⊆ for which fact entailment checking is EXPTIME-hard with respect to the size of the input data. The formal semantics of Datalog(S) codifies the intuitive idea of the set functions and relations. An interpretation I of Datalog(S) is defined by an object domain objI and an interpretation function ·I . The set domain setI of I is the powerset of objI . The interpretation maps non-special predicates p of signature sig(p) = 〈S1, . . . , Sn〉 to relations pI ⊆ SI1 × . . . × SIn, and special predicates as expected: ∈I = {〈δ, Γ〉 | δ ∈ Γ ∈ setI } and ⊆I = {〈Γ1, Γ2〉 | Γ1 ⊆ Γ2 ∈ setI }. Object constants c are mapped to elements cI ∈ objI . A variable assignment Z is a function mapping object variables x to elements Z(x) ∈ objI , and set variables Y to sets Z(Y ) ∈ setI . Given an arbitrary (set or object) term t, we define tI,Z recursively as follows: cI,Z = cI for c ∈ Cobj, xI,Z = Z(x) for x ∈ Vobj ∪Vset, ∅I,Z = ∅, {s}I,Z = {sI,Z }, and (S1 U S2)I,Z = SI,Z 1 ∪SI,Z 2 . An interpretation I and variable assignment Z satisfy an atom p(t1, . . . , tn), written I,Z |= p(t1, . . . , tn), if 〈tI,Z 1 , . . . , tI,Z n 〉 ∈ pI . I satisfies a Datalog(S) rule B1 ∧ . . . ∧ Bℓ → H1 ∧ . . . ∧ Hk if, for all variable assignments Z for I such that I,Z |= Bi for all 1 ≤ i ≤ ℓ, we also have I, Z |= Hj for all 1 ≤ j ≤ k. A program is satisfied if all of its rules are. A variable-free atom A is a logical consequence of a program P if I |= A for all I with I |= P . Since we require object and set variables to occur in (nonspecial) body predicates, it is easy to see that rules are only applicable to variable assignments that use values that correspond to (sets of) constants in the given input facts. A Datalog(S) program is therefore equivalent to its finite grounding, obtained by replacing variables by variable-free terms that represent all possible constants and sets of constants, respectively. This grounding results in an exponentially large propositional Horn theory for which reasoning tasks can be solved polynomially. Together with Lemma 1, we obtain: Theorem 1. Checking fact entailment for Datalog(S) is EXPTIME-complete for both data and combined complexity. ## 4 FromDatalog(S) to Existential Rules We now show how to polynomially translate Datalog(S) into existential rules while preserving (suitably translated) consequences. The heart of our approach is the following set RSU of existential rules (4)-(6), which can represent sets by nulls: Intuitively, set(s) means "s is a set" and empty(s) means "s = ∅." SU is for Singleton Union: SU(a, s, t) means "{a} ∪ s = t," and getSU(a, s) means "{a} ∪ s should be computed." Note that all terms are object terms in this one-sorted logic. Given an atom set A and a constant or null s ∈ C ∪ N, we therefore define the corresponding set [s]A = {a ∈ C ∪ N | SU (a, s, s) ∈ A}. We will combine RSU with additional non-generating rules, but some restrictions are needed to guarantee correctness. Definition 3. A type assignment α is a function that maps each predicate p ∈ P to a tuple α(p) = 〈S1, . . . , Sn〉 with n = ar(p) and Si ∈ {obj, set} for 1 ≤ i ≤ n, and where we require that α(empty) = 〈set〉, α(SU) = 〈obj, set, set〉, and α(getSU ) = 〈obj, set〉. We say position i in p is of type Si. A non-generating rule ρ is admissible if there is a type assignment such that: - (i) constants in ρ only occur on positions of type obj, - (ii) variables in ρ only occur on positions of a single type, - (iii) empty and SU do not occur in the head of ρ, and - (iv) getSU does not occur in the body of ρ. A set of rules (or facts) is admissible if all of its elements are. Example 2. RSU already suffices to simulate some Datalog(S) programs using further admissible rules. For example, rule (2) can be expressed with the following admissible rules, where the type assignment is as defined by the signature of the corresponding Datalog(S) predicates: The original rule is split into two: (7) requests the creation of an element to represent the set "{x}∪w′" by rule (5), and (8) uses this new element to instantiate the original head atoms. Example 2 illustrates how admissible rules can "call" the rules in RSU to provision "sets" as required. The following main correctness result confirms that this works as expected: Theorem 2. For every admissible set of non-generating rules R, the chase C = chase(R∪RSU) is such that - (a) empty(s) ∈ C implies [s]C = ∅, and If n is the size of R, then the size of C is in O(2n log n ). Proof. It is clear that rule (4) is applied exactly once, irrespective of R, introducing some null n∅ for v. By admissibility, the only rule heads with SU in R∪RSU are in (5) and (6), and an easy induction shows that n∅ can never occur in such facts. Hence, [n∅]C = ∅, showing claim (a). For (b), first note that the claim follows from the definition of [t]C if s = t. Facts SU(a, s, t) with s ̸= t are only derived by (5), and each null t occurs in at most one such fact. By the same rule, we get SU(a, t, t), showing a ∈ [t]C. If s = n∅, then rule (6) cannot produce further consequences, and we get [t]C = {a} as required. If s ̸= n∅, then we have a fact SU(b, s, s) for each b ∈ [s]C by definition of [s]C. Rule (6) Figure 1: Rules for arbitrary unions, membership, and containment (subscripts +/- are part of variable names; they hint at sets with additional/fewer elements) therefore derives SU(b, t, t), i.e., b ∈ [t]C. No other facts SU (b, t, t) can be derived, therefore [t]C = {a} ∪ [s]C. For the size of C, note that, all facts of the form SU(a, s, s) ∈ C are derived either when introducing s in (5), or immediately afterwards when closing under nongenerating rule (6) (which is prioritised in the Datalog-first chase). Therefore, whenever (5) is applied with a substitution σ to introduce a fresh null n = σ(v), all facts SU(b, σ(u), σ(u)) for b ∈ [σ(u)]C were already derived. Since (5) is applicable, σ(x) /∈ [σ(u)]C. Let CR be the finite set of constants that occur in R. By admissibility (and a simple induction), σ(x) ∈ CR, and by claim (b), [σ(u)]C ⊊ [n]C ⊆ 2CR . With ℓ = |CR|, there are at most ℓ! < ℓℓ ∈ O(2ℓ log ℓ ) possible sequences of applications of rule (5). This bounds the number of terms in the chase, and hence the number of derived facts, as claimed. Note that the proof relies on the prioritisation of rule (6) in the Datalog-first chase. However, by adapting a technique by Kr¨otzsch et al. [2019, Proof of Theorem 13], one can also obtain a (fixed) rule set that achieves the same termination and worst-case complexity properties for the standard chase. We omit this here as it makes rules more complicated and presumably less efficient in practice (since it artificially prevents the parallel application of rule (6) to all set elements). As the proof of Theorem 2 suggests, each set might be represented by several elements in the simulation via RSU. The elements generated by RSU correspond to sequences of unions of mutually distinct singleton sets, and several sequences might result in the same set. This has to be taken into account when simulating ⊆ and when performing joins over set terms. Singleton sets and the empty set have at most one representative. RSU can only simulate the empty set and unions with singletons. Arbitrary unions are supported by the rules (9)-(12) in Figure 1. Unions are constructed recursively by adding single elements from the first to the second input set. Rule (9) defines the base case. The other three rules split off a single element, use RSU to construct unions with singletons, and use the output to define the overall union. The rules are admissible for the intuitive type assignment α(getU) = 〈set, set〉 and α(U ) = 〈set, set, set〉. As the last ingredient, the rules (13)-(16) in Figure 1 define predicates in and sub that capture the built-in Datalog(S) predicates ∈ and ⊆, respectively. The complicated part is sub: facts of the form ckSub(u, v,w) ("check subset") express "v \ u ⊆ w." We initialise this for all pairs of sets (14), and recursively compare elements of the first argument (15) until reaching the empty set (16). This completes the required set of auxiliary rules. Before specifying the intended translation, we slightly normalise Datalog(S) rules. Let S1 = S2 be a shortcut for S1 ⊆ S2 ∧ S2 ⊆ S1. First, we replace every set term of the form S1 U S2 in a non-special predicate in the body with a fresh set variable S, and we add body atoms S = S1 U S2. Second, as long as a set variable S occurs more than once in a non-special predicate in the body of a rule, we replace one of these occurrences by a fresh variable S′ and add S = S′ to the body. It is easy to see that these transformations preserve semantics. Rules of the resulting form are called normalised. Normalisation ensures that set equality checks are performed using sub. Now consider a normalised Datalog(S) rule ρ. We will translate it to a set ER(ρ) of existential rules. For every set term S, let v(S) be a fresh (non-sorted) variable. Let S1, . . . , Sk be a sequence of all set terms in ρ that are neither variables nor ∅, such that no sub-term of any Si occurs to its right. For each term Si, we define atoms αi and βi: - if Si = {t} then αi = getSU(t, v(∅)) and βi = SU (t, v(∅), v(Si)), - if Si = T1 U T2, then αi = getU(v(T1), v(T2)) and βi = U (v(T1), v(T2), v(Si)). Finally, set γ0 = empty(v(∅)), and γj+1 = γj ∧ βj+1 for all 0 ≤ j < k. Now rule ρ = ϕ → ψ is translated into the set ER(ρ) of the following k + 1 rules: - (1) for each 0 ≤ i < k, a rule ϕ′ ∧ γi →αi+1, where ϕ′ and ψ′ are obtained from ϕ and ψ, respectively, by replacing all atoms t ∈ S by in(t, S), all atoms S ⊆ S′ by sub(S, S′ ), and all set terms S by v(S). Example 3. Let ρ = p(a, S, T, {a} U S) → q(S U T). Its normalisation ρ′ has the body ϕ = p(a, S, T,R) ∧ (R ⊆ {a} U S) ∧ ({a} U S ⊆ R). A possible order of set terms is S1 = {a}, S2 = {a} U S, S3 = S U T. The translated body is ϕ′ = p(a, v(S), v(T), v(R)) ∧ sub(v(R), v(S2)) ∧ sub(v(S2), v(R)). We obtain the following rules in ER(ρ′ ): where each ". . ." abbreviates the body of the previous rule. Definition 4. For a Datalog(S) program P, let ER(P) be the union of all rule sets ER(ρ) for ρ ∈ P and the rules (4)-(6) and (9)-(16). The following result is immediate from this definition: Theorem 3. For a Datalog(S) program P, the size of ER(P) is polynomial in the size of P. Theorem 4. For a Datalog(S) program P and Datalog(S) fact α, P |= α if and only if ER(P) |= ER(α). Moreover, the Datalog-first chase decides ER(P) |= ER(α) in EXPTIME. Proof sketch. The correctness of the extended set of rules (9)-(16) can be shown with a suitable extension of Theorem 2. We can restrict the notion of admissibility to also avoid the misuse of auxiliary predicates in these rules while requiring the expected type signatures. The correctness of the translation is easy; especially the translated rules are admissible when using the Datalog(S) signatures to define type signatures. The size bound on the chase carries over from Theorem 2, which establishes the second part of the claim. Together with Theorem 1, this correctness result implies that fact entailment is also EXPTIME-complete w.r.t. data complexity for the sets of rules obtained from our transformation. Therefore, these transformed sets are not covered by any decidable fragment of existential rules of P (or lower) data complexity, including previously proposed criteria that ensure termination of the skolem chase [Cuenca Grau et al., 2013] and Datalog-first chase [Carral et al., 2017], as well as first-order rewritability [Baget et al., 2011]. Weakly (frontier) guarded rules are one of the few fragments with similarly high data complexity [Gottlob et al., 2014], but already the rules in Figure 1 are not weakly frontier guarded. ## 5 Description Logics Reasoning To demonstrate the utility of our approach, we look at description logics (DLs) first. DLs are highly expressive logics with many applications, and for which numerous reasoning procedures have been proposed [Baader et al., 2007]. Among the many DLs that give rise to EXPTIME-complete reasoning tasks, we select Horn-ALC as a comparatively simple case that allows us to focus on our main ideas. 2 DL is based on mutually disjoint sets of concept names NC, role names NR, and individual names NI. We define Horn-ALC using axioms in normalised form [Kr¨otzsch et al., 2013]. Given A,B,C ∈ NC, R ∈ NR, and a, b ∈ NI, the following are axioms of Horn-ALC in normal form: Axioms (21) and (22), called class assertions, respectively role assertions, are ABox axioms, corresponding to unary and binary facts. The others are TBox axioms, with D ⊑ E representing a first-order formula ∀x.[D] → [E], where we define [A] = A(x), [B] = B(x), [∃R.C] = ∃y.R(x, y) ∧ C(y), [∀R.C] = ∀y.R(x, y) → C(y), and [A⊓B] = A(x) ∧B(x). ⊤ represents truth, and ⊥ falsity. 2 Our use of Horn DLs is not related to the fact that existential rules are in Horn logic. Rule-based reasoning methods for non-Horn DLs, e.g., from [Simanˇc´ık et al., 2011], could also be implemented. Classification is the task of computing all axioms of form (23) that are entailed by an ontology-i.e. a DL axiom set. Kazakov [2009] proposes a consequence-driven classification method for Horn-ALC. Figure 2 (left) shows the corresponding rules of inference in the version of Simanˇc´ık et al. [2011, Table 2]. Given a set T of TBox axioms, the rules produce inferences of the form H ⊑ B and H ⊑ ∃R.K where H, K are conjunctions of elements in NC ∪{⊥, ⊤} (viewed as sets when convenient). A rule is applicable if its pre- (above the line) and side conditions (on the right) are satisfied; then it derives the conclusion (below the line). A conjunction H is active if it is either defined to be active initially, or occurs in some inference, and rules (RA) and (R⊓) are restricted to such conjunctions. For classification, one initially sets all singleton conjunctions (i.e., concept names) to be active. The right of Figure 2 shows the corresponding Datalog(S) rules. It is easy to see how each rule corresponds to the inference rule to its left. We represent inferences by predicates SC and Ex with sig(SC ) = 〈set, obj〉 and sig(Ex ) = 〈set, obj, set〉, respectively. Predicates ax⊑, ax⊓⊑, ax⊑∀, ax∃⊑, and ax⊑∃ encode Horn-ALC axioms as facts. All elements of NC ∪ NR correspond to object constants in Datalog(S), and conjunctions are represented as sets. Only rules (R+∃ ) and (R∀) can activate new conjunctions, as recorded by predicate Act . To initialise the computation, we need to activate all singleton sets, which can be done by rules such as and analogous rules for all other types of axioms. It is obvious that this translation is faithful and therefore leads to an EXPTIME-complete (hence worst-case optimal) chase-based classification algorithm for Horn-ALC. We also note that the translation exhibits similar pay-asyou-go characteristics as the original approach. In particular, in EL-type description logics, which do not include axioms of type (28), only a linear number of singleton sets is needed, and the chase likewise terminates in polynomial time. It is an advantage of our approach that it can be used to make an existential rule engine perform essentially the same derivation steps as the original abstract inference-rule calculus. ## 6 Guarded Rules Reasoning We now apply our approach to reasoning with guarded existential rules (where all universally quantified variables appear in a single body atom). Ahmetaj et al. [2018] give an entailment-preserving translation from guarded rules with bounded predicate arity ˆa to a polynomial Datalog program. However, they require predicate arities in the order of 2ˆa . Their translation actually simulates sets in Datalog. For maximal arity ˆa, we consider the set A of all atoms that can be formed from a predicate in the guarded rules and generic variables x1, . . . , xˆa. A type is a subset of A, represented in Datalog by vectors of |A| constants 0 or 1. Datalog(S) rules are obtained, in essence, by replacing these vectors by sets, where we use constants cα for each α ∈ A. The rules frequently test for the absence of an element in a set. While not in Datalog(S), we can define this using an inequality predicate ̸≈ (even without logical inequality, this Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19) Figure 2: Horn-ALC inference rules by Simanˇc´ık et al. (left) and corresponding Datalog(S) program (right), where c⊤ and c⊥ are constants, lower-case letters are object variables, and upper-case letters are set variables can be axiomatised for constants; this suffices). We can now derive ckNotin(u, a, u) whenever a rule needs to know if "a /∈ u", and then apply the following rules: Confirmed non-memberships are recorded as notin(a, u). The approach resembles our computation of sub in Figure 1. With this additional feature, most rules of Ahmetaj et al. have a straightforward translation to Datalog(S). Their rules are organised in groups (I) to (IX), where (II) and (VI) only matter in the disjunctive case. Even the remaining rules are too many to specify, but we explain the key steps. Rules (I) initialise non-set predicates of arity ≤ ˆa, and require no modification. The rules in (III) define all types (vectors) and establish a linear order on them. This can be achieved in Datalog(S) along the lines of Example 1. Rules (IV) mark types based on the given guarded rules. Using a simple decomposition of rule bodies, we can assume that all guarded rules have the form ρ = A ∧ B → ∃⃗y.H. Then, for each mapping h from rule variables to {x1, . . . , xˆa}, we define a rule: If we assume that rules restrict to a common set of variables, there are only polynomially many possible mappings h due to the bounded arity. Therefore, instead of adding many rules, we can also encode those mappings and the rule ρ in Datalog(S) facts, and use a single Datalog(S) rule instead. The rules (V) are again very close to Datalog(S). They use predicates such as MarkedOneσ,h, named using rules σ and certain mappings h. As in (IV), we can remove the dependence on these input-related parts by representing rules and mappings as elements in the facts, and adding two additional parameters to MarkedOne to refer to them. Note that side conditions such as "R(⃗x) ∈ A with ⃗x ∈ h(vars(σ))" can simply be precomputed and stored as facts. Rules (VII) highlight some elements in types using a special constant 2 instead of 1, as in Such rules also depend on the given guarded rules that define A, but this dependence can easily be moved to the facts by encoding A there. Rules (VIII) define Horn types as those missing exactly one atom. We can build such types iteratively, so as to avoid the explicit mentioning of all elements in one rule. The remaining rules are also easy to express. Finally, rules (IX) infer entailed facts frommarked Horn types by removing elements from the type sets iteratively. Instead of removing elements, we can simply iterate by remembering the current position in an additional parameter. By these transformations, we can obtain a Datalog(S) program that captures the original Datalog program in a polynomial number of rules that each use only a bounded number of variables and atoms (based on the arity ˆa). If we further encode guarded rules, atoms, and mappings in Datalog(S) facts as indicated, we obtain a fixed Datalog(S) program that can reason on arbitrary guarded existential rules (encoded as facts), depending only on the signature of relevant predicates. Applying Theorem 4, we obtain a similarly small existential rule set for which the Datalog-first chase terminates: Theorem 5. For any fixed finite set of predicates P with maximal arity ˆa, there is a set of existential rules AOSP that 1. consists of polynomially many rules (in the size of P), 2. each with bounded number of atoms (independent of P), 3. using predicates of arity bounded by max(ˆa, 3), and 4. where chase(AOSP∪F) is exponential for every set of facts F, such that every set of guarded existential rules R over P can be translated into a polynomial set of facts FR such that AOSP∪FR and R entail the same ground facts over P. | ID | #Ax. | #Set | #SC | #Ex | VLog (sec) | |-------|--------|--------|-------|-------|--------------| | 00040 | 223K | 2K | 1051K | 334K | 432 | | 00048 | 142K | 19 | 718K | 171K | 387 | | 00477 | 318K | 0 | 162K | 167K | 1 | | 00533 | 159K | 0 | 965K | 351K | 132 | | 00786 | 152K | 12K | 2283K | 978K | 549 | Figure 3: Ontologies and results for classification (A) showing: axiom count; number of non-singleton "set terms" introduced (#Set); number of SC and Ex facts derived; reasoning time in VLog ![Image](https://ijcai.org/proceedings/2019/fulltext/225/image_000000_fb2f074063b53b0f7972fa70aaf265c2f9271979be3f56cfa928dc7367fb9341.png) UOBM 1.9M 4M 5.9M Number of assertions Figure 4: Experimental results for class retrieval (B) in VLog (pink/grey) and Konclude (black); note the log scale ## 7 Evaluation We conducted two experiments: (A) compute all consequences of the calculus in Figure 2, and (B) compute all entailed axioms of type (21) (class retrieval). All experiments where run on a MacBookPro (2.4GHz Intel Core i5, 8GB RAM). The rule engine VLog was used as an implementation for the Datalog-first chase [Urbani et al., 2018]. Further evaluation details can be found in [Carral et al., 2019]. For (A), we created a simplified rule set RCl from the rules in Figure 2, exploiting the fact that they do not need normalisation or all Datalog(S) features [Carral et al., 2019]. We classified five large and diverse ontologies from the Oxford Ontology Repository: 3 00040 (GO x-anatomy), 00048 (GO x-taxon), 00477 (Gazetteer), 00533 (ChEBI mol. function), and 00786 (NCI). The ontology statistics and results are shown in Figure 3. We measured pure reasoning time without the time needed to read the input file from disk. Columns #Set, #SC, and #Ex confirm that the ontologies require significant reasoning effort, which is also reflected in most VLog reasoning times. We observed that our rules for simulating sets made only small contributions to these times, although they dominate theoretical worst-case complexity. Most time instead was taken up by the computation of a small number of particularly slow joins - used to find rule matches in VLog -, especially for rule (R-∃ ). While our results show practicality, optimised DL reasoners are significantly faster: the DL reasoner Konclude [Steigmiller et al., 2014] needed between 2sec (00533) and 14sec (00786) for the tasks. This is not surprising, since Konclude is the leading implementation after decades of research on how to optimise this very computation, whereas VLog has never before been applied for such a task. Indeed, our ap- 3 https://www.cs.ox.ac.uk/isg/ontologies/ sec 103 102 101 100 proach leads to rules that are very different from the ones used in benchmarking rule engines today, and can therefore guide further optimisations of existing implementations. For experiment (B) we extend RCl with the following rules: Predicates CA and RA encode assertions: CA(A, c) encodes A(c); and RA(R, a, b) encodes R(a, b). We used several benchmark datasets that Zhou et al. [2015] created by sampling data for two large ontologies: the real-world knowledge base Reactome, and the synthetic benchmark UOBM. Figure 4 shows the total times (precomputing and reasoning) for VLog and Konclude. No times are shown in cases where Konclude exceeded a one-hour timeout. We observe that our approach leads to competitive performance in (B), which might have been expected since rule engines optimise for large datasets. In particular, VLog might benefit from its compact in-memory presentation of large predicates, which also helps to find rule matches more quickly if many facts can be processed together [Urbani et al., 2016]. ## 8 Conclusions We introduced Datalog(S) as a convenient high-level language for encoding complex reasoning algorithms, which can be "compiled" into existential rules that can be successfully executed on rule engines available today. This outlines an appealing new method for prototyping reasoning algorithms in an elegant and declarative way, potentially even resulting in highly scalable systems. It also indicates a promising new research direction for the development of modern rule engines. ## Acknowledgments This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in project number 389792660 (TRR 248, Center for Perspicuous Systems) and Emmy Noether grant KR 4381/1-1 (DIAMOND). ## References 1. [Abiteboul et al., 1994] Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison Wesley, 1994. 2. [Ahmetaj et al., 2018] Shqiponja Ahmetaj, Magdalena Or- tiz, and Mantas Simkus. Rewriting guarded existential rules into small datalog programs. In Proc. 21st Int. Conf. on Database Theory (ICDT'18), volume 98 of LIPIcs, pages 4:1-4:24. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2018. 3. [Aref et al., 2015] Molham Aref, Balder ten Cate, Todd J. Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L. Veldhuizen, and Geoffrey Washburn. Design and implementation of the LogicBlox system. In Proc. 2015 ACM SIGMOD Int. Conf. on Management of Data, pages 1371-1382. ACM, 2015. 4. [Baader et al., 2007] Franz Baader, Diego Calvanese, Deb- orah McGuinness, Daniele Nardi, and Peter Patel- Schneider. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, second edition, 2007. 5. [Baget et al., 2011] Jean-Franc ¸ois Baget, Michel Leclère, Marie-Laure Mugnier, and Eric Salvat. On rules with ex- istential variables: Walking the decidability line. Artif. In- tell., 175(9-10):1620-1654, 2011. 6. [Baget et al., 2015] Jean-Franc ¸ois Baget, Michel Leclère, Marie-Laure Mugnier, Swan Rocher, and Clément Sipi- eter. Graal: A toolkit for query answering with existential rules. In Proc. 9th Int. Web Rule Symposium (RuleML'15), volume 9202 of LNCS, pages 328-344. Springer, 2015. 7. [Benedikt et al., 2014] Michael Benedikt, Julien Leblay, and Efthymia Tsamoura. PDQ: proof-driven query answering over web-based data. PVLDB, 7(13):1553-1556, 2014. 8. [Benedikt et al., 2017] Michael Benedikt, George Konstan- tinidis, Giansalvatore Mecca, Boris Motik, Paolo Papotti, Donatello Santoro, and Efthymia Tsamoura. Benchmark- ing the chase. In Proc. 36th Symposium on Principles of Database Systems (PODS'17), pages 37-52. ACM, 2017. 9. [Carral et al., 2017] David Carral, Irina Dragoste, and Markus Krötzsch. Restricted chase (non)termination for existential rules with disjunctions. In Proc. 26th Int. Joint Conf. on Artif. Intell. (IJCAI'17), pages 922-928. ijcai.org, 2017. 10. [Carral et al., 2018] David Carral, Irina Dragoste, and Markus Krötzsch. The combined approach to query an- swering in Horn-ALCHOIQ. In Proc. 16th Int. Conf. on Principles of Knowledge Representation and Reason- ing (KR'18), pages 339-348. AAAI Press, 2018. 11. [Carral et al., 2019] David Carral, Irina Dragoste, Markus Krötzsch, and Christian Lewe. Chasing sets: How to use existential rules for expressive reasoning (extended techni- cal report). Available at https://iccl.inf.tu-dresden.de/web/ Inproceedings3212/en, 2019. 12. [Cuenca Grau et al., 2013] Bernardo Cuenca Grau, Ian Hor- rocks, Markus Krötzsch, Clemens Kupke, Despoina Magka, Boris Motik, and Zhe Wang. Acyclicity notions for existential rules and their application to query answer- ing in ontologies. J. Artif. Intell. Res., 47:741-808, 2013. 13. [Dantsin et al., 2001] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. ACM Computing Surveys, 33(3):374-425, 2001. 14. [Deutsch et al., 2008] Alin Deutsch, Alan Nash, and Jef- frey B. Remmel. The chase revisited. In Proc. 27th Sympo- sium on Principles of Database Systems (PODS'08), pages 149-158. ACM, 2008. 15. [Geerts et al., 2014] Floris Geerts, Giansalvatore Mecca, Paolo Papotti, and Donatello Santoro. That's all folks! LLUNATIC goes open source. PVLDB, 7(13):1565-1568, 2014. 16. [Gottlob et al., 2014] Georg Gottlob, Sebastian Rudolph, and Mantas Simkus. Expressiveness of guarded existential rule languages. In Proc. 33rd ACM SIGMOD-SIGACT- SIGART Symposium on Principles of Database Systems (PODS'14), pages 27-38. ACM, June 2014. 17. [Kazakov, 2009] Yevgeny Kazakov. Consequence-driven reasoning for Horn SHIQ ontologies. In Proc. 21st Int. Joint Conf. on Artif. Intell. (IJCAI'09), pages 2040-2045. IJCAI, 2009. 18. [Krötzsch et al., 2013] Markus Krötzsch, Sebastian Rudolph, and Pascal Hitzler. Complexities of Horn description logics. ACM Trans. Comput. Logic, 14(1):2:1- 2:36, 2013. 19. [Krötzsch, 2011] Markus Krötzsch. Efficient rule-based in- ferencing for OWL EL. In Proc. 22nd Int. Joint Conf. on Artif. Intell. (IJCAI'11), pages 2668-2673. AAAI Press/IJCAI, 2011. 20. [Krötzsch et al., 2019] Markus Krötzsch, Maximilian Marx, and Sebastian Rudolph. The power of the terminat- ing chase. In Proc. 22nd Int. Conf. on Database Theory (ICDT'19), volume 127 of LIPIcs, pages 3:1- 3:17. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2019. 21. [Nenov et al., 2015] Yavor Nenov, Robert Piro, Boris Motik, Ian Horrocks, Zhe Wu, and Jay Banerjee. RDFox: A highly-scalable RDF store. In Proc. 14th Int. Semantic Web Conf. (ISWC'15), Part II, volume 9367 of LNCS, pages 3-20. Springer, 2015. 22. [Ortiz et al., 2010] Magdalena Ortiz, Sebastian Rudolph, and Mantas Simkus. Worst-case optimal reasoning for the Horn-DL fragments of OWL 1 and 2. In Proc. 12th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR'10), pages 269-279. AAAI Press, 2010. 23. [Simančík et al., 2011] František Simančík, Yevgeny Kaza- kov, and Ian Horrocks. Consequence-based reasoning be- yond Horn ontologies. In Proc. 22nd Int. Joint Conf. on Artif. Intell. (IJCAI'11), pages 1093-1098. AAAI Press/IJCAI, 2011. 24. [Steigmiller et al., 2014] Andreas Steigmiller, Thorsten Liebig, and Birte Glimm. Konclude: System description. J. Web Semant., 27-28:78-85, 2014. 25. [Urbani et al., 2016] Jacopo Urbani, Ceriel Jacobs, and Markus Krötzsch. Column-oriented Datalog materializa- tion for large knowledge graphs. In Proc. 30th AAAI Conf. on Artif. Intell. (AAAI'16), pages 258-264. AAAI Press, 2016. 26. [Urbani et al., 2018] Jacopo Urbani, Markus Krötzsch, Ceriel J. H. Jacobs, Irina Dragoste, and David Carral. Efficient model construction for Horn logic with VLog: System description. In Proc. 9th Int. Joint Conf. on Automated Reasoning (IJCAR'18), volume 10900 of LNCS, pages 680-688. Springer, 2018. 27. [Zhou et al., 2015] Yujiao Zhou, Bernardo Cuenca Grau, Ya- vor Nenov, Mark Kaminski, and Ian Horrocks. PAGOdA: Pay-as-you-go ontology query answering using a Datalog reasoner. J. of Artif. Intell. Res., 54:309-367, 2015.