Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies

1.1 Chase Termination and Acyclicity Notions

• Existing acyclicity notions estimate whether rules can repeatedly trigger generating rules; their applicability tests can overestimate rule applicability and fail to detect chase termination.Joint acyclicity, for example, can miss that simultaneous satisfaction of all body atoms prevents a rule from applying.Source: §1.1 · p. 2

1.2 Applications of Acyclicity Notions

• Materialisation-based OWL 2 reasoners often restrict ontologies to OWL 2 RL for termination, excluding generating rules, while acyclicity can support complete materialisation of Horn ontologies.Some systems support generating rules ad hoc, without completeness and/or termination guarantees.Source: §1.2 · p. 3

1.3 Our Contributions

• MFA checks whether rules are acyclic using their canonical model and is 2ExpTime-complete to check, or ExpTime-complete when predicate arity is bounded; MSA checks are ExpTime-complete, or coNP-complete with bounded arity.MSA checking is connected to entailment of ground atoms in datalog programs.Source: §1.3 · pp. 3–4
• MFA and MSA strictly subsume known logic-programming acyclicity notions, MSA is strictly more general than SWA, and the paper completes the taxonomy of relative expressiveness.Both notions apply to general existential rules without equality; equality can be handled through singularisation.Source: §1.3 · p. 4
• Refined singularisation gives practically useful upper and lower bounds for acyclicity checks, and its lower bound coincides with WA when used with JA.Singularisation transforms rules to encode equality; it is nondeterministic, so some transformations may yield acyclic rules while others are not guaranteed to.Source: §1.3 · p. 4
• Acyclicity makes CQ answering easier for Horn-SROIF and Horn-SHIF ontologies, and acyclic unions of Horn ontologies with SWRL rules preserve decidability and worst-case complexity.For Horn-SROIF, CQ answering is ExpTime-complete; for Horn-SHIF, it is PSpace, compared with ExpTime-complete answering for general Horn-SHIF ontologies.Source: §1.3 · p. 4
• Many of 336 tested Horn ontologies are MSA, some complex ones are MSA but not JA, and materialised universal models are typically not too large.The results suggest principled materialisation-based reasoning beyond OWL 2 RL may be practically feasible.Source: §1.3 · p. 4

2.1 First-Order Logic

• The paper uses standard first-order logic conventions, including equality interpreted as identity unless stated otherwise.It distinguishes terms contained in an atom from terms that occur as subterms.Source: §2.1 · p. 5

2.2 Rules and Queries

• A conjunctive query is an existentially quantified conjunction of atoms; an answer maps its free variables to constants, and is tested by entailment from rules and an instance.The paper assumes query and instance predicates occur in the rules, and excludes equality from rule bodies and queries.Source: §2.2 · p. 6

2.3 The Skolem Chase

• The Skolem chase applies skolemised rules iteratively; a query answer holds exactly when the resulting chase entails that query instance.Skolemisation preserves conjunctive-query answers, and termination of the Skolem chase also guarantees termination of the nonoblivious and core chases.Source: §2.3 · p. 7, §2.2 · p. 7

2.4 Acyclicity Notions

• Weak acyclicity excludes cycles through special edges in its position graph, while joint acyclicity excludes cycles in a graph of existential variables and applies only to equality-free rules.Joint acyclicity generalises weak acyclicity.Source: §2.4 · pp. 8–9

2.5 Rule Normalisation

• Normalisation replaces a body or head conjunction with an atom using a fresh predicate; the resulting rules preserve answers to queries that omit those predicates.Structure sharing allows a predicate introduced in one step to be reused in later steps.Source: §2.5 · p. 9

3. Novel Acyclicity Notions

• MFA addresses the high cost of checking a very general notion with MSA, a stricter notion that gives the same results on most existing ontologies.The section also notes that joint acyclicity relaxes weak acyclicity, which may be too strict for applications.Source: §3 · p. 10

3.1 Limitations of Existing Acyclicity Notions

• Joint acyclicity rejects rules equivalent to common ontology axioms even when their chase terminates, because it estimates applicability without checking all body atoms together.In the example, the chase terminates because a required B fact is absent, although the JA dependency graph contains a self-loop.Source: §3.1 · pp. 10–11

