Restricted Chase (Non)Termination for Existential Rules with Disjunctions

1 Introduction

Answering conjunctive queries (CQs) over ontologies is an important reasoning task with many applications in knowledge representation and data management. A flurry of research efforts have significantly improved our understanding of this problem, and led to concrete solutions for many ontologies based either on description logics (DLs) [Calvanese et al., 2007; Stefanoni et al., 2014; Calvanese et al., 2014; Bienvenu et al., 2016] or on existential rules [Baget et al., 2011; Cuenca Grau et al., 2013; Cal`ı et al., 2013].

Nevertheless, the problem remains very challenging in theory and in practice. For the popular OWL Web Ontology Language (based on DLs), it is still unknown if the problem is decidable [Rudolph and Glimm, 2010]. For existential rules, which are syntactically closer to CQs, query answering is a basic reasoning task, but it is also undecidable. At the same time, existential rules are too weak to capture the non-deterministic features of ontology languages like OWL.

In this work, we study existential rules with disjunction, which generalise many expressive ontology languages. Our results apply to DLs (and OWL) and many rule languages.

Example 1. The following rules capture basic part-whole relationships (meronomy) and disjunctive information.

Similar modelling can be found, e.g., in many medical ontologies. This particular example can also be expressed in OWL.

The oblivious chase provides a sound and complete reasoning algorithm for this logic [Bourhis et al., 2016], computing rule entailments in a bottom-up fashion and branching on disjunctive choices. Unfortunately, the chase often fails to terminate. In Example 1, each bicycle introduces a new wheel (1), which could be a spoke wheel (2), which may introduce a new bicycle (3) - an infinite chain of bikes and wheels. To avoid this, we define a restricted chase that tries to reuse existing elements before introducing new ones.

However, the restricted chase may still fail to terminate, and determining this is undecidable in general [Beeri and Vardi, 1981]. We therefore develop new acyclicity criteria that can ensure termination in the spirit of previous approaches for rules without disjunctions [Marnette, 2009; Kr¨otzsch and Rudolph, 2011; Cuenca Grau et al., 2013]. Existing notions can actually be applied to disjunctive rules by replacing ∨ with ∧ for testing acyclicity. However, this only works for an oblivious chase, where non-termination is preserved if rules are logically strengthened. Our restricted chase is more challenging, since additional entailments can lead to termination. Indeed, the restricted chase terminates for Example 1 since rule (3) never needs to be applied to a wheel that was newly introduced by rule (1). Without the rules (4) and (5), this would not be true, and an infinite chase would be required. Only Carral et al. [2016] seem to have studied this setting so far, but their results are specific to the non-disjunctive DL Horn-SRIQ and do not apply to existential rules.

Acyclicity is sufficient but not necessary for termination. In experiments, we are often left with a significant amount of non-acyclic ontologies of which we cannot say anything. We therefore also develop a cyclicity notion to detect nontermination of the restricted chase. To the best of our knowledge, this is the first proposal for such a criterion. It allows us to show that a majority of practical ontologies is such that the chase will either terminate over all possible sets of input facts, or will necessarily be infinite over at least some inputs.

In summary, our main contributions are:

• we propose restricted joint acyclicity as a simple criterion for restricted chase termination on disjunctive rules,
• we design more general criteria by extending modelfaithful acyclicity and model-summarising acyclicity,

• we characterise the complexity of query answering and of checking acyclicity for each of the new notions,
• we introduce the first criterion for checking nontermination of the restricted chase,
• we empirically evaluate our results on a large corpus of real-world ontologies.

Experiments suggest that our new notions can significantly improve over the state of the art, and that a large subset of non-acyclic ontologies are indeed cyclic. Our treatment is fully self-contained, but a technical report with full formal details can be consulted if desired [Carral et al., 2017].

2 Preliminaries

We consider a standard first-order signature based on mutually disjoint, countably infinite sets of constants C, function symbols F, variables V, and predicates P. Every function symbol or predicate f has an arity ar(f) ≥ 0. Terms are built from C, V, and F as usual. We write lists of variables 〈x1, . . . , xn〉 as x, and similarly for term lists t. We treat such lists as sets when order is irrelevant. We will use function symbols only to represent auxiliary terms introduced during reasoning (via skolemisation; see below). An atom is a formula p(t) with p ∈ P and ar(p) = |t|. A term or formula is ground if it contains no variables. A fact is a ground atom. A disjunctive existential rule, or simply rule, is a formula

where n ≥ 1, and where B (the body) and Hi (the heads) are non-empty conjunctions of atoms that contain only variables from x ∪ y and x ∪ vi, respectively, and no constants or function symbols. We omit the universal quantifiers when writing rules. The variables x are called frontier variables. A rule is deterministic if n = 1 and nondeterministic otherwise; it is generating if it contains an existential variable and non-generating otherwise. When convenient, we treat conjunctions, such as B and Hi, as sets of atoms.

We consider finite sets of rules R, where we assume without loss of generality that each variable in R occurs only in the scope of a single quantifier within a single rule (‡). An instance I is a finite set of function-free facts. A program is a pair 〈R, I〉 with R a rule set and I an instance.

A Boolean conjunctive query (BCQ) is a formula ∃v.Q[v], where Q is a conjunction of function-free, constant-free atoms using only variables from v. A program 〈R, I〉 entails a BCQ ∃v.Q[v] if ∧ R ∧ ∧ I |= ∃v.Q[v] under standard first-order semantics. It is well known that arbitrary conjunctive query answering can be reduced to BCQ entailment.

A (ground) substitution σ is a partial function from variables to (ground) terms. We denote finite substitutions as [x1/t1, . . . , xn/tn] or [x/t], and we set σ(x) = x if σ is undefined for x. Given a term or formula F, we write Fσ for the expression obtained by concurrently replacing all unbound occurrences of variables x in F by σ(x).

The skolemisation sk(ρ) of a rule ρ as in (6) is the formula ∀x, y. (B[x, y] → ∨ni=1 sk(Hi)[x]) where sk(Hi) is obtained from Hi by replacing each variable v ∈ vi by the term fv(x), where fv is a fresh skolem function symbol specific to v (which, by (‡), occurs in only one quantifier).

The Restricted Chase We consider a restricted version of the disjunctive chase [Bourhis et al., 2016], where rules are only applicable if their heads are not satisfied by existing facts. Moreover, we impose an order of rule applications that defers the use of generating rules.

Definition 1. Consider a rule ρ of form (6), a ground substitution σ defined exactly on the variables x ∪ y from ρ, and a set of facts F. Then 〈ρ, σ〉 is applicable to F if (a) F |= Bσ, and (b) F ̸|= ∨ni=1 ∃vi.Hiσ. In this case, the result of applying 〈ρ, σ〉 to F is the set {F ∪ sk(H1)σ, . . . , F ∪ sk(Hn)σ}, consisting of all sets of facts obtained from F by adding the skolemised, σ-instantiated atoms of some head of ρ.

Note that condition (a) is the same as Bσ ⊆ F, while (b) states that there is no extension ˆσ of σ to the variables vi such that Hiˆσ ⊆ F, for any i ∈ {1, . . . , n}. The chase is the result of a possibly infinite process of recursive rule applications:

Definition 2. A chase tree of 〈R, I〉 is a (possibly infinite) tree; each node is labelled by a set of facts, such that:

1. the root is labelled with I,
2. if a node labelled F has n children labelled F1, . . . ,Fn, then there is a rule ρ ∈ R and substitution σ such that {F1, . . . , Fn} is the result of applying 〈ρ, σ〉 to F,
3. if a node α is labelled with F and 〈ρ, σ〉 is applicable to F, then each path starting from α contains a node in which 〈ρ, σ〉 is no longer applicable due Definition 1 (b),
4. generating rules are only applied in a nodewhere no nongenerating rule of R is applicable.

The result of a restricted chase is the (possibly infinite) set of all (possibly infinite) sets of facts that are obtained as the union of all set of facts along some path.

Condition (3) ensures fair, exhaustive application, while (4) improves the rule application strategy to reduce the amount of applicable generating rules. Bourhis et al. [2016] omit (4) and Definition 1 (b), but restricted disjunctive chase algorithms were considered before, e.g., by Deutsch and Tannen [2002].

Example 2. Consider the rules in Example 1, where we use first letters to abbreviate predicates from now on, and the instance {B(c)}. We obtain a finite chase tree with two leaves F1 = {B(c), hP(c, fv(c)),W(fv(c)), pO(fv(c), c), SW(fv(c))} and F2 = {B(c), hP(c, fv(c)), W(fv(c)), pO(fv(c), c),DW(fv(c))}. In particular, rule (3) is not applicable to F1, since the facts pO(fv(c), c) and B(c) already satisfy the head of this rule for the substitution [x/c].

In general, the chase tree and even its result is not unique, since the order of rule applications may matter, but we get the following consequence of well-known results:

Fact 1. A program 〈R, I〉 entails a BCQ ∃v.Q iff F |= ∃v.Q holds for all sets of facts F in the result of an (arbitrary) restricted chase.

If the chase terminates, the chase tree is finite, and the result is the set of all (finite) leaf labels. In this case, Fact 1 leads to a decision procedure for BCQ entailment. Unfortunately, chase termination is undecidable even for deterministic rules [Beeri and Vardi, 1981]. We therefore study sound but incomplete tests for restricted chase termination.

3 Restricted Joint Acyclicity

We first consider a limited but easy-to-check condition to ensure chase termination. As noted in the introduction, we could apply existing criteria for the deterministic skolem chase, but the result is often unsatisfactory:

Example 3. On the skolemisation of the rules in Example 1, the oblivious chase may produce an infinite set of facts {hP(c, fv(c)), W(fv(c)), pO(fv(c), c), SW(fv(c)), pO(fv(c), fw(fv(c))), B(fw(fv(c))), hP(fw(fv(c)), fv(c)), hP(fw(fv(c)), fv(fw(fv(c)))), W(fv(fw(fv(c)))), . . .}. Definition 1 (b) does not reduce the derivable facts, since the presence of one skolem term does not allow us to omit the introduction of another skolem term.

To address such cases, we extend the notion of joint acyclicity (JA), proposed by Kr¨otzsch and Rudolph [2011] for deterministic rules. JA proceeds in two steps: (1) for each existential variable v, we compute a set Ωv of predicate positions, to which values generated for v might propagate; (2) we build a dependency graph to show if the value generated for a variable v may participate in the generation of a new value for a variable w. A rule set is JA if this graph has no cycles. To adapt this idea to the restricted chase, we treat ∨ as ∧ for (1) and add a new blocking criterion for (2). For the next definition, recall assumption (‡) from Section 2.

Definition 3. A position in a predicate p is a pair 〈p, i〉 with i ∈ {1, . . . , ar(p)}. A term t occurs at position 〈p, i〉 in a formula ϕ if ϕ contains an atom p(s) with si = t. Given a rule ρ and variable z, a body position (head position) of z is a position in the body (in a head) of ρ at which z occurs.

For a rule set R and an existential variable v of R, a set Ωv of positions is defined recursively: (i) Ωv contains all head positions of v in a rule of R; (ii) for every universally quantified variable x in R, if Ωv contains every body position of x, then Ωv also contains every head position of x.

Example 4. For the rules of Example 1, we obtain Ωv = {〈hP, 2〉, 〈W, 1〉, 〈SW, 1〉, 〈DW, 1〉, 〈pO, 1〉} and Ωw = {〈pO, 2〉, 〈B, 1〉, 〈hP, 1〉}.

For a set of facts F and set of rules R, let Rdng(F) be the set of facts obtained from F by exhaustive application of all deterministic, non-generating rules of R. For an existentially quantified variable v, let Hv denote the (unique) head conjunction v occurs in, and let Bv be the body of the corresponding rule.

Definition 4. The restricted dependency graph of a rule set R has the existentially quantified variables of R as its nodes, and an edge v → w if w occurs in a rule ρw of form (6) with a frontier variable x ∈ x such that

• (a) all body positions of x occur in Ωv, and
• (b) for the set F = (Bw ∪ Hv[v/x] ∪ Bv)σ, where σ replaces all variables z by distinct constants cz, we have Rdng(F) ̸|= (∃w.Hw)σ.

R is restricted jointly acyclic (RJA) if its restricted dependency graph has no cycles.

Example 5. We consider Example 1 and rename variables by subscripting rule numbers. The existential dependency graph has nodes v and w. For the potential edge v → w, condition (a) of Definition 4 is satisfied for rule (3) and variable x3, since 〈SW, 1〉 ∈ Ωv (see Example 4). However, the set F of condition (b) is {SW(c3), B(c1), hP(c1, c3),W(c3)} and the application of deterministic, non-generating rules (4) and (5) yields Rdng(F) = F ∪ {pO(c3, c1)}, which satisfies rule (3). Hence, there is no edge v → w. A similar argument rules out w → v. For v → v and w → w, condition (a) is not satisfied. The graph therefore has no edges and the rule set is RJA.

RJA rules lead to a finite chase tree. The following property is the essence of this claim.

Lemma 2. If the restricted chase tree of 〈R, I〉 contains a term fw(t) where ti = fv(s) for some i ∈ {1, . . . , |t|}, then there is an edge v → w in the restricted dependency graph.

Proof. We denote rules etc. as in Definition 4, and assume that fw(t) was derived by applying 〈ρw, θ〉. The sets Ωv overestimate the possible positions of fv-terms, hence the applicability of ρw to fv(s) implies Definition 4 (a). Moreover, let Fw be the set of facts as it was when ρw was applied in the chase tree. There is a homomorphism h : F → Fw with h(Bwσ) = Bwθ and h(Bvσ) the premise of the application of ρv that produced fv(s). By our chase strategy, Rdng(Fw) = Fw. Hence, if Rdng(F) |= Hwσ, then Fw |= h(Hwσ) = Hwθ, such that 〈ρw, θ〉 would not be applicable. Since it is, we get Rdng(F) ̸|= Hwσ as claimed.

Theorem 3. Deciding BCQ entailment for programs 〈R, I〉 where R is RJA is coN2EXPTIME-complete, even if the arity of predicates is bounded.

Proof sketch. Membership follows since BCQ nonentailment can be shown by finding a model of 〈R, I〉 that does not satisfy the query. For this we may nondeterministically guess a branch of the chase tree. The maximal nesting depth of function terms in the chase tree is bounded by the number of existentially quantified variables in R, since a greater depth can only be achieved by repeating a function symbol, which would make the restricted dependency graph cyclic by Lemma 2. The maximal number of terms of linear depth is doubly exponential, so there are double exponentially many possible ground facts overall. A set of facts of this size can be computed in 2EXPTIME.

Hardness is established by modifying the construction of a 2EXPTIME Turing machine given for deterministic, weakly acyclic rules by Cal`ı et al. [2010]. The construction yields a grid of doubly exponential size, using predicates of arity ≤ 3. Using disjunction in rules, it is not hard to simulate a nondeterministic Turing machine in the same way.

Theorem 4. Deciding if R is RJA is EXPTIME-complete, coNP-complete if the arity of predicates is bounded, and Pcomplete if the number of variables per rule is bounded.

Proof. Sets Ωv can be computed in polynomial time, and there are only polynomially many possible edges and body variables x as in Definition 4 to be considered. However, Definition 4 (b) corresponds to the EXPTIME-complete Datalog reasoning task of checking non-entailment of a set of facts [Dantsin et al., 2001]. The task becomes coNP-complete for predicates of bounded arity: hardness follows from hardness of conjunctive query entailment (rule bodies are CQs); membership follows since there are only polynomially many ground facts over this signature, hence the derivation of any such fact can be represented as a polynomial directed acyclic graph with (true) facts as nodes and edges connecting premises with conclusions, such that fact entailment can be checked by guessing this graph and verifying each rule application. The task becomes P-complete for bounded numbers of variables, since grounding (instantiation of rules with constants) polynomially reduces fact entailment to propositional Horn logic entailment. In all cases, detecting cycles in the (polynomial) dependency graph is possible in P.

4 RestrictedModel-Faithful Acyclicity

Since RJA is not sufficient to capture all realistic cases, we develop more general, though also more complex, criteria.

Example 6. We extend Example 1 with the following rules:

The resulting rule set still leads to a finite restricted chase for all instances, but it is not RJA. Indeed, the restricted dependency graph contains a cycle v → u → z → v. For example, when considering z → v, the set F in Definition 4 (b) is {B(c1), pO(c7, c1), S(c7)}, which cannot entail W(c1).

For cases as in Example 6, we extend the notion of modelfaithful acyclicity (MFA) [Cuenca Grau et al., 2013]. To determine if a set of deterministic rules R is MFA, one computes the chase on 〈sk(R), I ⋆R〉, where I ⋆R is the critical instance, which contains all possible ground facts based on predicates of R and the single constant symbol ⋆. R is MFA if this chase terminates without introducing a cyclic term f(t), which is such that f occurs in the terms t. Alternatively, a cyclic term must appear after at most doubly exponentially many steps. Deciding MFA indeed is 2EXPTIME-complete.

MFA uses the fact that the chase terminates on every instance if it terminates on the critical instance. This is not true for the restricted chase, as no rule is applicable in the presence of the critical instance. We therefore consider a relaxed condition of applicability, which, in the spirit of Definition 4 (b), determines a rule's applicability from a smaller set of facts not including the whole critical instance. The body of the rule (instance) that is to be applied can always be assumed as given. Further facts can be obtained from this body's skolem terms, since each skolem function is introduced by one specific rule:

Definition 5. For a rule set R and a ground term t=fv(s) using skolem functions from sk(R), the set Ft contains all ground facts involved in the derivation of facts containing t:

1. Let B[x, y] → ∨i ∃vi.Hi[x, vi] be the unique rule that contains v in head disjunct Hk, and consider the substitution θ = [x/s, y/c], where c is a list of fresh constant symbols not used elsewhere. Then Bθ ∪ sk(Hk)θ ⊆ Ft.
2. For every functional term sj ∈ s, we have Fsj ⊆ Ft.

Example 7. For the rules from Examples 6 and 1, and term t = fu(fv(b)), we have Ft = {SW(fv(b)), hP(fv(b), t), S(t)}∪Ffv(b) with Ffv(b) = {B(b), hP(b, fv(b)), W(fv(b))}.

The next example illustrates another difficulty: even if we only take a rule's body into account to check its applicability, we might get much fewer derivations on the critical instance than on other instances.

Example 8. Consider the rule ρ : p(x, y) → ∃v.p(v, v) ∨ ∃w.p(y,w). On the critical instance, one could try to apply ρ with substitution [x/⋆, y/⋆]. But already the instantiated body p(⋆, ⋆) prevents the application of ρ, since p(⋆, ⋆) |= ∃v.p(v, v). The restricted chase terminates immediately. Yet, on the instance {p(a, b)}, one can compute an infinite set of facts {p(a, b), p(b, fw(b)), p(fw(b), fw(fw(b))), . . .}, so the restricted chase is not finite in general.

To handle this issue, we rename distinct occurrences of ⋆.

Definition 6. Consider a rule ρ : B[x, y] → ∨i ∃vi.Hi[x,vi], and a ground substitution σ defined exactly on x∪y. Let σ′ be such that, for all x ∈ V, σ′ (x) is σ(x) with each occurrence of a constant renamed so that no constant occurs more than once in the image of σ′ . The set Bρ,σ is the union of Bσ′ and each of the sets Ft for which there is a skolem term t in Bσ′ . We say that 〈ρ, σ〉 is blocked if Rdng(Bρ,σ) |= ∨i ∃vi.Hiσ′ .

Example 9. Consider the rules of Example 6, and especially rule ρ of (8) under substitution [x7/t] with t = fu(fv(b)). Intuitively speaking, t represents a spoke that was introduced as part of wheel fv(b), which in turn is part of bicycle b. We want to show that ρ does not need to be applied to introduce another bicycle fz(t). We do not need to rename any constants here, so Bρ,σ = {S(t)} ∪ Ft with Ft as in Example 7. While Bρ,σ does not satisfy the head of ρ yet, we get Rdng(Bρ,σ) = Bρ,σ ∪ {hP(b, t), pO(t, fv(b)), pO(fv(b), b), pO(t, b)}. Therefore Rdng(Bρ,σ) |= ∃z.pO(t, z) ∧ B(z) and 〈ρ, σ〉 is blocked as expected.

Our adaptation of MFA conducts a (deterministic) chase on the critical instance, but applies rules only if not blocked.

Definition 7. For a rule set R, RMFA(R) is the least set of facts for which I ⋆R ⊆ RMFA(R) and, whenever ρ :B→ ∨i ∃vi.Hi is a rule in R, and σ is such that Bσ ⊆ RMFA(R) and 〈ρ, σ〉 is not blocked, then sk(H1)σ ∪ . . . ∪ sk(Hn)σ ⊆ RMFA(R). R is restricted model-faithfully acyclic (RMFA) if RMFA(R) does not contain a cyclic term.

Example 10. The rules of Examples 1 and 6 together are RMFA, as one can easily check along the lines of Example 9.

Theorem 5. Deciding if R is RMFA is 2EXPTIME-complete even if the arity of predicates or the number of variables per rule is bounded. It is EXPTIME-complete if each rule contains at most one frontier variable.

Proof sketch. Membership in 2EXPTIME follows as in Theorem 3 by bounding the possible ground skolem terms. Similarly, rules with one frontier variable lead to unary skolem functions, which can form only exponentially many terms.

2EXPTIME-Hardness can be shown as for the case of MFA, where it was done by reduction from the 2EXPTIMEhard problem of BCQ entailment checking for weakly acyclic

(WA) rules [Cuenca Grau et al., 2013]. The hardness proof for WA in turn is based on a direct Turing machine construction using predicates of bounded arity and rules with a bounded number of variables [Cal`ı et al., 2010]. One may verify that no rule application is ever blocked in this particular construction, so that we can use the same proof for our purposes. EXPTIME-hardness can be obtained using a known proof for the case of MFA, which exhibit the same complexity for small frontiers [Cuenca Grau et al., 2013]. In particular, their construction in Lemma 59 works even when using blocking.

Lemma 6. Let π⋆ be the function that maps a term t to the term obtained from t by replacing all constants with ⋆. Then, for every term t that occurs in any restricted chase of 〈R, I〉 for any instance I, the term π⋆ (t) occurs in RMFA(R).

Proof sketch. We can show that π⋆ is a homomorphism from any leaf of the chase tree into RMFA(R). This is done by induction following the rule applications of one branch of the restricted chase. The main observation is that, if 〈ρ, σ〉 is applicable to a set of facts F during the restricted chase, and we define σ⋆ (z) = π⋆ (σ(z)), for all z, then 〈ρ, σ⋆ 〉 is not blocked. This in turn is shown by finding a homomorphism fromRdng(Bρ,σ⋆) (Definition 6) into F.

Theorem 7. Deciding BCQ entailment for programs 〈R, I〉 where R is RMFA is coN2EXPTIME-complete, even if the arity of predicates is bounded.

Proof sketch. The proof is similar as for Theorem 3. By Lemma 6, any chase derives at most doubly exponentially many facts, since this is the maximal number of non-cyclic terms, and π⋆ preserves non-cyclicity. Hardness follows by Theorem 3, as any RJA rule set can be shown to be RMFA (cf. the relation of JA and MFA [Cuenca Grau et al., 2013]).

Theorem 5 motivates the search for a simpler test that still extends RJA. We can achieve this by adapting modelsummarising acyclicity (MSA) to our setting [Cuenca Grau et al., 2013]. This criterion resembles MFA in that a chase on the critical instance is conducted to discover cycles. However, instead of using skolem terms, existential variables now are replaced by fresh constants, and cycles are tracked explicitly during the chase instead of using cyclic terms. Definition 6 can remain unchanged if we treat the fresh constants as nullary "skolem" function symbols in Definition 5 (the recursive case (2) for subterms becomes irrelevant).

Definition 8. For a rule set R, let S be a binary predicate not used in R, and let θ be a substitution that maps each existentially quantified variable v in R to a unique fresh constant cv. RMSA(R) is the least set of facts for which I ⋆R ⊆ RMSA(R) and, whenever ρ : B[x, y] → ∨n i=1 ∃vi.Hi[x, vi] is a rule in R, and σ is such that Bσ ⊆ RMSA(R) and 〈ρ, σ〉 is not blocked, then H1θσ ∪ . . . ∪Hnθσ ∪ {S(xσ, vθ) | x ∈ x, v ∈ vi, 1 ≤ i ≤ n} ⊆ RMSA(R).

R is restricted model-summarising acyclic (RMSA) if RMSA(R) does not contain a directed cycle of S-relations.

BCQ answering remains as hard as for RJA and RMFA, but recognising RMSA is only as hard as for RJA. The proof is similar to the proofs of Theorems 4 and 5.

Theorem 8. Deciding if R is RMSA is EXPTIME-complete, and P-complete if the number of variables per rule is fixed.

Example 11. RMSA cannot capture Example 6, but it generalises RJA. Consider the set R of the rules (1), (2), (7), and

R is RMSA since rule (10) is never applicable to fresh constants (which do not have parts that are bicycle chains). However, R is not RJA since (10) leads to 〈Bicycle, 1〉 ∈ Ωv.

5 Proving Nontermination

Even if rules are not acyclic by any of our criteria, they might still have a finite chase. In this section, we introduce a complementary criterion that is sufficient (but not necessary) to show that the chase will be infinite. By combining this with our previous acyclicity notions, we hope to decide the question of chase termination for most practical ontologies.

Sufficient conditions for nontermination can also look for cycles, e.g., by detecting cyclic terms in a chase as done for MFA. The critical instance cannot be used here, since it overestimates what can really be derived repeatedly. However, a cyclic term fv(. . . fv(t) . . .) might indicate nontermination if it was derived in a chase that started from nothing but the facts Bv∪sk(Hv), where we replace each variable z by a fresh constant cz (Bv and Hv are the unique body and head for v as in Section 3). Indeed, if this happens, then each application of the rule of v creates a set of facts that eventually enables another application of the same rule that will produce a skolem term of increased nesting depth. This discussion suggests a criterion for showing nontermination of the skolem chase:

Definition 9. Consider a set R of deterministic rules, and a rule ρ : B[x, y] → ∃v.H[x, v] in R. The set Iρ is obtained from B∪sk(H) by replacing all occurrences of every variable z with a fresh constant cz. Let Fρ be the set of facts obtained by exhaustive application of rules from sk(R) to Iρ, under the condition that no rule is applied to facts with a cyclic term. Then R has a ρ-cycle if there is a variable v ∈ v such that Fρ contains a cyclic term fv(. . . fv(t) . . .). R is model-faithful cyclic (MFC) if it has a ρ-cycle for a generating rule ρ ∈ R.

Excluding facts with cyclic terms in the computation of Fρ is necessary to ensure termination, since otherwise that chase might be infinite although none of the cyclic terms have the form fv(. . . fv(t) . . .) with v ∈ v. With this restriction, however, MFC can be checked in 2EXPTIME.

Example 12. The rules in Example 1 are MFC if we replace ∨ by ∧ to make them deterministic. Let ρ be rule (1). Then Iρ = {B(c), hP(c, fv(c)),W(fv(c))} and Fρ contains the facts SW(fv(c)), pO(fv(c), fw(fv(c))), B(fw(fv(c))), and hP(fw(fv(c)), fv(fw(fv(c)))), which has a cyclic term.

Theorem 9. If R is MFC, then there is an instance I for which the chase of 〈sk(R), I〉 is infinite.

Unfortunately, the approach of performing a chase on minimal sets of facts fails when the application of rules can be prevented by the presence of additional facts. We therefore perform an additional applicability check for the restricted chase. Recall that I ⋆R denotes the critical instance for R.

Definition 10. Consider a set R of deterministic rules, a rule ρ : B[x, y] → ∃v.H[x, v] ∈ R, and a ground substitution σ on x∪y. Let σ⋆ be such that σ⋆ (z) is σ(z) with all constants replaced by ⋆ for all z ∈ V. Let R⋆ be R with existential quantifiers omitted and existential variables replaced by ⋆, and let ρ⋆ ∈ R⋆ be the rule obtained from ρ.

We define Iρ,σ,R = I ⋆R ∪ Bσ⋆ ∪ ⋃t∈(x∪y)σ⋆ Ft. The set Uρ,σ,R is obtained by exhaustive application of rules from R⋆ to Iρ,σ,R, with the exception of the rule ρ⋆ under substitution σ⋆ . Then 〈ρ, σ〉 is unblockable for R if Uρ,σ,R ̸|= ∃v.Hσ⋆ .

Intuitively speaking, Uρ,σ,R represents a gross overestimation of what might be derivable in a situation ρ is applicable.

Lemma 10. Consider the chase tree for a program 〈R, I〉, let F be the label of some node n in this tree, and let R∧ be R with ∨ replaced by ∧. If ρ : B[x, z] → ∃v.H[x, v] is a deterministic rule in R, F |= Bσ, and 〈ρ, σ〉 is unblockable for R∧, then 〈ρ, σ〉 is applied in a node above or below n.

Proof sketch. For a contradiction, suppose that the preconditions hold but 〈ρ, σ〉 is not applied. Since applications are fair, Definition 1 (b) is violated in all leaf nodes below n. For any such leaf n′ labelled F ′ , we map F ′ to Uρ,σ,R as follows: every term t in Bσ⋆ (including subterms) is mapped to itself; all other terms are mapped to ⋆. One can show by induction over the chase of F ′ that this is a homomorphism. Since 〈ρ, σ〉 is not applicable to F ′ , we find Uρ,σ,R |= ∃v.Hσ⋆ .

Definition 11. For a set R of rules and a rule ρ ∈ R, we define Iρ and Fρ as in Definition 9, but with the additional restriction that the computation of Fρ uses only applications of deterministic rules that are unblockable for R∧, obtained from R by replacing ∨ with ∧.

As before R has a restricted ρ-cycle if there is a variable v ∈ v such that Fρ contains a cyclic term fv(. . . fv(t) . . .). R is restricted model-faithful cyclic (RMFC) if it has a ρ-cycle for some generating rule ρ ∈ R.

Theorem 11. If R is RMFC, then there is an instance I for which the restricted chase of 〈R, I〉 is infinite.

6 Evaluation

To evaluate the effectiveness of our criteria, we have used MOWLCorp, a large corpus of real-world OWL ontologies [Matentzoglu and Parsia, 2014; Matentzoglu et al., 2013], which we transformed into rules. To this end, we first normalised ontologies by structural decomposition of complex axioms, and then rewrote axioms into first-order logic to obtain rules. We refer to Cuenca Grau et al. [2013] for details on this standard process; our normal forms are as in their Table 1 but with an added form A1 ⊓ . . . ⊓ An ⊑ B1 ⊔ . . . ⊔ Bm.

We excluded ontologies with nominals (oneOf) and atmost-restrictions (maxCardinality) since they require equality reasoning. There are well-known techniques for this [Cuenca Grau et al., 2013], but they are not our focus. We then considered all ontologies with up to 1,000 existential quantifiers after normalisation, leading to a set of 1,576 ontologies.

We have implemented tests for RMSA, RMFA, RMFC, MSA, and MFA using RDFox [Motik et al., 2014] as a rule engine. The creation of new terms during the chase and our blocking conditions are implemented on top of RDFox. For MSA and MFA, we replaced ∨ by ∧ in all ontologies. We treat ⊤ (universal class) and ⊥ (empty class) as regular unary predicates, and we modify our tests to ensure that all elements are always in ⊤; likewise for the universal and the empty property. We have not implemented RJA since we found the more general RMSA to perform well.

Table 1 shows our results for ontologies without (top) and with (bottom) disjunctions, grouped by their number of existential axioms (#∃). The column "#" gives the number of ontologies per group; "open" counts ontologies that are neither RMFA nor RMFC. We can see that RMSA performs better than MFA, while (R)MFA hardly improves over (R)MSA. Using MFA, chase termination remains open for 602 ontologies overall (38.2%). The combination of RMFA and RMFC reduces this number to 250 (15.8%). As expected, many ontologies are indeed cyclic, but there are also an additional 85 that are acyclic (14.1% of the formerly open ones). In the deterministic case, our notions perform rather well and allow us to characterize 96.3% ontologies as acyclic or cyclic.

7 Conclusion

To the best of our knowledge, this is the first systematic study of termination of the restricted chase on existential rules (with disjunctions) and the first ever approach to restricted chase nontermination. We have shown our criteria to be theoretically and empirically more general than previous notions, deciding termination for 84.2% of the tested ontologies.

Our work motivates and enables further research on chasebased reasoning procedures. Many tableau-based OWL reasoners already implement chase-like algorithms that could be a starting point. In a test with a modified version of HermiT [Motik et al., 2009], we have already answered queries over an acyclic, non-Horn ontology with tens of thousands of facts. We believe this is a highly promising direction in description logics ontologies and existential rules alike.

Acknowledgements

This work was supported by the DFG within the cfaed Cluster of Excellence, CRC 912 (HAEC), and Emmy Noether grant KR 4381/1-1.