Paper deep dive
Stratified Negation in RDF Rules: A Correct Approach (Extended Version)
Nils Küchenmeister, Alex Ivliev, Dörthe Arndt, Markus Krötzsch
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 89%
Last extracted: 8/3/2026, 2:10:36 AM
Summary
The paper addresses the challenge of combining RDF rule languages (like N3 and SHACL Rules) with default negation, noting that existing stratification methods fail due to the lack of predicate-level information in triples and complications arising from blank nodes (existential variables). The authors propose 'chain stratification,' a new condition that guarantees a well-behaved, unique, and lean semantics for RDF rules with negation. This approach uses an analysis of multistep derivations (trails) and integrity constraints to discard impossible cases, ensuring that rule application order respects dependencies and avoids negative feedback cycles.
Entities (12)
Relation Signals (11)
Chain Stratification → handles → Default Negation
confidence 95% · chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation
Chain Stratification → solves → RDF Rules
confidence 95% · we propose chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation
N3 → istypeof → RDF Rule Language
confidence 92% · rule languages, such as N3 or SHACL Rules
SHACL Rules → istypeof → RDF Rule Language
confidence 92% · rule languages, such as N3 or SHACL Rules
Existing Methods → failsfor → RDF Rules
confidence 90% · Existing methods to stratify negation often fail for RDF rules
Chain Stratification → guarantees → Unique RDF Graph
confidence 90% · guaranteed to derive an RDF graph that is unique, lean, and justified
Chain Stratification → guarantees → Lean RDF Graph
confidence 90% · guaranteed to derive an RDF graph that is unique, lean, and justified
Chain Stratification → handles → Blank Nodes
confidence 90% · Blank nodes in rule heads further complicate the matter... To solve these open problems, we propose chain stratification
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Combining RDF rule languages, such as N3 or SHACL Rules, with default negation is challenging. Existing methods to stratify negation often fail for RDF rules, since individual triples do not carry enough information to meaningfully restrict potential dependencies. Blank nodes in rule heads further complicate the matter, since the order of rule applications may determine whether new values are created, which in turn can change the applicability of rules with negation. To solve these open problems, we propose chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation, and existential rules in general. Our condition combines an elaborate analysis of potential multistep derivations with a mechanism for using integrity constraints to discard impossible cases. Applying rules in any order that respects chain stratification is guaranteed to derive an RDF graph that is unique, lean, and justified under the usual negation-as-failure semantics. To show the practicality, we also provide a prototype implementation.
Tags
Links
- Source: https://arxiv.org/abs/2607.28778v1
- Canonical: https://arxiv.org/abs/2607.28778v1
Trouble viewing inline? Open PDF directly →
Full Text
119,992 characters extracted from source content.
Expand or collapse full text
threeinline]sparql 11institutetext: Knowledge-Based Systems Group, TU Dresden, Dresden, Germany 22institutetext: Computational Logic Group, TU Dresden / ScaDS.AI, Dresden/Leipzig, Germany 22email: firstname.lastname@tu-dresden.de Stratified Negation in RDF Rules: A Correct Approach (Extended Version)†thanks: This is the technical report accompanying our ISWC26 paper [KIAK:chains]. Nils Küchenmeister Alex Ivliev Dörthe Arndt Markus Krötzsch Abstract Combining RDF rule languages, such as N3 or SHACL Rules, with default negation is challenging. Existing methods to stratify negation often fail for RDF rules, since individual triples do not carry enough information to meaningfully restrict potential dependencies. Blank nodes in rule heads further complicate the matter, since the order of rule applications may determine whether new values are created, which in turn can change the applicability of rules with negation. To solve these open problems, we propose chain stratification as a robust new condition that guarantees a well-behaved semantics for RDF rules with negation, and existential rules in general. Our condition combines an elaborate analysis of potential multistep derivations with a mechanism for using integrity constraints to discard impossible cases. Applying rules in any order that respects chain stratification is guaranteed to derive an RDF graph that is unique, lean, and justified under the usual negation-as-failure semantics. To show the practicality, we also provide a prototype implementation. 1 Introduction The usefulness of rule languages for semantic web query answering, knowledge graph analysis, and ontological reasoning has long been recognised, and various rule engines now support RDF and SPARQL [N+15:RDFoxToolPaper, BSG:Vadalog18, Ivliev+:Nemo2024]. Attempts to establish corresponding web standards have been less successful [SWRL, RIF-overview], but ongoing works on N3 [n3-community-draft] and SHACL Rules [shacl12-rules] may yet change this. Even without standardised syntax, today’s rule languages share a common semantic basis — the classical language Datalog [Kroetzsch2025:Datalog] — which is intuitive and easy to implement, typically simply by applying rules until nothing new follows. Some useful features introduce complications though. A first case is that of non-monotonic operations, such as negation as failure and aggregation, the results of which may become invalid in the light of new data. A standard solution to this problem is to stratify (i.e., “order”) computation, so that non-monotonic operations are only applied to data that has been fully computed [Kroetzsch2025:Datalog]. This precludes feedback cycles from non-monotonic outputs to their own inputs. A second challenge is value invention where rules may lead to the creation of new elements, such that an infinite amount of new statements can be derived. In RDF, this is characteristic of rules with blank nodes (aka bnodes) in their conclusion; in databases and logic, existential quantifiers are used instead [BLMS11:decline]. A first mitigation is to create new bnodes only if the rule is not already satisfied by another element in place of the bnode, a method known as restricted (or standard) chase [DNR08:corechase]. Non-termination may still occur, and analysing rules to preclude (potential) feedback cycles can help detect such problems [BLMS11:decline, CG+13:acyclicity]. The working drafts for N3 [n3-community-draft] and SHACL Rules [shacl12-rules] combine non-monotonic features and value invention with a triple-based data model. Unfortunately, this leads to two major problems: (1) existing stratification and termination analyses fail in many cases, and (2) even if stratification succeeds, the rules may not have a well-defined semantics. Solving these will be our main contribution, but it is useful to first understand each problem in more detail. 1.0.1 Problem 1: Stratification fails with RDF rules. Traditional stratification is based on analysing dependencies between different predicates used in the rules. RDF does not have predicates, or, equivalently, has only a single predicate triple of arity three,111Such ternary predicates are also how relational rule engines import RDF [Ivliev+:Nemo2024]. Treating property names as binary predicates to represent RDF rules in Datalog would prevent the use of variables in predicate positions, as required for the RDFS rules. which means that any use of negation prevents stratification. SHACL proposes a refined unification-based dependency analysis [shacl12-rules, Section 3.4 “Stratification”], which helps when triples contain constants, as these N3 rules:222We use prefixes rdf:, rdfs:, and log: for the standard namespaces [rdf11-concepts, n3-community-draft]. ⬇ ?c :participant ?p => ?p rdf:type :Student. | rule_ex_intro_student| ?c :teacher ?p . [] log:notIncludes ?p rdf:type :Student => ?c :examiner ?p. | rule_ex_intro_negation| nthreelisting The rule in rule_ex_intro_student states that every participant ?p of some course ?c is a student. The rule in rule_ex_intro_negation means that course teachers who are not students are also examiners for the course, where [] log:notIncludes |$·s$| is N3 syntax for negation. SHACL’s stratification method orders rule_ex_intro_student before rule_ex_intro_negation, so that the negative precondition is only evaluated after inferring who is a student. Unfortunately, the approach breaks when adding further rules. For example, the following rules rdfs5 and rdfs7 are a standard way for handling subproperties in RDFS rdf11-semantics: nthreelisting ?p rdfs:subPropertyOf ?q . ?q rdfs:subPropertyOf ?r => ?p rdfs:subPropertyOf ?r. | rule_ex_intro_rdfs5| ?p rdfs:subPropertyOf ?q . ?x ?p ?y => ?x ?q ?y. | rule_ex_intro_rdfs7| nthreelisting The all-variable triples in rule rdfs7 ( rule_ex_intro_rdfs7) create dependencies from and to any other rule, making stratification impossible. Indeed, using all the rules rule_ex_intro_student– rule_ex_intro_rdfs7, there really are negative feedback cycles on valid input data, e.g., with the triple\\ :examiner rdfs:subPropertyOf :participant. In this case, a student might be discovered only after applying rule rule_ex_intro_negation. Similar issues would arise if :examiner were a subproperty of rdfs:subPropertyOf or rdf:type. These cases are unintended and would likely indicate errors, which N3 can express using constraints: nthreelisting :examiner rdfs:subPropertyOf :participant => false. | rule_constraint_teacher_participant| :examiner rdfs:subPropertyOf rdfs:subPropertyOf => false. | rule_constraint_teacher_spo| :examiner rdfs:subPropertyOf rdf:type => false. | rule_constraint_teacher_type| nthreelisting Negative feedback cycles are not possible without violating some of these constraints (which N3 tools would flag as an error), so the use of negation is safe now. Unfortunately, current stratification methods cannot detect this. Problem 2: Stratified RDF rules lack semantics. Bnodes require the existence of suitable elements, which may or may not need to be created. The next rule, e.g., states that humans must have some biological father who is male: nthreelisting ?x rdf:type :Human => ?x :father _:1 . _:1 rdf:type :Man. | rule_father| nthreelisting Given (a) :jo rdf:type :Human, applying rule_father creates a new value for _:1 (a fresh bnode in RDF, a labelled null in databases), but this should not happen if we already have (b) :jo :father :bob and (c) :bob rdf:type :Man. However, it is not always so easy to tell if a fresh bnode is necessary, and the decision can critically affect the result, as can be shown with some further rules [Ex.~6]KR20:cores: nthreelisting ?x :father ?y => ?y rdf:type :Man. | rule_father_male| ?x :father ?y => ?y :eq ?y. | rule_father_selfequal| ?x :father ?y1. ?x :father ?y2. [] log:notIncludes ?y1 :eq ?y2 => ?y1 :nef ?y2. | rule_different_fathers| nthreelisting rule_father_male defines a range for :father. rule_father_selfequal derives a simple equality, which is negated in rule_different_fathers to check for non-equal fathers ( :nef). Given triples (a) and (b), we could apply rule_father to create a fresh bnode _:a ( :bob does not satisfy the conclusion at this point). Rules rule_father_male and rule_father_selfequal would then produce (c), :bob :eq :bob and _:a :eq _:a, and rule_different_fathers would yield :bob :nef _:a and _:a :nef :bob. In contrast, if we apply rule_father_male first, then rule_father will not apply, and no :nef-triple follows. issue is serious: classically stratified RDF rule sets do not have a well-defined semantics. Indeed, rule_father– rule_different_fathers are stratified (by SHACL’s method), but stratification allows both of the above rule precedences. Other non-monotonic features, such as inequality or aggregation, can also expose the problem. might hope to avoid this issue by interleaving rule applications with additional algorithms to find and delete redundant bnodes, creating a lean RDF graph Hogan:LeanRDF:Tweb17 (or core DNR08:corechase). But even this (costly) workaround does not solve the problem: we can just apply rule_father_male last. As another solution, Krötzsch proposed a new type of dependency for rules with bnodes (existential variables) in their conclusion KR20:cores. His method can find a rule application order that leads to a lean graph and a well-defined result, but it also fails with rules like rdfs7 ( rule_ex_intro_rdfs7). Our proposed solution. We define a precedence relation on rules that can guide the order of rule applications so that negation-as-failure is justified and the inferred RDF graph is unique and lean (if the input data was). We start from Krötzsch’s reliances KR20:cores, recalled in the preliminaries (Section~ sec:prelim), which define several types of binary relations between rules to estimate potential interactions. generalise this approach based on two observations: (1) the transitive composition of reliances significantly overestimates which (problematic) interactions can occur in real sequences of rule applications, and (2) constraints and plain Datalog rules can effectively rule out problematic cases that would otherwise be allowed in RDF. The difficulty is to turn these into an implementable criterion, in particular (1), since there are infinitely many potential sequences of rules. In Section~ sec:trails, we introduce trails as a data-independent abstraction of such sequences, and show that it gives rise to a rule precedence with desirable properties. Since recognising trails is undecidable, we define chains as a decidable relaxation (Section~ sec:chains), which allows us to introduce chain stratification and to show that it meets our requirements (Section~ sec:chain-strat). this new form of stratification remains challenging, since chains can be arbitrarily long. By relating chains to words in a regular language, we finally obtain a decision procedure for chain stratification (Section~ sec:reg-lang). show its practical feasibility, Section~ sec:impl presents a prototype implementation that builds upon algorithmic methods for reliances GIKM2022, and an evaluation that shows applicability to rule sets with thousands of rules. Additional details and proofs can be found in the appendix, and our source code is included in the supplementary material statement at the end of this paper. show its practical feasibility, we provide a prototype implementation that builds upon algorithmic methods for reliances GIKM2022. Additional details and proofs can be found in the appendix see extended version of this paper at , and our source code is included in the supplementary material statement at the end of this paper. Preliminaries sec:prelim briefly define rules and recall required notions about reliances KR20:cores. We use first-order notation with predicates (not just triple) — our results apply to N3 (under common syntax translations existentialN3) but also to other rule languages RIF-overview,Ivliev+:Nemo2024,BSG:Vadalog18. Rules We use countably infinite, mutually disjoint sets $ $ ( predicates), $ $ ( variables), $ $ ( constants), and $ $ ( nulls). Each predicate $p∈ $ has an arity $ (p) 0$. An atom is an expression $p( t)$ with $p∈ $ and $ t∈( ∪ ∪ ) (p)$ a list. A fact is a variable-free atom, and a database is a set $ $ of facts. Negation is denoted $ $. We often treat lists and conjunctions of (negated) atoms as sets. For any expression or set of expressions $E$, $ (E)$ is the set of variables in $E$. rule $ρ$ is a null-free expression $ρ: (ρ) (ρ) ∃ z.\, (ρ)$, where $ z$ is a variable list, $ (ρ)$ and $ (ρ)$ are conjunctions of atoms, and $ (ρ)$ is a conjunction of negated atoms. Variables $ (ρ)= z$ are existential, all others $ (ρ)= (ρ) z$ are universal (as usual, we omit their quantifiers). Universal variables in $ (ρ)$ are frontier variables. All universal variables in $ (ρ)$ and $ (ρ)$ must occur in $ (ρ)$ ( safety). A rule $ρ$ is Datalog if $ (ρ)= $ and $ (ρ)= $. A ruleset $ $ is a finite set of rules; then $ $ is the subset of Datalog rules. Constraints as in rule_constraint_teacher_participant– rule_constraint_teacher_type are encoded in Datalog using a nullary head predicate $ $. We will discard cases where $ $ would be derived in our analyses, but not otherwise endow it with special logical semantics. Pieces A piece $ψ$ of $ (ρ)$ is a minimal non-empty set $ψ (ρ)$ such that $ (ψ)$ is disjoint from $ ( (ρ) ψ)$. Let $ (ρ) = \ ∃ (ψ).ψ ψ a piece of (ρ)\$, and $ ( ) = _ρ∈ (ρ)$. $ $ is piece-decomposed if each $ρ∈ $ has just one piece. example The rule $a(x) ,w.\,b(x),r(x,v),b(v),s(x,w)$ has three pieces: $b(x)$, $ .\,r(x,v),b(v)$ and $ .\,s(x,w)$. example Matches and models A substitution is a partial mapping $σ: →( ∪ ∪ )$. For $t∈ ∪ ∪ $, we set $tσ=σ(t)$ if $σ(t)$ is defined, and $tσ=t$ otherwise. Substitutions extend to (sets of) logical expressions as usual. Rule $ρ$ matches database $ $ if there is a substitution $ _∀$ defined on $ (ρ)$ such that $ (ρ) _∀ $ and $ (ρ) _∀∩ = $. We denote matches as pairs $ ρ, _∀$. Match $ ρ, _∀$ is satisfied by $ $ if there is a substitution $ _∃$ defined on $ (ρ)$ such that $ (ρ) _∀ _∃ $. $ $ is a model of $ρ$ (or satisfies $ρ$, written $ ρ$) if it satisfies all matches of $ρ$ over $ $. $ $ models a ruleset $ $ if $ ρ$ for all $ρ∈ $, and $ $ models a null-free database $J$ if $J $. The Chase Algorithms that construct models for a given database and ruleset are called chase procedures. We use the following standard chase: definition def:chase A chase $C$ for a null-free database $ $ and ruleset $ $ is a (possibly infinite) sequence of databases $ (C, 0), (C, 1), …$ such that $ (C, 0) = $ and: enumerate [(1)] it_chase_apply for each $i>0$, there is $ (C,i)∈ $ and $ (C,i)= (C,i), _∀$, such that (a) $ (C,i)$ is unsatisfied in $ (C,i-1)$, and (b) $ (C,i)= (C,i-1)∪\ ( (C,i)) _∀ _∃\$ for an injective function $ _∃: ( (C,i)) $ that maps variables to distinct fresh nulls (not occurring in $ (C,i-1)$); [(2)] if $ ρ,μ$ is a match over $ (C,i)$ for some $i 0$, then there is $j $ such that $ ρ,μ$ is satisfied in $ (C,j)$ (fairness). enumerate The set of chase steps is $ (C) $. The result of a chase is $ _C( , ) = _i∈ (C) (C,i)$. $C$ is generating if every $ (C,i)$ is a match in $ _C( , )$. definition In situations like it_chase_apply, we say $ (C,i)$ was obtained by applying $ (C,i)$ for $ _∀ _∃$. Many fair chase sequences may exist, based on the choice of rule applied in each step. If $C$ is generating, negated bodies of applied rules remain satisfied. If $ $ has no existentials, the results of generating chases are exactly the stable models KLS6:coloring-asp. If $ $ is Datalog, $ _C( , )$ is the unique perfect model, and we omit $_C$. , the chase result is the unique perfect model if $ $ is stratified: Let $ preds(A)$ be the set of predicates used in the set of atoms $A$, and for $ ∈\ +,- \$, let $ _ preds \ _1, _2 ∈ ^2 preds( ( _1)) ∩ preds( body ( _2)) ≠ \$. Then an existential-free ruleset $ $ is called (classically) stratified if it can be partitioned into $ = S_0 ∪ … ∪ S_n$ such that for all $ _i _i$ and $ _j _j$ we have that $ _i ^+_ preds _j$ implies $i $, and $ _i ^-_ preds _j$ implies $i < j$. Typically, it is also required that the sets of predicates $ _ρ _i preds( (ρ))$ defined by the strata $S_i$ are disjoint, which is inessential. $ $ is stratified iff $ ( ^+_ preds) ^-_ preds$ is acyclic. A chase exhaustively applying rules from the strata in order is clearly generating. are not so simple with $∃$ (cf.\ Section~ sec:intro, Problem~2). Universal models and cores Models with nulls are compared using homomorphisms (see KR20:cores for a definition). A model $U$ of $ $ and $ $ is universal if all other models $M$ of $ $ and $ $ have a homomorphism to $U$. Universality is the basis for answering monotonic queries DNR08:corechase. A core is a database without “redundant nulls”, which can be defined on finite databases $ $ by requiring that every homomorphism $ → $ is surjective (the infinite case is more subtle KR20:cores). The “minimality” of cores makes them useful for non-monotonic queries. A local criterion for a chase to yield a core is based on alternative matches: definition def:altM Let $ _a _b$ be databases, such that $ _a$ was obtained by applying $ρ$ for $μ$. A mapping $μ^A: (ρ)→ ∪ $ is an alternative match for $ ρ,μ$ over $ _b$ if (1) $ (ρ)μ^A _b$, (2) $xμ=xμ^A$ for all $x∈ (ρ)$, and (3) there is a null in $ (ρ)μ$ that is not in $ (ρ)μ^A$. An alternative match in a chase $C$ is one that uses $ _a= (C,i)$, $ρ= (C,i)$, and $ _b= _C( , )$. definition If a generating chase is finite and has no alternative matches, then it yields a core, but it is undecidable if such a chase exists [Thms~4~\&~11]KR20:cores. Moreover, rules rule_father– rule_different_fathers have generating chases $C$ and $C’$ where all databases $ (C^( ),i)$ are cores, but with non-homomorphic (hence non-universal) results. Decidable criteria for unique universal core models can be defined with rule precedences. Precedences A precedence for ruleset $ $ is a strict partial order $ × $. A chase $C$ violates $ $ if $ (C,i) (C,j)$ for some $i>j$. $C$ respects $ $ if, for every step $i$, $ (C,i)$ has no unsatisfied match $ ρ,μ$ with $ρ (C,i)$. This is different from “non-violating” since unsatisfied $ ρ,μ$ may become satisfied without $ρ$ being applied. Krötzsch defines precedences based on three types of reliance relations, which were shown to be efficiently computable GIKM2022. definition def:posr Rule $ _2$ positively relies on rule $ _1$, written $ _1 _2$, if there are databases $ _a _b$ such that $ _b$ was obtained from $ _a$ by applying $ _1$ for $ _1$, and there is an unsatisfied match $ _2, _2$ over $ _b$ that is not a match over $ _a$. definition definition def:negr Rule $ _2$ negatively relies on rule $ _1$, written $ _1 _2$, if there are databases $ _a _b$ such that $ _b$ was obtained from $ _a$ by applying $ _1$ for $ _1$, and there is an unsatisfied match $ _2, _2$ over $ _a$ that is not a match over $ _b$. definition definition def:restr Rule $ _1$ restrains rule $ _2$, written $ _1 _2$, if there are databases $ _a _b$ such that (1) $ _a$ was obtained by applying $ _2$ for $ _2$, (2) $ _b$ was obtained by applying $ _1$ for $ _1$, and (3) there is an alternative match $μ^A$ for $ _2, _2$ over $ _b$ that is not an alternative match over $ _b ( _1) _1$. definition intuition for these notions is that $ _1$ may produce an inference that is needed to match $ _2$ ($ $), prevents matching $ _2$ ($ $), or creates an alternative match for $ _2$ ($ $). A chase that does not violate $ $ is generating. A chase that does not violate $ $ has no alternative matches. ruleset $ $ is core stratified if the relation $ ∪ $ has no cycles through $ $, and fully stratified if $ ∪ ∪ $ has no cycles through $ ∪ $. For cases where a finite model exists, full stratification (which respects $ ( ) ( ∪ )$) yields a generating chase sequence that (if terminating) results in a uniquely determined core model, called the perfect core model KR20:cores. The conditions can be relaxed if negation is only used for some predicates EKM:ExNeg2022. Trails: Refining Transitive Positive Reliances sec:trails determine a precedence that yields a perfect core model, it is necessary to estimate when the application of one rule may cause a new unsatisfied match for another rule in the future. This may happen directly, as approximated with $ $, or possibly involve multiple intermediate steps. Previously, this was achieved by considering the reflexive transitive closure $ ( )$ of positive reliances KR20:cores, which is a coarse overestimation. A $ $-path does not detect whether the sequence of rule applications leading to a match implies that this match is always satisfied. This section aims to improve this by identifying a proper sub-relation of $ ( )$ that records the nuances of such multistep interactions. represent sequences of matches, we will use words over an infinite set of rule instances (individually denoted by $ $): equation ( ) \ ρθ ρ∈ , θ: (ρ)→( ( )) \ equation example ex:instances Below, rules $ _1, _2$ and $ _3$ on the left are shown with one of their (infinitely many) instances on the right: equation* arrayl|l _1\!: t(x,y,z), q(x,y) (x,z) \:&\: _1\!: t(x_1,y_1,x_1), q(x_1,y_1) (x_1,x_1) \\ _2\!: p(x,x) .\, s(x,v), t(v,v,v) \:&\: _2\!: p(x_1,x_1) _1.\, s(x_1,v_1), t(v_1,v_1,v_1) \\ _3\!: q(x,y), s(x,z), a(z) (x,x,z) \:&\: _3\!: q(x_1,y_1), s(x_1,v_1), a(v_1) (x_1,x_1,v_1) array equation* The rule instance $ _1$ was obtained from rule $ _1$ by applying the variable substitution $x θ x_1$, $y θ y_1$, $z θ x_1$, collapsing variables $x$ and $z$. will reuse these rules as a running example throughout Sections~ sec:trails– sec:chain-strat. example with a fixed arbitrary bijection $ω: ( ( )) ∪ $, each instance represents a match. Applying $ω$ to a set of atoms produces a database and, conversely, applying $ω^-1$ to a database yields a set of atoms. A sequence of matches $ _1, _1 , …, _n, _n $ is now represented by a word $ _1 _1ω^-1 … _n _n ω^-1$ over alphabet $ ( )$. As the chase algorithm always maps existentials to fresh nulls, we require these words to use fresh variables: definition def:exists-disjoint A finite sequence $( _i)_i=1,…,n ∈ ( )^*$ of rule instances $ _i ∈ ( )$ with pairwise disjoint existential variables is called $∃$-disjoint. definition example[ ex:instances] ex:exists-disjoint The sequence of instances $ _1 _2 _3$ is $∃$-disjoint, as the only existential variable $v_1$ is fresh in $ _2$. (It can be used universally again, as in $ _3$.) example a word indicates that the rule application corresponding to its first instance may indirectly cause a new unsatisfied match for the rule whose instance ends the word, if one can give a witnessing chase which applies the matches in the given order, such that each match directly requires the previous one. definition def:trail An $∃$-disjoint sequence of rule instances $t= _1,…, _n$ is a trail if there exists a generating chase sequence $C$, for which there is a strictly increasing function $f: [n] (C)$, such that for all $i∈ [n]$ itemize $ _i,ω = (C,f(i))$ and (match correspondence) $i>1$ implies $ ( _i)ω∩ ( _i-1)ω≠ $. (causal connection) itemize We write $ _1 _2$ if there is a trail from an instance of $ _1$ to an instance of $ _2$. definition , we have $ ( )$, as the databases $ _a= (C,f(i)-1)$ and $ _b= (C,f(i))$ witness the pairwise positive reliances for all $i$. example[ ex:exists-disjoint] ex:trail Let $c_x_1,c_y_1 ∈ $, $n_v_1 ∈ $, $x_1 ω c_x_1$, $y_1 ω c_y_1$, $v_1 ω n_v_1$. The $∃$-disjoint sequence $ _1 _2 _3$ is a trail, as there is a chase $C$ with equation* arrayl (C,0) = \ t(c_x_1,c_y_1,c_x_1), q(c_x_1,c_y_1) \ (C,1) = (C,0) ∪\ p(c_x_1, c_x_1) \ \\ (C,2) = (C,1) ∪\ s(c_x_1,n_v_1), t(n_v_1,n_v_1,n_v_1) \ \>\> (C,3) = (C,2) ∪\ a(n_v_1) \ \\ (C,4) = (C,3) ∪\ t(c_x_1,c_x_1,n_v_1) \ array equation* and step mapping $f: \1,2,3\ \1,2,3,4\$ with $1 1$, $2 2$, $3 4$, assuming a rule, e.g. $s(x,y) (y)$, to derive fact $a(n_v_1)$ in step $3$. Hence, $ _1 _3$. example restatabletheoremthmPosrTPrecNoViolate thm:posrT-prec-no-violate If $ ( ∪ )$ is a precedence (hence acyclic), then a chase that respects it does not violate it. In particular, it does not violate $ $ or $ $, and therefore is generating and free of alternative matches. restatable ~ thm:posrT-prec-no-violate can be shown by a contrapositive argument, where we take a chase that violates $ ( ∪ )$, inspect the first violation at chase step $i$ and argue that the chase must disrespect the precedence at $i$. The other properties follow from slight adaptations of known results on $ $ and $ $ KR20:cores. restatabletheoremthmPosrTPrecUniqeChaseResult thm:posrT-prec-unique-chase-result If $ ( ∪ )$ is a precedence, then the result of every chase of $ $ and $ $ that respects it is unique (up to isomorphism). restatable is shown by arguing that of two non-isomorphic chases, one must disrespect the precedence. A chase as in Theorem~ thm:posrT-prec-unique-chase-result is generating and free of alternative matches by Theorem~ thm:posrT-prec-no-violate. If finite, this unique result is a core [Theorem~11]KR20:cores, known as the perfect core model of $ $ and $ $. restatablelemmalemPosrTSmallest lem:posrT-smallest The $ $ relation is the smallest relation $<$, such that respecting $< $ ensures non-violation of $< $ for acyclic $< $ with $ $. restatable on proof of Theorem~ thm:posrT-prec-no-violate outlined above, this is shown by contradiction. Lemma~ lem:posrT-smallest therefore confirms that our choice of $ $ is optimal for our purposes. restatabletheoremthmTrailUndecidable thm:trail-undecidable For $ _1, _2∈ ( )$, it is undecidable whether $ _1 _2$ is a trail. restatable ~ thm:trail-undecidable is unsurprising, as chase termination is undecidable. Simulating the run of a Turing-machine with existential rules is a known technique that can be adapted such that the ruleset has a trail iff the TM halts. remark As a direct consequence of Theorem~ thm:trail-undecidable, it is also undecidable whether there is any trail starting and ending with instances of given rules, since that is already the case for only two instances. remark , we are looking for a decidable relation between $ $ and $ ( )$. Chains: A Decidable Approximation sec:chains Section~ sec:trails, $ $ is the smallest sub-relation of $ ( )$ that sufficiently captures when one rule application may enable another. We now develop a decidable overestimation of $ $ based on positive reliance checks. When checking $ $, it suffices to consider instances under $ω$, which leads to $ $ as a special case: definition def:direct-posr For $ _1, _2 ∈ ( )$, we write $ _1 _2$, if $ _1 _2$ with $ _a=( ( _1)∪( ( _2) ( _1)))ω$, and $ _1= _2=ω$. definition Above, database $ _a$ and matches $ _1$ and $ _2$ refer to Definition~ def:posr. example[ ex:trail] ex:direct-posr It is clear that $ _1 _2$, as $ _2,ω $ is no match on database $ _a = \ t(c_x_1, c_y_1, c_x_1), q(c_x_1, c_y_1) \$, but applying the unsatisfied match $ _1,ω $ yields $ _b = _a ∪\ p(c_x_1, c_x_1) \$ where $ _2,ω $ is an unsatisfied match. example is natural to ask if a sequence $c$ of instances — as a whole — can cause a new unsatisfied match $ ρ,μ $, i.e., if it can be extended by an instance $ ρμω^-1$. To determine this, we define a chain rule $ _c$ that is obtained from $c$ by combining all body atoms from the instances as well as all head atoms from all but the last instance $ _k$ into $ ( _c)$ and keeping the head of $ _k$ as $ ( _c)$. Any match for $ _k$ that arose due to prior applications of instances $ _1 … _k-1$ also satisfies the combined list of pre-conditions in $ ( _c)$. definition def:extend An $∃$-disjoint sequence of rule instances $c= _1,…, _k$ can be extended by $ ∈ ( )$ if $ _c $, where $ _c$ is the chain rule align eq:chain-rule ( _i∈ [k] ( _i) )∪ ( _i∈ [k-1] ( _i) ) ∃ ( _k) .\, ( _k) align definition definition def:chain An $∃$-disjoint sequence of rule instances $c= _1,…, _k$ is a chain if $k=1$ or, recursively, $ _1… _k-1$ is a chain that can be extended by $ _k$. definition example[ ex:direct-posr] ex:chain To see that $c = _1 _2 _3$ is a chain, check that $ _1$ is a chain of length $1$, $ _ _1 _2$ (see Example~ ex:direct-posr), and $ _ _1 _2 _3$ where the chain rule for $ _1 _2$ is $ _ _1 _2 : t(x_1,y_1,x_1), q(x_1,y_1), p(x_1,x_1) _1.\, s(x_1,v_1), t(v_1,v_1,v_1)$. example remark obs:trail-is-chain Every trail is a chain. remark it is easy to determine whether a given sequence of rule instances forms a chain, testing whether there is any chain between the instances of two rules is difficult, as chains can in principle grow arbitrarily long. We can, however, further restrict to certain chains: definition def:decoupled For a sequence $s= _1,…, _n$, the set of stale variables is: equation (s) _i,j∈ [n]. j<i ( ( ( _i) ( ( _i-1)) ) ∩ ( _j) ) equation If $ (s)= $, then $s$ is decoupled. definition Decoupled chains are special because the only variables re-used in the $i$th instance are frontier and existential variables stemming from the $(i-1)$th instance. example[ ex:chain] ex:decoupled The sequence $t= _1 _2 _3$ is not decoupled, as $y_1$ is re-used in $ _3$ although not present in $ ( ( _2))=\ x_1, v_1 \$ and thus $ (t)=\ y_1 \ ≠ $. example shows that trails are not always decoupled. We can, however, relate each trail to a decoupled chain. definition def:generalised A sequence $ ^A_1,…, ^A_n$ generalises a sequence $ ^B_1,…, ^B_n$ if there is a variable substitution $σ: → $, such that $ ^A_iσ= ^B_i$ for all $i∈ [n]$. definition example[ ex:decoupled] ex:generalised Any sequence of rule instances can be rewritten such that it is decoupled, by injectively replacing the stale variables with fresh ones. Consider $ _1 = _2 = $ and $ _3$ with $y_1 _2$. Then $c = ( _1 _1) ( _2 _2) ( _3 _3)$ is decoupled, and $c$ generalises $t$ with $σ= _1^-1 _2^-1 _3^-1$, which simply replaces $y_2$ by $y_1$. example restatablelemmalemTrailGenDecChain lem:trail-gen-dec-chain Every trail can be generalised by a decoupled chain. restatable ~ lem:trail-gen-dec-chain is shown by naming the trail’s stale variables apart, along the lines of Example~ ex:generalised. The resulting word may not be a trail any more, but is necessarily a chain. To show $ _ _1 _1… _k-1 _k-1 _k _k$ for all word positions $k$, we consider $ _a$ and $ _b$ obtained from the original trail’s witnessing chase and augmented with additional copies of facts under suitable renamings $ω^-1 _1ω$ up to $ω^-1 _kω$. example[ ex:generalised] ex:trail-gen-dec-chain Database $ _a$ from Definition~ def:direct-posr will, in addition to $q(c_x_1,c_y_1)$, contain a fact $q(c_x_1,c_y_2)$ matching $ ( _3 _3)$ with named apart variable $y_2$. example ruleset $ $, we collect all decoupled chains in set $ ( ) ( )^*$, which may be infinite. We write $ _1 _2$ if there is a decoupled chain between instances of $ _1$ and $ _2$. With Lemma~ lem:trail-gen-dec-chain, we know that indeed $ $, hence: corollary[of Theorem~ thm:posrT-prec-no-violate] cor:posrTc-restr-altM-free A chase that respects $ ( ∪ )$ does not violate $ $ or $ $, and therefore is generating and free of alternative matches. corollary , as the following example shows, there are decoupled chains that do not generalise any trail, i.e. $ ⊂ $ (the containment is proper). example[ ex:trail-gen-dec-chain] ex:dec-chain-not-gen-trail Recall that—in order to give the witnessing chase for the trail $t = _1 _2 _3$ in Example~ ex:trail—we had to assume the existence of a rule to derive a fact $a(n_v_1)$ after applying instance $ _2$, which invented the null $n_v_1$. This fact cannot originate from the input database, as it pertains to a null. If, however, the full ruleset were $ = \ _1, _2, _3 \$, $t$ would not be a trail (but still a chain). example $c= _1,…, _n$ is a chain, then $ _i _i+1$ for $i∈ [n-1]$, but the reverse does not hold, as attested below: The inclusion $ ⊂ ( )$ is proper. example ex:dl-posr-seq-not-chain Consider the rules $ _1 : r(x,y), a(y) (x)$, $ _2 : b(x) (x)$, and $ _3 : c(x) .\, r(x,v), a(v)$, which represent common types of ontological axioms. They are pairwise positively relying, i.e. $ _1 _2 _3$, but there are no instances thereof that would form a chain, as the way $ _1$ derives $b(x)$ ensures that $ ( _3)$ is already satisfied for any match of $ _3$ introduced by applying $ _1$ and then $ _2$. Therefore, the relation $ $ is indeed a proper sub-relation of $ ( )$. example Section~ sec:chain-strat we further refine the composition of $ $ with $ $ and $ $, and use it to introduce chain stratification. Afterwards, in Section~ sec:reg-lang, we examine how $ $ can be computed despite the fact that chains could be arbitrarily long. Rule Selection for Chain-Stratified Rulesets sec:chain-strat established that respecting $ ( ∪ )$ prevents violation of $ $ and $ $, we now take a closer look at the negative or restraint reliance after the chain’s last instance: We introduce relations $ ⊂ $ and $ ⊂ $, and use them to demarcate a class of rulesets which we call (fully) chain-stratified. These subsume fully stratified rulesets KR20:cores. definition def:restrC A chain $c = _1… _n$ restrains a rule $ρ$ if $ _c ρ$ where $ _c$ is the chain rule of $c$. If $ _1$ is an instance of $ _1∈ $, then we write $ _1 ρ$. definition , $ _1 ρ$ implies $ _1 ρ$, but the reverse does not hold: example[ ex:dec-chain-not-gen-trail] ex:restrC The last instance $ _3$ restrains both rules $ _4: p(x,x) . t(v,x,v)$ and $ _5: q(x,y) .\, t(x,y,v)$ but $ _c$ only restrains $ _5$. example $ $ still prevents $( )$-violations causing alternative matches. restatablelemmalemTrailRestrC lem:trail-restrC Let $t= _1… _n$ be a trail and $C$ a witnessing chase for $t$ with step mapping $f$. If there is a chase step $i < f(n)$, such that $ (C,i)$ has an alternative match over $ (C,f(n))$ but not over $ (C,f(n)-1)$, then $ _1 (C,i)$. restatable is shown by obtaining a pair of databases from the offending chase and applying Definition~ def:restr. Negative reliances are treated similarly: definition def:negrC A rule $ρ$ negatively relies on a chain $c = _1… _n$ if $ _c ρ$. If $ _1$ is an instance of $ _1∈ $, then we write $ _1 ρ$. definition restatablelemmalemTrailNegrC lem:trail-negrC Let $t= _1… _n$ be a trail and $C$ a witnessing chase for $t$ with step mapping $f$. If there is a chase step $i < f(n)$ such that $ (C,i)$ is a match for $ (C,i)$ over $ (C,f(n)-1)$ but not over $ (C,f(n))$, then $ _1 (C,i)$. restatable the above improvements, we can finally define our novel stratification condition, which we call chain stratification: definition def:chain-stratified A ruleset $ $ is core chain-stratified if $ , $ is acyclic. It is (fully) chain-stratified if $ , ∪ $ is acyclic. definition corollary[of Theorems~ thm:posrT-prec-no-violate and thm:posrT-prec-unique-chase-result, and Lemma~ lem:trail-gen-dec-chain] cor:core-chain-stratified On a chain-stratified ruleset the result of any chase that respects $ ∪ $ is generating, alternative match-free, and unique (up to isomorphism). If finite, it is a perfect core model. corollary chain-stratified rulesets, the rule precedence $ ∪ $ induces a “stratification” where rules may belong to multiple strata, obtained by first computing the minimum-rank layering $L_0…L_n$ of the precedence, and then forming strata $S_i = _j L_j$. Successively chasing fixpoints for $S_0…S_n$ ensures that no new unsatisfied matches for any $( ∪ )$-predecessors of $S_i$ are added. The Regular Language of Chains sec:reg-lang now address the issue of deciding whether there is an (arbitrarily long) decoupled chain connecting instances of two given rules. Enumerating the set $ ( )$ merely yields a semi-decision procedure, because a ruleset can have infinitely many chains. Therefore, we characterise $ ( )$ with a language $ ( )$ and establish that $ ( )$ is regular, which yields a decision procedure. Our restriction to decoupled chains (Section~ sec:chains) is essential for this to work. assign to each $c∈ ( )$ a label $ (c)∈ $ from some (yet to be defined) alphabet $ $. Intuitively, $ (c)$ captures all information needed for reliance checks between the chain rule $ _c$ and any rule from $ $, but in bounded space that does not grow arbitrarily with (the body of) $ _c$. This requires some auxiliary notation. For ruleset $ $, the finite set $ ( ) \ ρθ ρ∈ , θ: (ρ)→ ( ) \$ eq:variants is obtained by replacing variables in $ $ by any combination of variables found in $ $. Further, let $ : ( ) → ( )$ be an arbitrary but fixed mapping such that $ = ( ) _ ( )$ with injective variable renaming $ _ ( )$. example[ ex:instances] ex:variants Let $ = \ _1, _2, _3 \$. Then $ ( ) = \ x,y,z,v \$ and, e.g., $ ρ^a_1: t(v,z,y), q(v,z) (v,y)$ and $ ρ^b_1: t(x,y,x), q(x,y) (x,x)$ both are variants of $ _1$. In our example instance $ _1$ of rule $ _1$, the variables in the first and the third position of predicate $t$ are collapsed. So we can set $ ( _1) = ρ^b_1$ with the injection $ _ ( _1): x _1, y _1$, which yields $ _1 = ( _1) _ ( _1)$. example , given a set $F$ of formulae $∃ v.\, ψ$ where $ψ$ is a conjunction of atoms, let $ (F) \ ∃ v.\, ψ ∃ v.\, ψ , ψ ψ, ψ≠ , v= v∩ ( ψ) \$. example Consider the set $ ( ( ( )))$ of “partial pieces of rule variants.” The rule $a(x) .\, r(x,v), b(v)$ has a single piece, and contributes three partial pieces: (1) $ .\, r(x,v), b(v)$, (2) $ .\, r(x,v)$, and (3) $ .\, b(v)$. Another variant of the same rule is $a(x) (x,x), b(x)$, which has two partial pieces $r(x,x)$ and $b(x)$ (but not $r(x,x), b(x)$, which is no piece). example understand how we label a chain $c$, consider the chain rule $ _c$ and some rule $ρ∈ $. To check $ _c ρ$, Definition~ def:posr requires $ _a$ and $ _b$ such that: (i) the positive body of $ρ$ matches $ _b$ but not $ _a$ (i.e., $ _c$ contributed something relevant to $ _b$); (i) the negative body of $ρ$ is not matched in $ _b$; and (i) applying $ρ$ adds something over $ _b$ (match unsatisfied). To check these, we store three components: ($ $) pieces of $ _c$ that $ c$ontribute new facts when applying $ _c$ ($ $ (i)); ($ $) partial pieces $ s$atisfied after applying $ _c$ ($ $ (i)); and ($ $) variants of rules inhibited by $ n$egative body atoms after applying $ _c$ ($ $ (i)). we can define the finite alphabet $ 2^H ×2^F ×2 ( )$ where $H ( ( ))$ and $F (H)$. To define the labelling function $ $, consider a chain $c = _1… _n$ with chain rule $ _c$, and let $ _n _ ( _n)$, i.e., $ _n= ( _n) _n$. Moreover, let $ _c ( ( _c)∪ ( _c) ) _n^-1ω$, which represents the necessary facts in $ _b$ when checking $ _c ρ$ for any $ρ∈ $ (Definition~ def:posr), in the notation of Definition~ def:direct-posr with the fixed mapping $ω$. We define $ (c) = (c), (c), (c) $ where: align (c) & \ ∃ v. ψ ∈ ( ( _n)) ψ _n ( _c) \ eq:alpha-label\\ (c) & \ ∃ v. ψ _c ∃ v. ψ _∀\ eq:beta-label\\ (c) & \ ρ ∈ ( ) ( _c∪ ( ρ)ω ) ∩ ( ρ)ω≠ \ eq:gamma-label align where $ _∀$ is the restriction of $ω$ to universal variables. Note that $ (c)$ contains all head pieces of $ _c$ except possibly Datalog atoms. The main correctness property of $ $ is this: if $ (c_1)= (c_2)$ for chains $c_1$ and $c_2$, then for all $ρ∈ $ and all $ ∈\ , , \$, we have that $ _c_1 ρ$ iff $ _c_2 ρ$. For $ $, the proof of this claim establishes that the three label components can indeed be used as in the intuition given above. Cases for $ $ and $ $ are similar. We can then show: counterLemEquiLabelChains ( counterLemEquiLabelChains) restatablelemmalemEquiLabelChains lem:equi-label-chains Let $c_1,c_2∈ ( )$ with $ (c_1)= (c_2)$. If $c_1 _1∈ ( )$ then there is $ _2∈ ( )$ (both $ _1$ and $ _2$ belong to the same $ρ∈ $), such that center tabular*.8 @ l l l counterLemEquiLabelChains lem:equi-label-chains:1 $c_2 _2∈ ( )$ & and & counterLemEquiLabelChains lem:equi-label-chains:2 $ (c_1 _1)= (c_2 _2)$ . tabular* center counterLemEquiLabelChains0 restatable lem:equi-label-chains:1 largely follows from the correctness for $ $ by Definitions~ def:extend and def:chain. Part lem:equi-label-chains:2 is easy to see for $ $ and $ $; for $ $, it holds because $F$ is closed under $ ( (·))$ and the instances added to the end of the chains are decoupled. word function is $w: ( )→ ^*$ with $c (c)$ for $|c|=1$, $c (c_ ) (c)$ for $c=c_ _n$. The language of chains is $ ( )=\ w(c) ∈ ( ) \$. Now given two words $u,v∈ ( )$ with $u_|u| = v_|v|$, $uw∈ ( )$ implies $vw∈ ( )$ for any $w∈ ^*$, which follows from an inductive application of Lemma~ lem:equi-label-chains. An equivalence relation on words based purely on their last letter therefore fully characterises their extensions into longer words. By Myhill-Nerode, we find that: restatabletheoremthmLrRegular thm:LR-regular The language $ ( )$ is regular. restatable G_ rel -.5mu -.5mu ContinueContinue Andand Withwith Forfor: IfElseIfElseifthen :else ifelse algorithm[t] Is ruleset $ $ chain-stratified? alg:chains $ , , , $ *[r]compute the reliance graph $ $ has no cycle via $ ∪ $ “$ $ is fully stratified” $ ∪ $ *[r]precedence from $ $ (will approach $ ∪ $) $C \ ρ,ρ,ρ,ε ρ∈ $ and there is $ρ’∈ $ with $ρ’ ρ$ or $ρ’ ρ$ in $ \$; line_cinit\\ $ _1, _n, _c, w(c_ ) $ $ρ∈ $ $ _n ρ$ in $ $ $ _c ρ$ line_cloop $ $ is cyclic “$ $ is not chain stratified” line_return_false $ $ injectively rename $ρ$, such that it does not use $ ( _c)$;\\ $V ( ( _c) ∪ ( ))$;$ $ $C ( ( _c) ∪ ( ))$;\\ $η: V $ $ _cη η$ line_etaloop $ (cη) (c_ )$ line_norepeat $ _cη η ( ( _c)∪ ( _c)∪ ( ))η ∃ ( )η.\, ( )η$; line_chainrule\\ $C ∪\ _1, ρ, _cη η, w(c_ ) (cη) \$; line_addchain\\ $ρ’∈ $ $ρ ρ’$ in $ $ line_loop_restr $ _cη η ρ’$$ ∪\ _1, ρ’ \$ line_new_restr $ρ’∈ $ $ρ ρ’$ in $ $ line_loop_negr $ _cη η ρ’$$ ∪\ _1, ρ’ \$ line_new_negr “$ $ is chain stratified”; line_return_true algorithm Algorithm~ alg:chains outlines a procedure that uses these insights to check chain stratification. We represent chains $c= _1… _n$ as 4-tuples $ _1, _n, _c,w( _1… _n-1)$. We start with single-rule chains (line~A line_cinit) for rules in the range of $ $ or $ $; this suffices since we search for $ ∪ $-cycles and $ ∪ $ only ranges over such rules. We then iteratively extend $C$ and $ $ (A line_cloop) until a cycle is found (A line_return_false) or all chains have been considered and no cycle found (A line_return_true). For each $ _c ρ$, we consider all concrete mappings $η$ such that $ _cη η$ (A line_etaloop), if the $η$-specific chain’s label was not encountered yet (A line_norepeat). Since chains are extended step-wise, presence of a label in $w(c_ )$ means a label-equivalent chain was already considered (and all related restraints and negative reliances found). Then we construct the extended chain rule (A line_chainrule), add the new chain (A line_addchain, this adds to the cases iterated in A line_cloop), and add new pairs to $ $ (A line_loop_restr– line_new_negr). a hash set of seen chain labels and checking if labels of new chains are already present alleviates the need to store $w(c)$ as a whole. Chain labels can even be canonised, as Lemma~ lem:equi-label-chains generalises to chains with isomorphic labels. Further Improving Chain Stratification sec_refinements stratification generalises full stratification, which controls the interaction of value invention and negation, and solves, e.g., Problem~2 ( rule_father– rule_different_fathers) of Section~ sec:intro. Some generalisations, outlined next, allow us to cover more cases, e.g., Problem~1. Closure under constraints All reliances require a minimal set of facts (up to homomorphism), e.g., $ _a$ in Def.~ def:posr. If the Datalog rules $ $ entail $ $ on these facts, then the reliance can be discarded MKH13:reliances. For chains $c$, we could apply $ $ to $ _c$ (see Section~ sec:reg-lang), but for Algorithm~ alg:chains to be correct, we also must ensure that the label (not the specific chain) determines if $ $ is derived or not. therefore consider additional formulae $B$ to capture partial matches of Datalog rule bodies: $B (\ ∃ v .\, ( ρ) ρ ∈ ( )_D, v ( ρ) \)$. In $ (c)$, we will replace $ (c) $ eq:beta-label by $ _D(c) $. We convert sets $S $ to databases $ toDb(S) \ ψ _∀ _∃ ∃ v. ψ , _∃: v (v, ∃ v. ψ) \$, using the mapping $ω$ and an auxiliary injection $ : (S) ×S ( ( )ω)$. chain $c= _1… _n$ with $ _i _ ( _i)$, we recursively define $ _D(c)$, where we use $ Pre_c $ if $n=1$ and $ Pre_c toDb( _D( _1… _n-1))ω^-1 _n-1$ otherwise: align split _D(c) \ & ∃ v. ψ \\ & (( Pre_c ∪ ( _n) ∪ ( _n)) _n^-1ω, ) ∃ v. ψ _∀\ split align Compared to eq:beta-label, we replaced $ _c$ by a chase result based on the previous chain label and the new final rule, which has a homomorphism to $ ( _c, )$. Relying on the previous label lets us lift Lemma~ lem:equi-label-chains and related correctness results to $ _D$. We also recast the extended label as a rule: equation eq:chain-rule-dlclosure _c^D : toDb( _D(c))ω^-1 _n ( _n) ∃ ( _n) .\, ( _n) equation An $∃$-disjoint sequence $c$ can be extended by $ $ under constraints if $ρ^D_c $. It is a chain if $ ∉ (ρ^D_c)$ and Definition~ def:chain holds. We write $ _1 _2$ (respectively $ _1 _2$) if there is $c$ with $ρ^D_c _2$ (respectively $ρ^D_c _2$). definition def_chainstratRD $ $ is chain-stratified under constraints if $ ∪ $ is acyclic. definition ~ def_chainstratRD generalises chain stratification since only fewer chains are considered. Correctness is retained if the chase prioritises Datalog rules: corollary cor_chainstratRD If $ $ is chain-stratified under constraints, a chase that respects $ _D ∪ ∪( ×( ))$ is generating and alternative match-free. corollary relation $ _D$ is acyclic if $ ∪ $ is, since $ _D$ ranges over $ $. [1] _ #1 [1] _ #1 example ex_problem1_solved We return to Problem~1 ( rule_ex_intro_student– rule_constraint_teacher_type), denoting the respective rules $ rule_ex_intro_student, …, rule_constraint_teacher_type$. For $ =\ rule_ex_intro_student, rule_ex_intro_negation, rule_ex_intro_rdfs5, rule_ex_intro_rdfs7\$, we find reliances $ rule_ex_intro_student rule_ex_intro_negation$, $ rule_ex_intro_rdfs5 rule_ex_intro_rdfs5$, $ rule_ex_intro_rdfs7 rule_ex_intro_negation$, and $ρ rule_ex_intro_rdfs7 ρ$ for all $ρ∈ $ (due to the all-variable triple ?x ?p ?y in rule_ex_intro_rdfs7). $ $ is not fully stratified, e.g., due to $ rule_ex_intro_negation rule_ex_intro_rdfs7 rule_ex_intro_student rule_ex_intro_negation$. $ $ is not chain stratified either. For clarity, we substitute constants from the image of $ω$ directly. To construct a chain for $ rule_ex_intro_negation rule_ex_intro_rdfs7 rule_ex_intro_student$, consider instances $ rule_ex_intro_negation = rule_ex_intro_negation$, $ rule_ex_intro_rdfs7= rule_ex_intro_rdfs7[ ?p/:examiner,?q/:participant,?x/?c,?y/?p]$, and $ rule_ex_intro_student = rule_ex_intro_student$. Then $ rule_ex_intro_negation$ is a length-1 chain, and $ rule_ex_intro_negation rule_ex_intro_rdfs7$ is a chain since $ rule_ex_intro_negation rule_ex_intro_rdfs7$, with chain rule $ _ rule_ex_intro_negation, rule_ex_intro_rdfs7$: nthreelisting ?c :teacher ?p . :examiner rdfs:subPropertyOf :participant . ?c :examiner ?p | rule_ex_intro_chain_rule| => ?c :participant ?p. nthreelisting We have $ _ rule_ex_intro_negation, rule_ex_intro_rdfs7 rule_ex_intro_student$, so $ rule_ex_intro_negation rule_ex_intro_rdfs7 rule_ex_intro_student$ is a chain, hence $ rule_ex_intro_negation rule_ex_intro_student$. Similarly, $ _ rule_ex_intro_negation, rule_ex_intro_rdfs7, rule_ex_intro_student rule_ex_intro_negation$, so we have a cycle $ rule_ex_intro_negation rule_ex_intro_negation$, and $ $ is not chain stratified. , the extended $ =\ rule_ex_intro_student, …, rule_constraint_teacher_type\$ is chain stratified under constraints, where $ = \ rule_ex_intro_negation\$. The $ $-paths from $ rule_ex_intro_negation$ to $ rule_ex_intro_student$ that do not revisit $ rule_ex_intro_negation$ or pass through $ rule_ex_intro_student$ can be described by a regular expression $ rule_ex_intro_negation ( rule_ex_intro_rdfs7 rule_ex_intro_rdfs5 ) rule_ex_intro_rdfs7 rule_ex_intro_student$, and each such path corresponds to one or more chains. Similarly, $ rule_ex_intro_negation( rule_ex_intro_rdfs7 rule_ex_intro_rdfs5 ) rule_ex_intro_rdfs7$, for $ rule_ex_intro_negation$ to $ rule_ex_intro_rdfs7$. All chains from $ rule_ex_intro_negation$ to $ rule_ex_intro_student$ violate constraints $ rule_constraint_teacher_participant$ or $ rule_constraint_teacher_spo$, and the chains from $ rule_ex_intro_negation$ to $ rule_ex_intro_rdfs7$ that negatively rely on $ rule_ex_intro_negation$ violate constraint $ rule_constraint_teacher_type$. The above chain $ rule_ex_intro_negation rule_ex_intro_rdfs7 rule_ex_intro_student$ will be discarded due to $ rule_constraint_teacher_participant$. Since rdfs:subPropertyOf is transitive by $ rule_ex_intro_rdfs5$, longer chains of the form $ rule_ex_intro_negation rule_ex_intro_rdfs7^+ rule_ex_intro_student$ entail the same constraint-violating fact. Any alternative chain from $ rule_ex_intro_negation[ ?p/rdf:type]$ to $ rule_ex_intro_student$ via $ rule_ex_intro_rdfs7[ ?q/rdfs:subPropertyOf]$, entails ?c rdfs:subPropertyOf rdf:type. Then any triple ?x ?c :Student entails ?x rdf:type :Student, which could create a negative feedback cycle for $ rule_ex_intro_negation$. Such chains are discarded due to $ rule_constraint_teacher_spo$. Similarly, any chain starting like $ rule_ex_intro_negation rule_ex_intro_rdfs7^+ rule_ex_intro_rdfs5 …$ violates $ rule_constraint_teacher_spo$. All surviving chains of the form $ rule_ex_intro_negation rule_ex_intro_rdfs7 rule_ex_intro_rdfs7[ ?q/rdf:type]$, whose chain rules negatively rely on $ rule_ex_intro_negation$, are eliminated by $ rule_constraint_teacher_type$. The remaining chains (all of the form $ rule_ex_intro_negation rule_ex_intro_rdfs7^+$) are unproblematic. chains is still crucial here. For a “full stratification under constraints” (following MKH13:reliances), we would need to prevent $ rule_ex_intro_negation rule_ex_intro_rdfs7$ with a stronger constraint such as :examiner rdfs:subPropertyOf ?q => false, which would forbid useful triples, e.g., :examiner rdfs:subPropertyOf :teacher. example Null awareness When building chain rules as in eq:chain-rule (or eq:chain-rule-dlclosure under constraint closure), the information which variables are existential is lost for all but the last instance. To prohibit them from unifying with constants, we can restrict a fixed arbitrary injection $ $ to $ ( _k-1)$ and apply it to the chain rule. The latter may thus contain nulls, which can eliminate some irrelevant reliances. Negation awareness Keeping negations of the atoms $ _i∈ [k] ( _i)$ in the chain rule’s body sharpens the analysis further. They may prevent some outgoing reliances of the chain rule. However, this needs to be reflected in $ (c)$, tracking the subset of these atoms that only use frontier variables. This is clearly bounded. It suffices, as only such atoms may unify with facts of the representative databases examined for reliance checks between the chain rule and other rules. Implementation \& Evaluation sec:impl implement null- and negation-aware chain stratification under $ $-closure in a Rust library Source code (ca. 13k LoC) available in the supplementary material statement. and a PoC tool using it, which accepts Nemo Ivliev+:Nemo2024 and VLog UJK:VLog2016 syntax, as well as (a subset of) N3 syntax (via a Python transpiler). our method is designed to address known problematic cases that arise in RDF rules, there are no representative RDF-based rulesets that could be used to evaluate its effectiveness. However, we can investigate the feasibility of our analysis in terms of performance. To this end, we use our tool to check chain stratification on a benchmark that was also used by González~et al. GIKM2022 in their analysis of core stratification, which consists of 201 piece-decomposed, negation-free rulesets with predicate symbols (not just triple). They correspond to a subset of the https://w.cs.ox.ac.uk/isg/ontologies/Oxford Ontology Repository, accessed 2025-12-01. Without negation, core and full chain stratification coincide, but the effort of computing chains is still realistic. We ran our experiments on a Linux server (2$×$QuadCore Intel Xeon 3.5GHz, 768GiB RAM), with a 15min timeout per analysis. Each run is repeated thrice and the median time values are reported in our supplementary material. , $80$ rulesets were classified in less than 0.1sec, $115$ in less than 1sec, $160$ in under 1 min, and $187$ within the total timeout. The remaining $14$ rulesets that did not finish in that time each contained over 60,000 rules. $128$ cases were not core-stratified (the previous best condition for negation-free rules), and required the analysis of chains. These cases on average required an additional $12.51\%$ of analysis time in comparison to the check for core stratification. Considering the relative complexity of our definitions, we consider this to be a very acceptable overhead that appears to be feasible in practice, especially since many sets of RDF rules are not covered by any other conditions. Conclusion sec:conclude established chain stratification to improve beyond prior notions. Augmented by constraints, our approach enables the use of N3 rules like rdfs7 in combination with blank nodes and negation. We designed a refined criterion based on the transitive closure of positive reliances, contributed interesting theoretical results on their decidability, and provided a prototypical implementation in Rust. Promising directions of future work may include (1) integration with RDF rule engines, (2) repair of non-chain-stratified rulesets by mining constraints from counter examples generated by reliance computations, (3) transfer of our finding to the handling of aggregates, and (4) analysis of the utility of $ $ to establish new termination criteria. Finally, we hope that our insights can also contribute to ongoing standardisation activities of RDF rules. credits This work is supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in project number 389792660 (TRR 248, https://w.perspicuous-computing.science/Center for Perspicuous Systems) and 390696704 (CeTI Cluster of Excellence), by the Bundesministerium für Forschung, Technologie und Raumfahrt (BMFTR, Federal Ministry of Research, Technology and Space) in the https://w.scads.de/Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), and in DAAD project 57616814 ( https://secai.org/SECAI, School of Embedded Composite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence. Supplemental Material Statement. separate annex with full proofs of Lemmata and Theorems is published in an extended version of the paper at . source code of our Rust implementation is published at . to README.md to reproduce the results. Declaration of use of Generative AI. During the preparation of this work the authors used ChatGPT to ask for Rust programming tips. Opus 4.6 was used for proofreading. The text in this paper as well as the source code is fully handwritten. credits splncs04 thebibliography10 [1] #1 URL [1]https://doi.org/#1 existentialN3 Arndt, D., Mennicke, S.: Existential Notation3 Logic. Theory Pract. Log. Program. 25(3), 304–339 (2025). 10.1017/S1471068425000055, https://doi.org/10.1017/s1471068425000055 BLMS11:decline Baget, J.F., Lecl\‘ere, M., Mugnier, M.L., Salvat, E.: On rules with existential variables: Walking the decidability line. Artificial Intelligence 175(9–10), 1620–1654 (2011) BSG:Vadalog18 Bellomarini, L., Sallinger, E., Gottlob, G.: The Vadalog system: Datalog-based reasoning for knowledge graphs. Proc.\ VLDB Endowment 11(9), 975–987 (2018). 10.14778/3213880.3213888 CG+13:acyclicity Cuenca Grau, B., Horrocks, I., Kr\"otzsch, M., Kupke, C., Magka, D., Motik, B., Wang, Z.: Acyclicity notions for existential rules and their application to query answering in ontologies. J.\ of Artificial Intelligence Research 47, 741–808 (2013) rdf11-concepts Cyganiak, R., Wood, D., Lanthaler, M. (eds.): RDF 1.1 Concepts and Abstract Syntax. W3C Recommendation (25 February 2014), available at http://w.w3.org/TR/rdf11-concepts/ shacl12-rules David, R., Habgood, D., Seaborne, A., Steyskal, S. (eds.): SHACL 1.2 Rules. W3C Working Draft (02 April 2026), available at https://w.w3.org/TR/2026/WD-shacl12-rules-20260402/ DNR08:corechase Deutsch, A., Nash, A., Remmel, J.B.: The chase revisited. In: Lenzerini, M., Lembo, D. (eds.) Proc.\ 27th Symp. on Principles of Database Systems (PODS’08). p. 149–158. ACM (2008) EKM:ExNeg2022 Ellmauthaler, S., Kr\"otzsch, M., Mennicke, S.: Answering queries with negation over existential rules. In: Proc.\ 36th AAAI Conf.\ on Artificial Intelligence (AAAI’22). p. 5626–5633 (2022). 10.1609/aaai.v36i5.20503 GIKM2022 Gonz\’alez, L., Ivliev, A., Kr\"otzsch, M., Mennicke, S.: Efficient dependency analysis for rule-based ontologies. In: Sattler, U., Hogan, A., Keet, M., Presutti, V., Almeida, J.P.A., Takeda, H., Monnin, P., Pirr\‘o, G., d’Amato, C. (eds.) Proc. 21st International Semantic Web Conference (ISWC 2022). LNCS, vol. 13489, p. 267–283. Springer (2022). 10.1007/978-3-031-19433-7_16 rdf11-semantics Hayes, P., Patel-Schneider, P.F. (eds.): RDF 1.1 Semantics. W3C Recommendation (25 February 2014), available at http://w.w3.org/TR/rdf11-mt/ Hogan:LeanRDF:Tweb17 Hogan, A.: Canonical forms for isomorphic and equivalent RDF graphs: Algorithms for leaning and labelling blank nodes. ACM Trans. Web 11(4), 22:1–22:62 (2017). 10.1145/3068333 SWRL Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B.N., Dean, M.: SWRL: A Semantic Web Rule Language. W3C Member Submission (21 May 2004), available at http://w.w3.org/Submission/SWRL/ Ivliev+:Nemo2024 Ivliev, A., Gerlach, L., Meusel, S., Steinberg, J., Kr\"otzsch, M.: Nemo: Your friendly and versatile rule reasoning toolkit. In: Marquis, P., Ortiz, M., Pagnucco, M. (eds.) Proc.\ 21st Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning (KR’24). p. 743–754. IJCAI Organization (2024). 10.24963/kr.2024/70 RIF-overview Kifer, M., Boley, H. (eds.): RIF Overview. W3C Working Group Note (22 June 2010), available at http://w.w3.org/TR/rif-overview/ KLS6:coloring-asp Konczak, K., Linke, T., Schaub, T.: Graphs and colorings for answer set programming. Theory Pract. Log. Program. 6(1-2), 61–106 (2006) KR20:cores Kr\"otzsch, M.: Computing cores for existential rules with the standard chase and ASP. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proc.\ 17th Int.\ Conf.\ on Principles of Knowledge Representation and Reasoning (KR’20). p. 603–613. IJCAI (2020). 10.24963/kr.2020/60 Kroetzsch2025:Datalog Kr\"otzsch, M.: Modern Datalog: Concepts, methods, applications. In: Artale, A., Bienvenu, M., Garc\’ia, Y.I., Murlak, F. (eds.) Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025). OASIcs, vol.~138. Dagstuhl Publishing (2025). 10.4230/OASIcs.RW.2024/2025.7 KIAK:chains K\"uchenmeister, N., Ivliev, A., Arndt, D., Kr\"otzsch, M.: Stratified negation in RDF rules: A correct approach. In: Koubarakis, M., Vidal, M.E., Polleres, A., van Erp, M., Ruiz, E.J., Seneviratne, O., Aroyo, L., Demartini, G., Alharbi, R., Barile, R., d’Amato, C., Tamma, V. (eds.) Proc. 25th International Semantic Web Conference (ISWC 2026). LNCS, vol.~tbd, p.~tbd. Springer (2026). tbd MKH13:reliances Magka, D., Kr\"otzsch, M., Horrocks, I.: Computing stable models for nonmonotonic existential rules. In: Rossi, F. (ed.) Proc.\ 23rd Int.\ Joint Conf.\ on Artificial Intelligence (IJCAI’13). p. 1031–1038. AAAI Press/IJCAI (2013) N+15:RDFoxToolPaper Nenov, Y., Piro, R., Motik, B., Horrocks, I., Wu, Z., Banerjee, J.: RDFox: A highly-scalable RDF store. In: et~al., M.A. (ed.) Proc.\ 14th Int.\ Semantic Web Conf.\ (ISWC’15), Part I. LNCS, vol.~9367, p. 3–20. Springer (2015). 10.1007/978-3-319-25010-6_1 UJK:VLog2016 Urbani, J., Jacobs, C., Kr\"otzsch, M.: Column-oriented Datalog materialization for large knowledge graphs. In: Schuurmans, D., Wellman, M.P. (eds.) Proc.\ 30th AAAI Conf.\ on Artificial Intelligence (AAAI’16). p. 258–264. AAAI Press (2016). 10.1609/aaai.v30i1.9993 n3-community-draft Van Woensel, W., Arndt, D., Champin, P.A., Tomaszuk, D., Kellogg, G. (eds.): Notation3 Language. W3C Draft Community Group Report (15 May 2024), available at https://w3c.github.io/N3/spec/ thebibliography Proofs for Section~ sec:trails the ensuing proofs, we will use the following additional notation: itemize $ ( )$ for the set of all matches of rules from $ $ over database $ $. $ ( ) ( )$ to collect all the unsatisfied matches over $ $. $ (C,k)$ for $ _∀ _∃$ in the extended match $ (C,k)= (C,k), _∀ _∃ $ applied in step $k$ of chase $C$. itemize * will show a slightly stronger version of the theorem for $ $, assuming only that $ $. (The specifics of $ $ are irrelevant for the proof.) proof[of contrapositive of Theorem~ thm:posrT-prec-no-violate] Let $C$ be a chase sequence that violates $ $. Then there must be chase steps $i $ with $ (C,k) (C,i)$. In fact, $i<k$ as there would otherwise be a self-loop in $ $. Select such $ ,k $ (lexicographic) minimally. the following sequence of indices: align a_1 & \\ a_x+1 & \ j (C,a_x) ∈ ( (C,j)) \ i < a_x align This sequence is clearly strictly decreasing (and finite). Also, it has length $|a| > 1$. For all $x<|a|$, we have $i < a_x$. Only $a_|a|$ may be smaller or equal to $i$. to the minimality of $ ,k $, and because of $ $, no negative reliance can be violated in $C$ up to step $k$. Therefore, $C$ is generating up to $k$. Hence, we know that a match selected in step $a_x$ that was already available in step $j<a_x$ must also be available in all intermediate steps. second-to-last match $ (C,a_|a|-1)$ was already applicable in step $a_|a| $. We therefore clearly have $ (C,a_|a|-1) ∈ ( (C,i))$. center tikzpicture[>=stealth] [->] (-1.3,0) – (5,0); [below] at (-0.5,0) chase seq.; (1,-0.1) – (1,0.1); (4,-0.1) – (4,0.1); [below] at (1,0) $i$; [below] at (4,0) $k$; [->, bend right=40] (4,0.2) to node[above,align=center] violates\\$ (C,k) (C,i)$ (1,0.2); [below] at (4,-0.6) $a_1$; [below] at (3.2,-0.6) $a_2$; [->, bend left=20] (4,-0.5) to (3.2,-0.5); [below] at (2.5,-0.6) $a_3$; [->, bend left=20] (3.2,-0.5) to (2.5,-0.5); [below] at (1.9,-0.4) $…$; [below] at (0.6,-0.6) $a_|a|$; [->, bend left=25] (1.3,-0.5) to (0.6,-0.5); tikzpicture center The sequence of rule instances $t= _1,…, _|a|$ with equation _x = (C,a_|a|+1-x) (C,a_|a|+1-x)ω^-1 x∈ [|a|] equation is a trail, because the chase $C$ with step mapping $f: [|a|] (C)$, $x f a_|a|+1-x$ fulfils the two conditions from Definition~ def:trail. Match correspondence follows from the definition of $ _x$ based on the matches applied in step $f(x)$ of $C$. Causal connection is a consequence of the subsequent sequence item $a_x+1$ being the minimal chase step where the match used at $a_x$ was available. This means that $ (C,a_x)$ must map a body atom of $ (C,a_x)$ onto a fact added by applying $ (C,a_x+1)$, i.e. $ ( _x)∩ ( _x+1)≠ $. thus have $ (C,a_|a|) (C,a_1)$. we set $a_1=k$, we have $ (C,a_1)= (C,k)$ and we hence $ (C,a_1) (C,i)$. This gives $ (C,a_|a|) (C,i)$ and both rules were selectable in chase step $i$. We also know that $ (C,a_|a|) ≠ (C,i)$, because $ $ would otherwise have a self-loop. Hence, $C$ disrespects $ $, as $ (C,a_|a|)$ should have been preferred over $ (C,i)$ in chase step $i$. proof * proof[of contrapositive of Theorem~ thm:posrT-prec-unique-chase-result] Let $C_1$ and $C_2$ be two generating chases of (the same) $ $ with non-isomorphic results. This can only be the case if there is (w.l.o.g) a match that is applied in $C_1$ but never applied in $C_2$. Further, there must be such a match, whose application in $C_1$ has added facts which are not present in $C_2$ ($ $). Select a minimal $i∈ (C_1)$, such that $ (C_1,i)$ is such a match. All matches applied before $i$ in $C_1$ must therefore be applied at some point in $C_2$. Let $i_2∈ (C_2)$ be the chase step at which the last of them was applied. The database $ (C_1,i-1) = _0 ∪ _k<i ( (C_1,k)) (C_1,k)$ must homomorphically map into $ (C_2,i_2)$ ($ $). Thus, any unsatisfied match over $ (C_2,i_2)$ must either (1) also be unsatisfied over $ (C_1,i-1)$ or (2) not be a match there (because the necessary facts were not derived yet). In case (2), it must be derivable by a sequence of applications starting with an unsatisfied match over $ (C_1,i-1)$. The $ (C_1,i)$ may either be (a) unsatisfied, (b) satisfied, or (c) invalidated by deriving a fact from $ ( (C_1,i)) (C_1,i)$ over $ (C_2,i_2)$. If (a), then, there must be a $k _2$, such that $ (C_1,i)$ is no unsatisfied match over $ (C_2,k)$ (due to fairness). Applying $ (C_2,k)$ has either (b) satisfied $ (C_1,i)$, or (c) invalidated it. In case (b), $ (C_1,i)$ cannot be Datalog, as satisfying it would otherwise not have added facts in $C_1$ which $C_2$ lacks (as is required by $ $). Either $ (C_1,i)$ has both Datalog and existential pieces, which makes it self-restraining. This would mean that $C_1$ does not respect the precedence $ ( ∪ )$. Or $ (C_1,i)$ has only existential pieces, which means that there is an alternative match for $ (C_1,i)$ over $ (C_2,k)$, i.e. $ (C_2,k) (C_1,i)$ by Definition~ def:restr. In case (c), $ (C_2,k) (C_1,i)$ by Definition~ def:negr. Similar to the proof of Theorem~ thm:posrT-prec-no-violate above, we construct a sequence of chase steps from $C_2$ like align a_1 & \\ a_x+1 & \ j (C_2,a_x) ∈ ( (C_2,j)) \ align It is finite, as it is clearly strictly decreasing and all sequence items are non-negative. In fact, it ends with $a_|a| = 0$. By ($ $) and because $C_2$ is generating, we must be able to find an $x$, such that either (1) $ (C_2,a_x) ∈ ( (C_1,i-1))$, or (2) there exists a $ ρ,μ ∈ ( (C_1,i-1))$ with appropriate step mapping for $C_2$ witnessing that $t_ = ρμω^-1… (C_2,a_x) (C_2,a_x)ω^-1$ is a trail. We then use $a_x …a_1$ to define a sequence of rule instances $t$ and step mapping $f$. By Definition~ def:trail, $C_2$ and $f$ witness that $t$ is a trail. So we now have that $ (C_2,a_x) (C_2,k) ( ∪ ) (C_1,i)$. If (1), there is an unsatisfied match over $ (C_1,i-1)$ for $ (C_2,a_x)$ (and clearly also for $ (C,i)$). As $ ( ∪ )$ is acyclic by assumption, $ (C,i) ≠ (C_2,a_x)$. So $C_1$ does not respect $ ( ∪ )$, as $ (C_2,a_x)$ should have been preferred over $ (C_1,i)$. If (2), $ρ (C_2,a_x) (C_2,k) ( ∪ ) (C_1,i)$. The sequence $t_ $ is also a trail, i.e. $ρ (C_2,k) ( ∪ ) (C_1,i)$ and $ ρ,μ $ should have been preferred over $ (C_1,i)$. Again, $C_1$ disrespects $ ( ∪ )$. proof * proof Let $< ⊂ $ be a smaller relation. Then there must be some $ _1 _2$ with $ _1 < _2$. Consider a relation $ $, such that there is some $ _3$, such that $ _2 _3$ and $< $ is acyclic. Suppose towards contradiction that any chase respecting $< $ has no $ $ violations. Consider a chase sequence $C$ that violates $ _2 _3$, but no other $ $-edges. Analogous to the proof of Theorem~ thm:posrT-prec-no-violate, select $i<k$ minimally, such that $ (C,k) (C,i)$ (in fact, $ (C,k) = _2$ and $ (C,i) = _3$), then construct the sequence $(a_x)_x=1,…|a|$, and the trail $t= _1,…, _|a|$. In chase step $i$, both $ (C,i)$ and $ (C,a_|a|)$ are selectable, but not $ (C,k)$. As $ _1 < _2$, we do not have $ (C,a_|a|) = _1 < _3 = (C,i)$, so $C$ respects $< $. proof * proof[by reduction from the halting problem] Let $M$ be a Turing machine with initial state $q_0$ and single “accept” state $q_f$ and let $w$ be a word. It is undecidable whether $M$ has a finite run on $w$ that reaches the “accept” state. itemize machine $M= , , , δ, q_0, q_f $ with set of states $Q$, input alphabet $ $, tape alphabet $ $, (partial) transition function $δ: Q× × ×\L,R\$, initial state $q_0$ and final state $q_f$. of $ ^*×Q× ^*$ are configurations of $M$. For $δ(q,a)= ’,a’,d $, write $ ,q,by ’b,q’,y $ iff $d=R$ and $ ,q,by ,q’,a’by $ iff $d=L$. word $w∈ ^*$, a run of $M$ is $ ,q_0,ε …$. If this run is finite and ends with $q_f$, then $M$ accepts $w$. itemize Encode $M$ and $w$ into a ruleset $ (M,w)$ with two designated rules $ _1, _2 ∈ (M,w)$, such that $ _1 _2$ if and only if $M$ holds and accepts $w$. In detail:\\ . : $ , w $ for word $w∈ ^*$\\ Output: $ (M,w)$ (constants in bold) align* _1 : & _0,x_1,…,x_|w| .\, state(t_0, q_0), pos(t_0,x_1), tape(t_0,x_1, w_1), next(x_1,x_2), \\ & …, tape(t_0,x_|w|-1, w_|w|-1), next(x_|w|-1,x_|w|), tape(t_0,x_|w|, w_|w|)\\ & state(t,s) ’.\, step(t,t’)\\ & tape(t,x,c) ’.\, next(x,x’)\\ & tape(t,x,c), pos(t,x’), x ’, step(t,t’) tape(t’,x,c)\\ & state(t, s), pos(t,x), tape(t,x, c), next(x’,x), step(t,t’) \\ & state(t’, s’), tape(t’,x, c’), pos(t’,x’) δ( s, c)= s’, c’,L \\ & state(t, s), pos(t,x), tape(t,x, c), next(x,x’), step(t,t’) \\ & state(t’, s’), tape(t’,x, c’), pos(t’,x’) δ( s, c)= s’, c’,R \\ _2 : & state(t_0, q_0), state(t, q_f) accept() align* restricted chase $C$ of the $ $ and $ (M,w)$ is a faithful simulation, irrespective of $ $. (Even if $ ≠ $ and for instance contains a cyclic $ tape$ or $ step$ predicate, this is no problem, as the initialization rule invents fresh nulls without connection to atoms in $ $.) In case $M$ holds and accepts $w$, the sequence $t= _1 _2$ is a trail, witnessed by some such chase (representing the finite accepting run) and a corresponding step mapping. (The causal connection property is always met due to the $ state(t_0, q_0)$ atoms occurring both in $ ( _1)$ and $ ( _2)$.) Otherwise, no chase with appropriate step mapping exists and $t$ cannot be a trail. proof Proof for Section~ sec:chains * proof Let $t= _1… _n$ be a trail. By Definition~ def:trail, $t$ is $∃$-disjoint and there must be a witnessing chase $C$ with step mapping $f: [n] (C)$, such that $ (C,f(x)) = _x,ω $ and $ ( _x)∩ ( _x+1)≠ $. each $i∈ [n]$, consider an injective replacement $ _1= $ and for $i>1$ $ _i: ( _i) ( ( _i-1)) ( _j∈ [i] ( _j))$ of stale variables with fresh ones (as in Example~ ex:generalised). The sequence $ (t)= _1 _1,…, _n _n$ is clearly decoupled (and remains $∃$-disjoint). It generalises $t$ with $σ= _1^-1 … _n^-1$. (The individual replacements are invertible because they are injective. This function composition assumes that the domains of $ _i^-1$ are extended to $ $ by identity in the usual way.) show that $ (t)$ is a chain, by Definition~ def:chain, we have to show for each $k∈ [n-1]$ that $ _ _1 _1… _k _k _k+1 _k+1$. We have $ _i _iσ= _i$ for all $i∈ [n]$, and hence also $ _ _1 _1… _i _iσ= _ _1… _n$ for the corresponding chain rules (see Equation~ eq:chain-rule). So $ _i _i, ω ∈ ( ω^-1 _iω)$ iff $ _i, ω ∈ ( )$ and $ _ _1 _1… _i _i, ω ∈ ( _j∈ [i] ω^-1 _jω)$ iff $ _ _1… _n, ω ∈ ( )$. Since $ ω^-1 _iω _j∈ [i] ω^-1 _iω$ and none of the negative body atoms of the matching rules can match in any of the copies, we further have that $ ( ω^-1 _iω) ( _j∈ [i] ω^-1 _jω)$. $k∈ [n-1]$ and define align* _δ& ( ( _ _1 _1… _k _k) ( _ _1 _1… _k _k) )ω,\\ _b & _j∈ [k] (C,f(k))ω^-1 _jω, and\\ _a & _b _δ. align* Now consider the matches $ _1 _ _1 _1… _k _k, ω $ and $ _2 _k+1 _k+1,ω $. We have $ _1 ∈ ( _j∈ [k] (C,f(k))ω^-1 _jω) = ( _b)$ (see above). Removal of $ _δ$ cannot have removed the match, so $ _1∈ ( _b _δ)= ( _a)$. The match $ _1$ is unsatisfied over $ _a$, as $ _δ$ is not contained in $ _a$. Thus, $ _1 ∈ ( _a)$ and the database $ _b$ was obtained by applying $ _1$ to $ _a$. , we have $ _2 ∈ ( (C,f(k))ω^-1 _kω)$, i.e. $ _2 ∈ ( _b)$. Also, $ _2 ∈ ( _a)$, as it requires facts from $ _δ$ that are only present in $ _b$. Hence, $ _2 ∈ ( _b) ( _a)$. proof Proofs for Section~ sec:chain-strat * proof To show $ _1 (C,i)$, by Definition~ def:restrC we need to give a decoupled chain $c$ that starts with $ _1$, such that $ _c (C,i)$. Obtain $c∈ ( )$ generalising $t$ with $σ$, by injectively renaming stale variables as in Lemma~ lem:trail-gen-dec-chain. By Definition~ def:restr, we thus need to give databases $ _a _b$ and mappings $ _1, _2$, with $ (C,i), _2 ∈ ( ’_a)$ and $ _a = ’_a ∪ ( (C,i)) _2$ and $ _c, _1 ∈ ( _a)$ and $ _b = ’_b ∪ ( _c) _1$, such that there is alternative match for $ (C,i), _2 $ over $ _b$ but not over $ ’_b$. Take $ ’_a = (C,i-1)$ and $ _a = (C,i)$ with $ _2 = (C,i)$. We clearly have $ (C,i), _2 ∈ ( ’_a)$ and $ _a = ’_a ∪ ( (C,i)) _2$ by Definition~ def:chase. Take $ ’_b = (C,f(n)-1)$ and $ _b = (C,f(n))$. It is clear that $ _a _b$, since $i (n)-1$. Recall that by Equation~ eq:chain-rule, $ ( _c) = ( _i∈ [n] ( _i) )∪ ( _i∈ [n-1] ( _i) )$ and $ ( _c) = ( _n)$. We now have: itemize $ ( _c)σω ’_b$ and $ ’_b ( _c) σ _∀$, i.e. $ _c, σω ∈ ( ’_b)$, and $ _b = (C,f(n)+1) = (C,f(n)) ∪ ( (C,f(n))) (C,f(n))$\\ $ _b = (C,f(n)+1)$ $= ’_b ∪ ( _n)ω= ’_b ∪ ( _c)ω$. itemize By assumption, we have an alternative match for $ (C,i)$ over $ _b$ but not $ ’_b$. proof * proof Analogous to the above proof of Lemma~ lem:trail-restrC, we show by Definition~ def:negrC $ _1 (C,i)$ via chain $c$ generalising $t$ with $σ$ as in Lemma~ lem:trail-gen-dec-chain. By Definition~ def:negr we need to give database $ _a$ and mappings $ _1, _2$ with $ _c, _1 ∈ ( _a)$ and $ _b = _a ∪ ( _c) _1$, such that $ (C,i), _2 ∈ ( _a) ( _b)$. This is the case for $ _a = (C,f(n)-1)$, $ _1 = σω$ and $ _2= (C,i)$. proof Proofs for Section~ sec:reg-lang * will use some auxiliary notation: itemize we say formula set, we mean a set of formulae of the form $∃ v.ψ$ for conjunction of atoms $ψ$. This is essentially a set of pieces. databases $ _1$ and $ _2$ and formula set $F$, we write $I_1 _F I_2$, if for all formulae $∃ v. ψ $, we have that $ _1 ∃ v. ψ _∀$ iff $ _2 ∃ v. ψ _∀$. database $ $, we write $ ( )$ for the set of constants and nulls occurring in facts of $ $.\\ For formula set $F$, we write $ (F) = _∃ v.ψ (∃ v.ψ)ω$ for the set of constants and nulls injectively assigned to universal variables of $F$ by $ω$. will apply $ (·)$ to formula sets, defined exactly like $ ( )$ (page eq:variants) but using $F$ instead of $ $. itemize proof Let $c_1$ and $c_2$ be two decoupled chains with the same label. Then $ (c_1) = (c_2)$, $ (c_1) = (c_2)$, and $ (c_1) = (c_2)$. Let $ _n$ and $ _m$ be the last rule instances of $c_1$ and $c_2$, respectively. Further, let $ _n$ and $ _m$ be the two (unique) injective mappings, such that $ _n = ( _n) _n$ and $ _m = ( _m) _m$. $ _1 ∈ ( )$, such that $c_1 _1$ is a decoupled chain. By Definition~ def:decoupled, $c_1 _1$ is decoupled if and only if all variables from $ ( _1) ( ( _n))$ are fresh w.r.t. $c_1$. By Definitions~ def:chain, $c_1 _1$ is a chain if and only if $ _c_1 _1$. Since $ _n$ is injective, we can apply its inverse on both sides and get $ _c_1 _n^-1 _1 _n^-1$, which means by Definition~ def:direct-posr that, for the database $ _1 ( ( _c_1) ∪ ( _c_1) ∪ ( _1)) _n^-1ω$, we have enumerate[leftmargin=.9cm,label=(1. *)] it:c1-alpha the intersection between the atom sets $( ( _c_1) ( _c_1)) _n^-1$ and $ ( _1) _n^-1$ is non-empty, and it:c1-beta the database $ _1$ does not satisfy $∃ v .\, ( _1) _n^-1 _∀$, and it:c1-gamma none of the negative body atoms of $ _1 _n^-1$ are in $ _1$. enumerate $ _1$ be the (unique) injective mapping, such that $ _1 = ( _1) _1$. prove lem:equi-label-chains:1, we want to construct an instance $ _2$, such that $c_2 _2$ is a chain, which is the case if and only if $ _c_2 _2$. Let $ _2 _1 _n^-1 _m$ be that instance. Since $ _m$ is injective, we can apply its inverse on both sides and get $ _c_2 _m^-1 _2 _m^-1$. Unfolding $ _2$, the right-hand side becomes $ _2 _m^-1 = _1 _n^-1 _m _m^-1 = _1 _n^-1$. Unpacking Definition~ def:direct-posr for $ _c_2 _m^-1 _1 _n^-1$, we need to show for database $ _2 ( ( _c_2) ∪ ( _c_2) ∪ ( _2)) _m^-1ω$, that enumerate[leftmargin=.9cm,label=(2. *)] it:c2-alpha the intersection between the atom sets $( ( _c_2) ( _c_2)) _m^-1$ and $ ( _1) _n^-1$ is non-empty, and it:c2-beta the database $ _2$ does not satisfy $∃ v .\, ( _1) _n^-1 _∀$, and it:c2-gamma none of the negative body atoms of $ _1 _n^-1$ are in $ _2$. enumerate , we derive it:c2-alpha: Recall that $ (c_1) = (c_2)$ means by Equation~ eq:alpha-label, that the pieces of $ ( _n)$, which are not contained in $ ( _c_1)$ under $ _n$, are exactly the pieces of $ ( _m)$, which are not contained in $ ( _c_2)$ under $ _m$. Also recall that $ ( _c_1) = ( ( _n)) _n$ and $ ( _c_2) = ( ( _m)) _m$. Therefore, $( ( _c_1) ( _c_1)) _n^-1 = ( ( _c_2) ( _c_2)) _m^-1$. With this equality, it:c2-alpha directly follows from it:c1-alpha. , we derive it:c2-beta: Expanding Equation~ eq:beta-label at $ (c_1) = (c_2)$, we get that $( ( _c_1) ∪ ( _c_1)) ω ∃ v .\, ψ ( _n ω)_∀$ if and only if $( ( _c_2) ∪ ( _c_2)) ω ∃ v .\, ψ ( _m ω)_∀$ for all $∃ v .\, ψ ( ( ( )))$. As $ _n$ and $ _m$ are both injective, we can apply their inverses to learn that $ _1 ∃ v .\, ψ _∀$ if and only if $ _2 ∃ v .\, ψ _∀$. Using the forward direction of this equivalence, it:c2-beta follows from it:c1-beta. The defining condition for $ _F$ is exactly this equivalence, so $ _1 _F _2$, which will later be needed to argue for lem:equi-label-chains:2. , we derive it:c2-gamma: By Equation~ eq:gamma-label, $ (c_1) = (c_2)$ says that a variant $ ρ$ has a negative body atom falling into $ _1$ under $ _n$ if and only if it has a negative body atom falling into $ _2$ under $ _m$. By it:c1-gamma, the variant $ ( _1) = _1 _n^-1$ cannot be one of them, so it:c2-gamma follows. it:c2-alpha– it:c2-gamma, we conclude that $c_2 _2$ is a chain. Note that $c_2 _2$ might not be decoupled, if the variables from $ ( _1) ( ( _n))$, which necessarily are fresh w.r.t. $c_1$, are not also fresh w.r.t. $c_2$. If so, just take any injective mapping $θ’ : (c_2 _2) _i∈ [m] ( _i)$, and $c_2 _2θ’$ is clearly decoupled. As $θ’$ acts only on the variables in $ _2$ not shared with the head of $c_2$’s final instance, $ _c_2 _2θ’$ holds iff $ _c_2 _2$ (by an argument similar to the proof of Lemma~ lem:trail-gen-dec-chain), i.e. $c_2 _2θ’$ is a (decoupled) chain. prove lem:equi-label-chains:2, we first establish: claim[$ $] Let $F$ be a formula set, such that $ ( (F)) = F$. Let $ _1$, $ _2$, and $X$ be databases, such that $( ( _1 ∪ _2)) ∩ (X) (F)$. Then $ _1 _F _2$ implies that $ _1 _F _2 $. claim proof Let databases $ _1 _F _2$, and $X$ as well as formula set $F$ be as in the claim. This means that $ _1$ and $ _2$ agree on satisfaction of formulae from $F$ under $ _∀$ and that $X$ uses only fresh symbols, except for $ (F)$. Let $∃ v. ψ$ be any formula from $F$. prove the claim, we need to show that either both $ _1 ∃ v. ψ _∀$ and $ _2 ∃ v. ψ _∀$ or neither $ _1 ∃ v. ψ _∀$ nor $ _2 ∃ v. ψ _∀$. case that $ _1 ∃ v. ψ _∀$, then $ _2$ must also satisfy it because of $ _1 _F _2$. As satisfaction for pieces is monotone, we directly get that $ _1 ∃ v. ψ _∀$ and $ _2 ∃ v. ψ _∀$. the case that $ _1 ∃ v. ψ _∀$. By $ _1 _F _2$, we must also have $ _2 ∃ v. ψ _∀$. Suppose that $ _2 ∃ v. ψ _∀$. So there exists a mapping $ _∃: v → ∪ $ such that $ ψ _∀ _∃ _2 $. It remains to show that $ _1 ∃ v. ψ _∀$. image of $ _∃$ can be separated into three disjoint sets $A = (F)$ and $B = (X) $ and finally $C = ( _2) $. Accordingly, we can split $ v$ into three disjoint sets $ v_A ∪ v_B ∪ v_C$ where $ v_S = \ v∈ v _∃(v) \$ for a set $S$. And finally, we can split $ _∃$ into three separate mappings $ _∃^A : v_A $, $ _∃^B : v_B $, and $ _∃^C: v_C $, such that $ _∃= _∃^A _∃^B _∃^C$. For a function $f: A $, we call $f : A $ with $x (x)$ for $x $ and $x $ for $x $ the identity extension of $f$. Given two functions $f: A_1 $ and $g: A_2 $ where $A_1 _2 = $, we write $f : A_1 ∪ A_2 $ for the composition $f $ of their identify extensions. $ ψ _∀ _∃ _2 $, we can write $ ψ$ as the disjoint union of two sets $ ψ_1$ and $ ψ_2$, such that $ ψ_1 _∀ _∃ _2$ and $ ψ_2 _∀ _∃ $. Clearly, the image of existentials from the first set is $ _∃[ ( ψ_1)] ( _2) = A $ and the image of existentials from the second set is $ _∃[ ( ψ_2)] (X) = A $. So we have $ ψ_1 _∀ _∃^A _∃^C _2$ and $ ψ_2 _∀ _∃^A _∃^B $. $ ρ$ be a variant with $∃ v .\, ψ ∈ ( ρ)$. Applying the variable mapping $( _∃^Aω^-1) : ( ) → ( )$ yields the variant $ ρ ( _∃^A ω^-1)$. The pieces of the formula $∃ v_C .\, ψ_1 ( _∃^Aω^-1)$ are subformulae of $ ρ( _∃^A ω^-1) ∈ (F)$. Since each of them is satisfied by $ _2$ (with $ _∃^C$) they must also be satisfied by $ _1$, i.e. we must be able to find a $ _∃^C’: v_C → ( _1)$, such that $ ψ_1 ( _∃^A ω^-1) _∀ _∃^C’ = ψ_1 _∀ _∃^A _∃^C’ _1$. Thus, $ _1 ∃ v .\, ψ _∀$ with $ _∃^A _∃^B _∃^C’$. proof lem:equi-label-chains:2, we need to show that $ (c_1 _1) = (c_2 _2)$. We will show this for the three components of the label separately. , we have $ (c_1 _1) = (c_2 _2)$, because the final instances $ _1$ and $ _2$ both correspond to the same variant $ ( _1)$. In it:c1-alpha and it:c2-alpha we thus identified the same non-empty intersection between the body of this variant and the heads of the chain rules minus their bodies. noted, $ (c_1) = (c_2)$ gives $ _1 _F _2$. Since $ ( (·))$ is idempotent and the set $F$ used for computing $ $ is $ (H)$ (or with $ $-closure $ (H )$), and $H$ and $B$ are closed under $ (·)$, it fulfils the requirement of the claim $ $. The variables used universally in $F$ are from $ ( )$, i.e. $X$ may share only symbols $ ( )ω$ with the union of $ _1$ and $ _2$. Note that $ ( _1∪ _2) = ( ( _1) ∪ ( _2))$. The set of facts $X = ( ( ( _1)) ∪ ( ( _1))) ω$ meets the conditions for claim $ $, since the instance is decoupled w.r.t. both chains $c_1$ and $c_2$. So we find that $ _1 _F _2 $ by ($ $). This set $X$ is exactly the set of facts that is added to the respective databases for computing $ (c_1)$ and $ (c_2)$. , we clearly have $ (c_1 _1) = (c_2 _2)$, as the fact set $X$ which adds to the databases are again identical. proof * claim[$ $] Let $w_1,w_2∈ ( )$ be two words with the same final letter. For any $v∈ ^*$, $w_1v∈ ( )$ iff $w_2v∈ ( )$. claim proof[by induction on $|v|$] For the induction base, the length of $v$ is zero, i.e. $v = ε$ (the empty word) and $w_2v = w_2$. By assumption $w_2 ∈ ( )$ and so directly $w_2v ∈ ( )$. induction hypothesis (IH) is that for any word $v’∈ ^*$ and symbol $c ∈ $, $w_1v’∈ ( ) _2v’∈ ( )$ implies $w_1v’c∈ ( ) _2v’c∈ ( )$. the induction step, let $v = v’c$ for $v’∈ ^*$ and $c∈ $. If $v’ = ε$, the final letter of $w_1v’$ is the final letter of $w_1$ and the final letter of $w_2v’$ is the final letter of $w_2$, which are the same by assumption. Otherwise, the final letter of both $w_1v’$ and $w_2v’$ is the final letter of $v’$. Therefore, $w_1v’$ and $w_2v’$ have identical final letters in both cases and hence correspond to equi-labelled chains. Applying Lemma~ lem:equi-label-chains finishes the induction. proof itemize sets $S$ and $T$, an equivalence relation $ $ over $S$ distinguishes elements based on a predicate $p: S $, if $x $ iff $p(x) = p(y)$ for all $x,y $. a language $ () ^*$, the extensions of a word $w ∈ ()$ is the set of all $v∈ ^*$ for which $wv ∈ ()$. Myhill-Nerode, a language is regular, if it is possible to give an equivalence relation over its words that has finitely many equivalence classes and distinguishes words based on their extensions. itemize proof[of Theorem~ thm:LR-regular] We define an equivalence relation over words in the language $ ( )$ based on their final letters equation _ ( ) \ (c_1),w(c_2) _1,c_2∈ ( ), (c_1)= (c_2) \. equation Clearly, $ _ ( )$ has at most $| |$-many equivalence classes, which is finitely many as the alphabet is finite. By ($ $), two words from $ ( )$ that share the same label ($ =$ final letter), i.e. are $ _ ( )$-equivalent, have the same extensions. , $ _ ( ) ∪( ^* ( ))^2$ meets the conditions of Myhill-Nerode, which makes $ ( )$ a regular language. proof claim lem:equi-label-chains-restr-negr For $c_1,c_2 ∈ ( )$ with $ (c_1)= (c_2)$, we have $ _c_1 ρ$ iff $ _c_2 ρ$ and $ _c_1 ρ$ iff $ _c_2 ρ$. claim proof To compute $ _c_i ρ$ (see Definition~ def:restr) and $ _c_i ρ$ (see Definition~ def:negr) for $i∈\1,2\$, it suffices to examine unifiable subsets of $ (ρ)$ or $ (ρ)$ with $ ( _c_i)$ (c.f. efficient algorithms of GIKM2022). Remaining checks concern the satisfaction of the heads of the involved rules on representative databases. Let $ _n_i$ be the final instances in $c_i$, with unique $ _n_i$, such that $ _n_i = ( _n_i) _n_i$. Again, we can equivalently test for $ _c_i _n_i^-1 ρ _n_i^-1$ and $ _c_i _n_i^-1 ρ _n_i^-1$ (as $ _n_i$ is revertible and $ _n_i^-1$ is injective). These will involve $( ( _c_i) ∪ ( _c_i)) _n_i^-1ω$, and we stated before that these are $ _F$-equivalent due to $ (c_1)= (c_2)$ (see proof of Lemma~ lem:equi-label-chains~ lem:equi-label-chains:1) and satisfy the same rule heads. proof Details on Introductory Example (#1) (#1) 1em will now revisit the introductory examples (cf. Section~ sec:intro, Problems~1 and 2). Here, we refer to the N3 rule in line $i$ by $ _i$. Figure~ fig:intro_rel-graphs depicts a graphical representation of the reliance relations between these rules. Evidently, this yields an acyclic graph for rule_father– rule_different_fathers on the right, which means that $ _P2 = \ _8, _9, _10, _11 \$ is fully stratified (and thus also chain-stratified). The graph on the left, however, has cycles through negative reliances $ _1 _2$ and $ _4 _2$, i.e. $ _P1 = \ _1, _2, _3, _4 \$ and $ ’_P1 = _P1 ∪\ _5, _6, _7 \$ are not fully stratified. Below, we will examine $ _P1$ and $ ’_P1$ in detail, to see that — while neither is chain-stratified either (see Example~ ex_problem1_solved) — $ ’_P1$ is chain-stratified under constraints (as defined in Section~ sec_refinements). figure tikzpicture[>=Latex[length=2m,width=1.5m], baseline=(current bounding box.north)] [draw,circle] (1) at (0,0) $ _1$; [draw,circle] (2) at (0,-2) $ _2$; [draw,circle] (3) at (2,0) $ _3$; [draw,circle] (4) at (2,-2) $ _4$; [draw,circle] (5) at (4,0) $ _5$; [draw,circle] (6) at (4,-1) $ _6$; [draw,circle] (7) at (4,-2) $ _7$; [->] (1)–node[left]$ $(2); [->] (4)edge[bend left]node[below]$ $(2); [dashed,->] (3)edge[loop left](3); [dashed,<->] (3)–(4); [dashed,->] (3)–(5); [dashed,->] (3)–(6); [dashed,->] (3)–(7); [dashed,<->] (4)–(1); [dashed,<->] (4)–(2); [dashed,<->] (4)edge[loop below](4); [dashed,->] (4)–(5); [dashed,->] (4)–(6); [dashed,->] (4)–(7); tikzpicture 5em tikzpicture[>=Latex[length=2m,width=1.5m], baseline=(current bounding box.north)] [draw,circle] (8) at (0,0) $ _8$; [draw,circle] (9) at (0,-2) $ _9$; [draw,circle] (10) at (2,0) $ _10$; [draw,circle] (11) at (2,-2) $ _11$; [->] (10)–node[right]$ $(11); [->] (9)–node[left]$ $(8); [dashed,->] (8)–(10); [dashed,->] (8)–(11); tikzpicture Reliance graph of rule_ex_intro_student– rule_constraint_teacher_type (left) and rule_father– rule_different_fathers (right); dashed lines are $ $ fig:intro_rel-graphs figure us first rewrite L1–L7 in more compact syntax and using fewer variables. equation* arrayc aligned _1&: (?x,pa,?y) (?y,ty,St) \\ _2&: (?x,te,?y), (?y,ty,St) (?x,ex,?y) \\ _3&: (?p,spo,?y), (?y,spo,?q) (?p,spo,?q) \\ _4&: (?p,spo,?q), (?x,?p,?y) (?x,?q,?y) aligned & aligned _5&: (ex,spo,pa) \\ _6&: (ex,spo,spo) \\ _7&: (ex,spo,ty) aligned array equation* are cycles through negative reliances, e.g. $ _2 _4 _1 _2$ or just $ _2 _4 _2$. All $ $-edges end in $ _2$, so we only need to examine chains starting with instances of $ _2$. As explained earlier, the ruleset is indeed not chain stratified, but it is chain stratified under constraints due to the constraints $ _5$, $ _6$ and $ _7$. Algorithm~ alg:chains will consider the following chains in the given order: 1em 8pt10pt description [$ _2, _4\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1) (?x,?q_1,?y)$ itemize [$ $] chain accepted [$ $] $ _2$ rejected because it would require $?q_1 $, $?y $, violating constraint $ _7$ itemize [$ _2, _4, _1\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,pa), (?x,pa,?y) (?y,ty,St)$ itemize [$ $] chain rejected because of constraint $ _5$ itemize [$ _2, _4, _2\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,te), (?x,te,?y) (?x,ex,?y)$ itemize [$ $] chain rejected because the head is already entailed itemize [$ _2, _4, _3\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,spo), (?x,spo,?y), (?y,spo,?z) (?x,spo,?z)$ itemize [$ $] chain rejected because of constraint $ _6$ itemize [$ _2, _4, _4\>:\>$] . description [$ [?p/?q_1,?q/?q_2 ]\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,?q_2) (?x,?q_2,?y)$ itemize [$ $] chain accepted [$ $] $ _2$ rejected because it would require $?q_2 $, $?y $, such that $ _3$ derives $ (ex,spo,ty)$, violating constraint $ _7$ itemize [$ [?q_1/spo,?p/?x,?q/?y ]\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,spo), (?x,spo,?y), (?x_1,?x,?y_1) (?x_1,?y,?y_1)$ itemize [$ $] chain rejected because of constraint $ _6$ itemize description [$ _2, _4, _4, _1\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,pa), (?x,pa,?y) (?y,ty,St)$ itemize [$ $] chain rejected because $ _3$ derives $ (ex,spo,pa)$, violating constraint $ _5$ itemize [$ _2, _4, _4, _2\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,te), (?x,te,?y) (?x,ex,?y)$ itemize [$ $] chain rejected because the head is already entailed itemize [$ _2, _4, _4, _3\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,spo), (?x,spo,?y), (?y,spo,?z) (?x,spo,?z)$ itemize [$ $] chain rejected because $ _3$ derives $ (ex,spo,spo)$, violating constraint $ _6$ itemize [$ _2, _4, _4, _4\>:\>$] . description [$ [?p/?q_2,?q/?q_3 ]\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,?q_2), (?x,?q_2,?y), (?q_2,spo,?q_3) (?x,?q_3,?y)$ itemize [$ $] chain accepted (…but continuing like this will repeat label) [$ $] $ _2$ rejected because it would require $?q_3 $, $?y $, such that two $ _3$ applications derive $ (ex,spo,ty)$, violating constraint $ _7$ itemize [$ [?q_2/spo,?p/?x,?q/?y ]\>:\>$] $ (?x,te,?y), (?x,ex,?y), (ex,spo,?q_1), (?x,?q_1,?y), (?q_1,spo,spo), (?x,spo,?y), (?x_1,?x,?y_1) (?x_1,?y,?y_1)$ itemize [$ $] chain rejected because $ _3$ derives $ (ex,spo,spo)$, violating constraint $ _6$ itemize description description of these passed the conditions in A line_new_restr or A line_new_negr of the algorithm, so no new edges were added to $ $. Therefore, A line_return_false will not find cycles and A line_return_true is reached, concluding that $ ’_P1$ indeed is chain-stratified under constraints. document