3.2 Model-Faithful Acyclicity (MFA)

• MFA declaratively tracks rule dependencies against the universal model and identifies acyclicity when the transformed rules do not entail C, guaranteeing termination of skolem, nonoblivious, and core chase.MFA is semantic and can be checked with any sound and complete first-order calculus; the example’s rules are universally MFA.Source: §3.2 · pp. 11–12
• MFA characterizes chase derivations without cyclic terms, and its skolem chase terminates in double exponential time, placing BCQ answering for MFA rules in 2ExpTime.The passage also states that CQ answering for MFA rules is not harder than for weakly acyclic rules.Source: §3.2 · pp. 12–14
• Checking MFA for a specific instance is in 2ExpTime, while checking universal MFA is 2ExpTime-hard.The paper relates query answering for certain rules to universal MFA checking to establish these complexity bounds.Source: §3.2 · p. 14
• For unrestricted rules, deciding MFA relative to an instance is in 2ExpTime, while deciding universal MFA is 2ExpTime-hard, even with bounded predicate arity.The high checking cost is attributed to unbounded function-symbol arity and cyclic terms whose depth can be linear in the rule set.Source: §3.2 · p. 15, §3.3 · p. 17
• For ∃-1 rules, MFA checking is in ExpTime, universal MFA checking is ExpTime-hard, and BCQ answering under MFA is ExpTime-complete.For unrestricted rules, MFA checking is in 2ExpTime and universal MFA checking is 2ExpTime-hard, even with bounded predicate arity.Source: §3.2 · pp. 15, 17

3.3 Model-Summarising Acyclicity (MSA)

• MSA reuses rule-specific constants for existential variables instead of generating deep terms, making its transformed rules equivalent to datalog rules.MSA checking is in ExpTime and universal MSA checking is ExpTime-hard; with bounded predicate arity, the respective bounds are coNP and coNP-hard.Source: §3.3 · pp. 17–18
• Every MSA rule set is MFA, but the inclusion is strict: an example is universally MFA and not universally MSA.The implication also holds relative to an instance.Source: §3.3 · p. 19

3.4 Acyclicity Notions and Normalisation

• Normalisation preserves MFA, and an example shows it can turn a nonterminating chase into a set of rules that is even JA.The preservation claim depends on technical assumptions about equality handling.Source: §3.4 · pp. 19–20
• Normalisation can harm universal termination: a universally MFA rule set can yield a normalised set whose chase does not terminate on the critical instance.The stated termination guarantee for the normalised set applies to inputs using only predicates from the original rule set.Source: §3.4 · p. 20

• MFA and MSA generalise most of the known acyclicity notions.Source: §4 · p. 20
• The paper investigates the relative expressiveness of MFA, MSA, and the other known acyclicity notions.Source: §4 · p. 20
• Relationships among the many proposed acyclicity notions had been only partially investigated.Source: §4 · p. 20

4.1.1 Super-Weak Acyclicity

• SWA builds a rule-dependency graph from variable-place flows and declares a rule set acyclic when that graph has no cycles.Its Move sets capture how existentially generated values can flow to positions of body variables shared with a rule head.Source: §4.1.1 · p. 21
• MSA is strictly more general than SWA, while SWA is strictly more general than joint acyclicity.The paper also notes that SWA and JA differ only when a body variable occurs more than once in a rule.Source: §4.1.1 · pp. 21–23

4.1.2 Acyclicity by Rewriting

• Adn-WA adorns predicate positions before testing weak acyclicity, but examples show it and MFA are incomparable.The paper also leaves some broader relationships among adorned notions unresolved, including whether strict inclusions are preserved by adornment.Source: §4.1.2 · pp. 23–25

4.1.3 Monitor Graph

• Monitor graphs track chase steps: an infinite chase yields cycles of arbitrary length, while ruling out a fixed cycle length guarantees termination.Unlike semantic MFA, this approach is tied to the nonoblivious chase, whose result depends on rule-application order.Source: §4.1.3 · p. 25

4.2 Acyclicity in Knowledge Representation

• A rule set can be aGRD but not SWA: the example establishes no self-dependency even though SWA rejects the set.The argument uses that the instance contains only constants, so a fact with a functional term cannot supply the required second trigger.Source: §4.2 · p. 26
• The dependency relation partitions rules into strongly connected components, each checked against X unless it is a singleton rule that does not depend on itself.This special case ensures that aGRD is included in X≺ for any X.Source: §4.2 · pp. 26–27
• For any X contained in SWA, adding rule dependencies yields a strictly stronger notion X≺, while MSA does not contain aGRD.The paper attributes the latter non-containment to the optimisation in its dependency definition.Source: §4.2 · p. 27
• MFA≺ coincides with MFA, so combining dependencies with any notion contained in MFA remains within MFA.Theorem 32 states this for an arbitrary rule set and instance.Source: §4.2 · pp. 28–29
• The paper distinguishes its dependency relation from nonoblivious-chase dependency notions, which are tied to that chase variant and its rule-application strategy.For the cited notions, Deutsch et al.'s criterion guarantees a finite nonoblivious chase sequence, while Meier et al.'s guarantees all such sequences are finite.Source: §4.2 · p. 30

4.3.1 Finite Domain Notion

• WA is strictly contained in FD: every WA rule set is FD, and an example is FD but not WA.FD uses finite-domain positions defined through recursive relationships in the WA dependency graph.Source: §4.3.1 · pp. 31–32

4.3.2 Argument-Restricted Rule Sets

• Argument-restricted rule sets have finite skolem chases on arbitrary instances, and AR is strictly contained in JA.The paper gives an example that is JA but not AR.Source: §4.3.2 · pp. 32–33
• FD is strictly contained in AR; the paper also notes that λ-restricted and ω-restricted programs fall within both FD and AR, and thus within JA.The example establishing FD ⊊ AR provides an argument ranking despite failing the FD conditions.Source: §4.3.2 · p. 33
• Γ-acyclicity for existential rules marks positions safe using FD positions and rule-dependency conditions, then requires the affected-position propagation graph to have no cycle with a special edge.The simplified notion reuses rule dependencies and omits machinery for functional terms in rule bodies, yielding a slightly stronger version for existential rules than Greco et al. (2012).Source: §4.3.3 · p. 34
• FD is strictly contained in ΓA, aGRD is contained in ΓA, and ΓA≺ is contained in AR≺.The example used for FD ⊊ ΓA has all positions safe but is not FD.Source: §4.3.3 · p. 35
• Counterexamples show ΓA≺ is strictly contained in AR≺, ΓA is not contained in MSA, and WA≺ is not contained in ΓA.These examples qualify the containment relationships among the acyclicity notions.Source: §4.3.3 · p. 36
• In another example, PosS(Σ)=PosFD(Σ), yet affected positions R|2, T|1, and T|2 yield a propagation-graph self-loop at T|2, so Σ is not ΓA.Source: §4.3.3 · p. 37
• ΓA≺ is strictly contained in AR≺; the examples also show AR≺ is not contained in ΓA≺.The rule-dependency-based safe-position condition weakens on rules occurring on cycles, allowing ΓA≺ to be subsumed by AR≺.Source: §4.3.3 · p. 37
• Example 45 is ΓA and aGRD but not MSA, JA, AR, or FD, establishing ΓA is not contained in MSA, SWA, JA, AR, or FD.Source: §4.3.3 · p. 37
• Example 46 is WA≺ but not ΓA: every position is affected, so its propagation graph equals WA(Σ).Its rule-dependency relation has two strongly connected components, each WA; all positions are recursive with themselves, leaving PosFD(Σ) and PosS(Σ) empty.Source: §4.3.3 · p. 37

4.4 The Landscape of Acyclicity Notions

• JA≺ is strictly contained in SWA≺, but SWA is not contained in JA≺.The rule set from Example 20 supplies the separation.Source: §4.4 · p. 38
• Examples show MSA≺ strictly contains SWA≺, while MFA strictly contains MSA≺.The cited examples also establish that MSA is not contained in SWA≺ and that MSA≺ is strictly contained in MFA≺.Source: §4.4 · p. 38
• Neither aGRD nor FD is contained in Adn-WA, as shown by the rule set from Example 22.That rule set is both aGRD and FD.Source: §4.4 · p. 38
• The landscape is complete: every displayed inclusion is strict, and missing paths indicate non-containment.A notion reachable from another by directed arcs is strictly more general.Source: §4.4 · p. 38

5. Handling Equality via Singularisation

• Explicitly axiomatizing equality can cause skolem-chase equalities to proliferate, while WA and MFA are incomparable with equality because WA uses the nonoblivious chase and canonical representatives.The example rules are WA but not WA when equality is explicitly axiomatized; the skolem-chase termination results apply to equality-free rules or rules with explicit equality axioms.Source: §5 · p. 39
• Singularisation replaces equality with an equivalence-relation predicate, omits replacement rules, and modifies rule bodies; its chase yields a universal model that supports equivalent conjunctive-query answering.The transformed chase is not itself a model of the original rules, and the transformation is nondeterministic because different markings can produce different outcomes.Source: §5 · pp. 39–41
• JA∀ coincides with WA, whereas X∀ is properly contained in X∃ for X in {MFA, MSA, JA}, so the choice of marking can affect singularised acyclicity.For the example, one singularisation does not universally terminate under the skolem chase, while another is JA.Source: §5 · p. 41
• Markings that agree on relevant variables produce the same chase and preserve JA, MSA, and MFA; the resulting Sing∪ construction is a lower bound on X∀ and is linear in rule count when rules have at most one relevant variable.In general, Sing∪ has size exponential in the maximum number of relevant variables in a rule; for DL-derived rules with at most one relevant variable per rule, it is linear in the size of Σ.Source: §5 · pp. 43–44
• MFA∪, MFA∃, and MFA∀ are 2ExpTime-complete, while MSA∪, MSA∃, and MSA∀ are ExpTime-complete.Source: §5 · p. 44
• Without structure sharing, an MFA marking for the original rules can be extended to one for rules after a single normalisation step; the section warns that this does not hold with structure sharing.Source: §5 · pp. 44–45
• The proof shows that if u is cyclic and µ(u) is defined, then µ(u) is cyclic as well.The proof also establishes that µ is defined for every term in I∞, with the function symbols hy occurring only inside terms of the form hy(s, g1(s, t)).Source: §5 · p. 46
• Normalisation with structure sharing can leave no marking that makes the singularised rules MFA, so it must be used with care when handling equality.Structure sharing reduces the available markings, which can make it impossible to find one that yields acyclic rules.Source: §5 · p. 47
• In the example, Sing(Σ, M) is MFA, but neither alternative marking M1 nor M2 is MFA, and structure sharing makes every marking fail.The example shows that normalisation with structure sharing prevents any marking M′ from making the singularised rules MFA with respect to I.Source: §5 · p. 47

6. Applying Acyclicity to Horn Description Logics

• Horn TBoxes can be normalized in linear time as model-conservative extensions, and the paper identifies each TBox with its corresponding existential rules.Horn-SROIF provides the formal underpinning for a prominent subset of OWL.Source: §6 · pp. 48–49

6.1 Acyclic Horn-SROIF TBoxes

• For Horn-SROIF, MFA checking and BCQ answering under MFA are ExpTime-complete; the section overview places both problems in PSpace for Horn-SHIF.The Horn-SROIF hardness stems from Type 6 axioms, which can encode exponential non-tree-like structures.Source: §6.1 · pp. 49, 53, §6 · p. 49
• Even beyond Horn-SROIF’s global conditions, including with added SWRL rules, acyclic ∃-1 rule sets retain ExpTime MFA checking and BCQ answering.This result applies to universal or instance-relative MFA checking.Source: §6.1 · p. 53
• For Horn-SROIF, checking MSA w.r.t. an instance is in PTime because the resulting rules have bounded variables and predicate arities.These bounds make the chase polynomial in size.Source: §6.1 · pp. 53–54

6.2 Acyclic Horn-SHIF TBoxes

• The Horn-SHIF polynomial-space argument handles equality through an explicit axiomatisation; extending it to singularised rules is left open.Singularised rules may require non-local matching, and their chase can be exponential in size.Source: §6.2 · p. 55
• For Horn-SHIF TBoxes that are MFA w.r.t. an instance, BCQ answering is PSpace-complete, with hardness established by reduction from QBF validity.The polynomial-space upper bound uses a tracing technique that handles transitive roles in queries.Source: §6.2 · pp. 54–55
• The proof’s model-checking procedure uses polynomial space by checking rule satisfaction locally around central variables and keeping only polynomially sized interpretations at each recursion level.Its recursion depth is the number of function symbols; the MFA membership adaptation examines models to depth n+1.Source: §6.2 · p. 57
• For Horn-SHIF TBoxes, checking MFA with respect to an instance is in PSpace, while universal MFA checking is PSpace-hard.The membership proof adapts the earlier algorithm to inspect models to depth n+1 for n function symbols while still using polynomial space.Source: §6.2 · p. 57
• Checking whether a Horn-SHI TBox is universally MSA is PTime-hard, giving a matching lower bound for Theorem 62.The hardness proof reduces Horn propositional entailment and uses a Horn-SHI TBox that is universally MFA exactly when it is universally MSA.Source: §6.2 · p. 58

7.1 Acyclicity Tests

• 213 of 336 ontologies (63.4%) were MSA, and MFA and MSA classifications coincided across all 336 tests.The corpus included 49 Gardiner ontologies, 208 OBO ontologies, and LUBM; Table 2 summarizes the results.Source: §7.1 · p. 59, Table 2 · p. 60
• Ontology versions sometimes changed classification: five older OBO versions were MSA while their newer versions were not MFA.Conversely, two older versions were not MFA while their newer versions were MSA.Source: §7.1 · p. 59
• 15 large OBO ontologies were MSA but not JA, suggesting MSA is useful on complex ontologies.The authors attribute this to MSA analysing implications between existentially quantified variables more precisely than previously known notions.Source: §7.1 · p. 60, Table 3 · p. 61

7.2 Materialisation Tests

• Depth tests finished for 207 of 213 MSA ontologies; 123 (59.4%) had depth below 5.Tests were aborted if they did not finish within three hours.Source: §7.2 · p. 60
• Materialisation took 2 seconds for LUBM and produced 231,200 new facts; kmi-basic-portal took 0.03 seconds and produced 744 new facts.The tests estimated fact growth rather than implementation performance; most test ontologies did not contain many facts.Source: §7.2 · pp. 60–62
• For 123 ontologies with depth below 5, materialisation increased ontology size by a factor of 8.This supports the authors’ conclusion that materialisation may be feasible for many ontologies, especially those with relatively small depths.Source: §7.2 · p. 62, Table 4 · p. 62

8. Conclusions

• The paper proposes MFA and MSA as sufficient conditions for skolem-chase termination and establishes tight complexity bounds for membership checking and query answering over acyclic rules.Source: §8 · p. 62
• MFA and MSA generalise most previously considered acyclicity notions, within a complete taxonomy of their relative expressiveness.The paper also establishes tight membership-checking and conjunctive-query-answering complexity bounds for MFA and MSA.Source: §8 · p. 62
• Optimisations to Marnette’s singularisation technique can often reduce the number of acyclicity checks for existential rules containing equality.The stated aim is to make singularisation more suitable for practical use.Source: §8 · p. 62
• For acyclic DL ontologies, query answering can be computationally easier; acyclic results also permit arbitrary SWRL rules in Horn ontologies without changing decidability or worst-case query-answering complexity.These results concern the stated condition that the result is acyclic.Source: §8 · pp. 62–63
• Experiments found many commonly used ontologies acyclic and materialisation fact-count increases manageable, suggesting materialisation-based ontology reasoning is practically feasible and useful.The study investigated whether acyclicity notions support principled extensions of materialisation-based reasoners with existential quantification.Source: §8 · p. 63
• Extending these acyclicity notions to general logic programs remains future work, with function terms in rule bodies and nonmonotonic negation presenting technical difficulties.The paper also identifies modularly combining approaches to these concerns as a possible direction.Source: §8 · p. 63