arXiv CSopen access

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)⋆ Nils Küchenmeister1 , Alex Ivliev1 , Dörthe Arndt2 , and Markus Krötzsch1 Knowledge-Based Systems Group, TU Dresden, Dresden, Germany Computational Logic Group, TU Dresden / ScaDS.AI, Dresden/Leipzig, Germany [email protected] 1

arXiv:2607.28778v1 [cs.LO] 30 Jul 2026

2

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. Keywords: rules languages · N3 · SHACL · Datalog · full stratification

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 [20,3,13]. Attempts to establish corresponding web standards have been less successful [12,14], but ongoing works on N3 [22] and SHACL Rules [6] may yet change this. Even without standardised syntax, today’s rule languages share a common semantic basis — the classical language Datalog [17] — 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 ⋆

This is the technical report accompanying our ISWC26 paper [18].

2

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

operations are only applied to data that has been fully computed [17]. 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 [2]. 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 [7]. Non-termination may still occur, and analysing rules to preclude (potential) feedback cycles can help detect such problems [2,4]. The working drafts for N3 [22] and SHACL Rules [6] 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. 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,3 which means that any use of negation prevents stratification. SHACL proposes a refined unification-based dependency analysis [6, Section 3.4 “Stratification”], which helps when triples contain constants, as these N3 rules:4 1 {?c 2 {?c

:participant ?p} => {?p rdf:type :Student}. :teacher ?p . [] log:notIncludes {?p rdf:type :Student}} => {?c :examiner ?p}.

The rule in L1 states that every participant ?p of some course ?c is a student. The rule in L2 means that course teachers who are not students are also examiners for the course, where [] log:notIncludes {· · · } is N3 syntax for negation. SHACL’s stratification method orders L1 before L2, 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 [10]: 3 {?p 4 {?p

rdfs:subPropertyOf ?q . ?q rdfs:subPropertyOf ?r} => {?p rdfs:subPropertyOf ?r}. rdfs:subPropertyOf ?q . ?x ?p ?y} => {?x ?q ?y}.

The all-variable triples in rule rdfs7 (L4) create dependencies from and to any other rule, making stratification impossible. Indeed, using all the rules L1–L4, 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 L2. Similar issues would arise if :examiner Such ternary predicates are also how relational rule engines import RDF [13]. 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. 4 We use prefixes rdf:, rdfs:, and log: for the standard namespaces [5,22]. 3

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

3

were a subproperty of rdfs:subPropertyOf or rdf:type. These cases are unintended and would likely indicate errors, which N3 can express using constraints: 5 {:examiner

rdfs:subPropertyOf :participant} => false. rdfs:subPropertyOf rdfs:subPropertyOf} => false. 7 {:examiner rdfs:subPropertyOf rdf:type} => false. 6 {:examiner

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: 8 {?x

rdf:type :Human} => {?x :father _:1 . _:1 rdf:type :Man}.

Given (a) :jo rdf:type :Human, applying L8 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 [16, Ex. 6]: 9 {?x

:father ?y} => {?y rdf:type :Man}. :father ?y} => {?y :eq ?y}. 11 {?x :father ?y1. ?x :father ?y2. [] log:notIncludes {?y1 :eq ?y2}} => {?y1 :nef ?y2}. 10 {?x

L9 defines a range for :father. L10 derives a simple equality, which is negated in L11 to check for non-equal fathers (:nef). Given triples (a) and (b), we could apply L8 to create a fresh bnode _:a (:bob does not satisfy the conclusion at this point). Rules L9 and L10 would then produce (c), :bob :eq :bob and _:a :eq _:a, and L11 would yield :bob :nef _:a and _:a :nef :bob. In contrast, if we apply L9 first, then L8 will not apply, and no :nef-triple follows. The issue is serious: classically stratified RDF rule sets do not have a welldefined semantics. Indeed, L8–L11 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. We might hope to avoid this issue by interleaving rule applications with additional algorithms to find and delete redundant bnodes, creating a lean RDF graph [11] (or core [7]). But even this (costly) workaround does not solve the problem: we can just apply L9 last. As another solution, Krötzsch proposed a new type of dependency for rules with bnodes (existential variables) in their conclusion [16]. 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 (L4). 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

4

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

Krötzsch’s reliances [16], recalled in the preliminaries (Section 2), which define several types of binary relations between rules to estimate potential interactions. We 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 3, 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 4), which allows us to introduce chain stratification and to show that it meets our requirements (Section 5). Deciding 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 6). To show its practical feasibility, Section 8 presents a prototype implementation that builds upon algorithmic methods for reliances [9], 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.

2

Preliminaries

We briefly define rules and recall required notions about reliances [16]. We use first-order notation with predicates (not just triple) — our results apply to N3 (under common syntax translations [1]) but also to other rule languages [14,13,3]. Rules We use countably infinite, mutually disjoint sets P (predicates), V (variables), C (constants), and N (nulls). Each predicate p ∈ P has an arity ar(p) ≥ 0. An atom is an expression p(t) with p ∈ P and t ∈ (V ∪ C ∪ N )ar(p) a list. A fact is a variable-free atom, and a database is a set I of facts. Negation is denoted ¬. We often treat lists and conjunctions of (negated) atoms as sets. For any expression or set of expressions E, var(E) is the set of variables in E. A rule ρ is a null-free expression ρ : body+ (ρ) ∧ body− (ρ) → ∃z. head(ρ), where z is a variable list, body+ (ρ) and head(ρ) are conjunctions of atoms, and body− (ρ) is a conjunction of negated atoms. Variables var∃ (ρ) = z are existential, all others var∀ (ρ) = var(ρ) \ z are universal (as usual, we omit their quantifiers). Universal variables in head(ρ) are frontier variables. All universal variables in head(ρ) and body− (ρ) must occur in body+ (ρ) (safety). A rule ρ is Datalog if body− (ρ) = ∅ and var∃ (ρ) = ∅. A ruleset R is a finite set of rules; then RD ⊆ R is the subset of Datalog rules. Constraints as in L5–L7 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 head(ρ) is a minimal non-empty set ψ ⊆ head(ρ) such that var∃ (ψ) is disjoint from var∃ (head(ρ) \ ψ). Let pieces(ρ) = {∃var∃ (ψ).ψ |

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

ψ a piece of head(ρ)}, and pieces(R) = each ρ ∈ R has just one piece.

S

5

ρ∈R pieces(ρ). R is piece-decomposed if

Example 1. The rule a(x) → ∃v, w. b(x), r(x, v), b(v), s(x, w) has three pieces: b(x), ∃v. r(x, v), b(v) and ∃w. s(x, w). Matches and models A substitution is a partial mapping σ : V → (V ∪ C ∪ N ). For t ∈ V ∪ C ∪ N , we set tσ = σ(t) if σ(t) is defined, and tσ = t otherwise. Substitutions extend to (sets of) logical expressions as usual. Rule ρ matches database I if there is a substitution µ∀ defined on var∀ (ρ) such that body+ (ρ)µ∀ ⊆ I and body− (ρ)µ∀ ∩ I = ∅. We denote matches as pairs ⟨ρ, µ∀ ⟩. Match ⟨ρ, µ∀ ⟩ is satisfied by I if there is a substitution µ∃ defined on var∃ (ρ) such that head(ρ)µ∀ µ∃ ⊆ I. I is a model of ρ (or satisfies ρ, written I |= ρ) if it satisfies all matches of ρ over I. I models a ruleset R if I |= ρ for all ρ ∈ R, and I models a null-free database J if J ⊆ I. The Chase Algorithms that construct models for a given database and ruleset are called chase procedures. We use the following standard chase: Definition 1. A chase C for a null-free database I and ruleset R is a (possibly infinite) sequence of databases dbC (0), dbC (1), . . . such that dbC (0) = I and: (1) for each i > 0, there is ruleC (i) ∈ R and matchC (i) = ⟨ruleC (i), µ∀ ⟩, such that (a) matchC (i) is unsatisfied in dbC (i − 1), and (b) dbC (i) = dbC (i − 1) ∪ {head(ruleC (i))µ∀ µ∃ } for an injective function µ∃ : var∃ (ruleC (i)) → N that maps variables to distinct fresh nulls (not occurring in dbC (i − 1)); (2) if ⟨ρ, µ⟩ is a match over dbC (i) for some i ≥ 0, then there is j ≥ i such that ⟨ρ, µ⟩ is satisfied in dbC (j) (fairness). The S set of chase steps is stepsC ⊆ N. The result of a chase is chaseC (I, R) = i∈stepsC dbC (i). C is generating if every matchC (i) is a match in chaseC (I, R). In situations like (1), we say dbC (i) was obtained by applying ruleC (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 R has no existentials, the results of generating chases are exactly the stable models [15]. If R is Datalog, chaseC (I, R) is the unique perfect model, and we omit C . Likewise, the chase result is the unique perfect model if R is stratified : Let preds(A) be the set of predicates used in the set of atoms A, and for ◦ ∈ {+, −}, let ≺◦preds := {⟨ρ1 , ρ2 ⟩ ∈ R2 | preds(head(ρ1 )) ∩ preds(body◦ (ρ2 )) ̸= ∅}. Then an existential-free ruleset R is called (classically) stratified if it can be partitioned into R = S0 ∪˙ . . . ∪˙ Sn such that for all ρi ∈ Si and ρj ∈ Sj we have that ρ i ≺+ ≺− preds ρj implies i ≤ j, and ρi S preds ρj implies i < j. Typically, it is also required that the sets of predicates ρ∈Si preds(head(ρ)) defined by the strata Si − ⋆ are disjoint, which is inessential. R is stratified iff (≺+ preds ) ◦ ≺preds is acyclic. A chase exhaustively applying rules from the strata in order is clearly generating. Things are not so simple with ∃ (cf. Section 1, Problem 2). Universal models and cores Models with nulls are compared using homomorphisms (see [16] for a definition). A model U of R and I is universal

6

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

if all other models M of R and I have a homomorphism to U. Universality is the basis for answering monotonic queries [7]. A core is a database without “redundant nulls”, which can be defined on finite databases I by requiring that every homomorphism I → I is surjective (the infinite case is more subtle [16]). 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 2. Let Ia ⊆ Ib be databases, such that Ia was obtained by applying ρ for µ. A mapping µA : var(ρ) → C ∪ N is an alternative match for ⟨ρ, µ⟩ over Ib if (1) head(ρ)µA ⊆ Ib , (2) xµ = xµA for all x ∈ var∀ (ρ), and (3) there is a null in head(ρ)µ that is not in head(ρ)µA . An alternative match in a chase C is one that uses Ia = dbC (i), ρ = ruleC (i), and Ib = chaseC (I, R). 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 [16, Thms 4 & 11]. Moreover, rules L8–L11 have generating chases C and C ′ where all databases dbC (′) (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 R is a strict partial order ≺ ⊆ R × R. A chase C violates ≺ if ruleC (i) ≺ ruleC (j) for some i > j. C respects ≺ if, for every step i, dbC (i) has no unsatisfied match ⟨ρ, µ⟩ with ρ ≺ ruleC (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 [9]. Definition 3. Rule ρ2 positively relies on rule ρ1 , written ρ1 ≺+ ρ2 , if there are databases Ia ⊆ Ib such that Ib was obtained from Ia by applying ρ1 for µ1 , and there is an unsatisfied match ⟨ρ2 , µ2 ⟩ over Ib that is not a match over Ia . Definition 4. Rule ρ2 negatively relies on rule ρ1 , written ρ1 ≺− ρ2 , if there are databases Ia ⊆ Ib such that Ib was obtained from Ia by applying ρ1 for µ1 , and there is an unsatisfied match ⟨ρ2 , µ2 ⟩ over Ia that is not a match over Ib . Definition 5. Rule ρ1 restrains rule ρ2 , written ρ1 ≺□ ρ2 , if there are databases Ia ⊆ Ib such that (1) Ia was obtained by applying ρ2 for µ2 , (2) Ib was obtained by applying ρ1 for µ1 , and (3) there is an alternative match µA for ⟨ρ2 , µ2 ⟩ over Ib that is not an alternative match over Ib \ head(ρ1 )µ1 . The 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. A ruleset R 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 [16]. The conditions can be relaxed if negation is only used for some predicates [8].

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

3

7

Trails: Refining Transitive Positive Reliances

To 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 [16], 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. To represent sequences of matches, we will use words over an infinite set of rule instances (individually denoted by ρ̂): instances(R) := {ρθ | ρ ∈ R, θ : var(ρ) → (V \ var(R))}

(1)

Example 2. Below, rules ρ1 , ρ2 and ρ3 on the left are shown with one of their (infinitely many) instances on the right: ρ̂1 : t(x1 , y1 , x1 ), q(x1 , y1 ) → p(x1 , x1 ) ρ1 : t(x, y, z), q(x, y) → p(x, z) ρ2 : p(x, x) → ∃v. s(x, v), t(v, v, v) ρ̂2 : p(x1 , x1 ) → ∃v1 . s(x1 , v1 ), t(v1 , v1 , v1 ) ρ3 : q(x, y), s(x, z), a(z) → t(x, x, z) ρ̂3 : q(x1 , y1 ), s(x1 , v1 ), a(v1 ) → t(x1 , x1 , v1 ) The rule instance ρ̂1 was obtained from rule ρ1 by applying the variable substiθ θ θ tution x 7− → x1 , y 7− → y1 , z 7− → x1 , collapsing variables x and z. We will reuse these rules as a running example throughout Sections 3–5. Together with a fixed arbitrary bijection ω : (V \ var(R)) → C ∪ N , 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 instances(R). As the chase algorithm always maps existentials to fresh nulls, we require these words to use fresh variables: Definition 6. A finite sequence (ρ̂i )i=1,...,n ∈ instances(R)∗ of rule instances ρ̂i ∈ instances(R) with pairwise disjoint existential variables is called ∃-disjoint. Example 3 (cont.). The sequence of instances ρ̂1 ρ̂2 ρ̂3 is ∃-disjoint, as the only existential variable v1 is fresh in ρ̂2 . (It can be used universally again, as in ρ̂3 .) Such 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 7. 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 : {1, . . . , n} → stepsC , such that for all i ∈ {1, . . . , n}

8

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

– ⟨ρ̂i , ω⟩ = matchC (f (i)) and – i > 1 implies body+ (ρ̂i )ω ∩ head(ρ̂i−1 )ω ̸= ∅.

(match correspondence) (causal connection)

We write ρ1 ≺+ t ρ2 if there is a trail from an instance of ρ1 to an instance of ρ2 . + ⋆ Clearly, we have ≺+ t ⊆ (≺ ) , as the databases Ia = dbC (f (i) − 1) and Ib = dbC (f (i)) witness the pairwise positive reliances for all i. ω

ω

ω

Example 4 (cont.). Let cx1 , cy1 ∈ C, nv1 ∈ N , x1 7− → cx1 , y1 7− → cy1 , v1 7− → n v1 . The ∃-disjoint sequence ρ̂1 ρ̂2 ρ̂3 is a trail, as there is a chase C with dbC (0) = {t(cx1 , cy1 , cx1 ), q(cx1 , cy1 )} dbC (1) = dbC (0) ∪ {p(cx1 , cx1 )} dbC (2) = dbC (1) ∪ {s(cx1 , nv1 ), t(nv1 , nv1 , nv1 )} dbC (3) = dbC (2) ∪ {a(nv1 )} dbC (4) = dbC (3) ∪ {t(cx1 , cx1 , nv1 )} and step mapping f : {1, 2, 3} → {1, 2, 3, 4} with 1 7→ 1, 2 7→ 2, 3 7→ 4, assuming a rule, e.g. s(x, y) → a(y), to derive fact a(nv1 ) in step 3. Hence, ρ1 ≺+ t ρ3 . − □ Theorem 1. If ≺+ t ◦ (≺ ∪ ≺ ) 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.

Theorem 1 can be shown by a contrapositive argument, where we take a chase − □ that violates ≺+ t ◦(≺ ∪ ≺ ), 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 ≺□ [16]. − □ Theorem 2. If ≺+ t ◦ (≺ ∪ ≺ ) is a precedence, then the result of every chase of I and R that respects it is unique (up to isomorphism).

Uniqueness is shown by arguing that of two non-isomorphic chases, one must disrespect the precedence. A chase as in Theorem 2 is generating and free of alternative matches by Theorem 1. If finite, this unique result is a core [16, Theorem 11], known as the perfect core model of I and R. Lemma 3. The ≺+ t relation is the smallest relation <, such that respecting < ◦ ≺ ensures non-violation of < ◦ ≺ for acyclic < ◦ ≺ with ≺− ⊆ ≺. Based on proof of Theorem 1 outlined above, this is shown by contradiction. Lemma 3 therefore confirms that our choice of ≺+ t is optimal for our purposes. Theorem 4. For ρ̂1 , ρ̂2 ∈ instances(R), it is undecidable whether ρ̂1 ρ̂2 is a trail. Theorem 4 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 1. As a direct consequence of Theorem 4, 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. + ⋆ Consequently, we are looking for a decidable relation between ≺+ t and (≺ ) .

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

4

9

Chains: A Decidable Approximation

+ ⋆ By Section 3, ≺+ t is the smallest sub-relation of (≺ ) that sufficiently captures when one rule application may enable another. We now develop a decidable + overestimation of ≺+ t based on positive reliance checks. When checking ≺ , it + suffices to consider instances under ω, which leads to ≺≺ as a special case:

Definition 8. For ρ̂1 , ρ̂2 ∈ instances(R), we write ρ̂1 ≺≺+ ρ̂2 , if ρ̂1 ≺+ ρ̂2 with Ia = (body+ (ρ̂1 ) ∪ (body+ (ρ̂2 ) \ head(ρ̂1 )))ω, and µ1 = µ2 = ω. Above, database Ia and matches µ1 and µ2 refer to Definition 3. Example 5 (cont.). It is clear that ρ̂1 ≺≺+ ρ̂2 , as ⟨ρ̂2 , ω⟩ is no match on database Ia = {t(cx1 , cy1 , cx1 ), q(cx1 , cy1 )}, but applying the unsatisfied match ⟨ρ̂1 , ω⟩ yields Ib = Ia ∪ {p(cx1 , cx1 )} where ⟨ρ̂2 , ω⟩ is an unsatisfied match. It 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 body+ (ρc ) and keeping the head of ρ̂k as head(ρ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 body+ (ρc ). Definition 9. An ∃-disjoint sequence of rule instances c = ρ̂1 , . . . , ρ̂k can be extended by ρ̂ ∈ instances(R) if ρc ≺≺+ ρ̂, where ρc is the chain rule S  S  + i∈{1,...,k} body (ρ̂i ) ∪ i∈{1,...,k−1} head(ρ̂i ) → ∃var∃ (ρ̂k ). head(ρ̂k ) (2) Definition 10. 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 . Example 6 (cont.). To see that c = ρ̂1 ρ̂2 ρ̂3 is a chain, check that ρ̂1 is a chain of length 1, ρρ̂1 ≺ ≺+ ρ̂2 (see Example 5), and ρρ̂1 ρ̂2 ≺≺+ ρ̂3 where the chain rule for ρ̂1 ρ̂2 is ρρ̂1 ρ̂2 : t(x1 , y1 , x1 ), q(x1 , y1 ), p(x1 , x1 ) → ∃v1 . s(x1 , v1 ), t(v1 , v1 , v1 ). Remark 2. Every trail is a chain. Although 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 11. For a sequence s = ρ̂1 , . . . , ρ̂n , the set of stale variables is: S stale(s) := i,j∈{1,...,n}.j<i ((var∀ (ρ̂i ) \ var(head(ρ̂i−1 ))) ∩ var∀ (ρ̂j )) (3) If stale(s) = ∅, then s is decoupled.

10

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

Decoupled chains are special because the only variables re-used in the ith instance are frontier and existential variables stemming from the (i−1)th instance. Example 7 (cont.). The sequence t = ρ̂1 ρ̂2 ρ̂3 is not decoupled, as y1 is re-used in ρ̂3 although not present in var(head(ρ̂2 )) = {x1 , v1 } and thus stale(t) = {y1 } ̸= ∅. This shows that trails are not always decoupled. We can, however, relate each trail to a decoupled chain. A B B Definition 12. A sequence ρ̂A 1 , . . . , ρ̂n generalises a sequence ρ̂1 , . . . , ρ̂n if there A B is a variable substitution σ : V → V , such that ρ̂i σ = ρ̂i for all i ∈ {1, . . . , n}.

Example 8 (cont.). 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 = id and θ3 with y1 7→ y2 . Then c = (ρ̂1 θ1 )(ρ̂2 θ2 )(ρ̂3 θ3 ) is decoupled, and c generalises t with σ = θ1−1 ◦ θ2−1 ◦ θ3−1 , which simply replaces y2 by y1 . Lemma 5. Every trail can be generalised by a decoupled chain. Lemma 5 is shown by naming the trail’s stale variables apart, along the lines of Example 8. 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 Ia and Ib 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 9 (cont.). Database Ia from Definition 8 will, in addition to q(cx1 , cy1 ), contain a fact q(cx1 , cy2 ) matching body+ (ρ̂3 θ3 ) with named apart variable y2 . For ruleset R, we collect all decoupled chains in set chains(R) ⊆ instances(R)∗ , which may be infinite. We write ρ1 ≺+ c ρ2 if there is a decoupled chain between + instances of ρ1 and ρ2 . With Lemma 5, we know that indeed ≺+ t ⊆ ≺c , hence: − □ Corollary 6 (of Theorem 1). A chase that respects ≺+ c ◦ (≺ ∪ ≺ ) does not − □ violate ≺ or ≺ , and therefore is generating and free of alternative matches.

However, as the following example shows, there are decoupled chains that do + not generalise any trail, i.e. ≺+ t ⊂ ≺c (the containment is proper). Example 10 (cont.). Recall that—in order to give the witnessing chase for the trail t = ρ̂1 ρ̂2 ρ̂3 in Example 4—we had to assume the existence of a rule to derive a fact a(nv1 ) after applying instance ρ̂2 , which invented the null nv1 . This fact cannot originate from the input database, as it pertains to a null. If, however, the full ruleset were R = {ρ1 , ρ2 , ρ3 }, t would not be a trail (but still a chain). If c = ρ̂1 , . . . , ρ̂n is a chain, then ρ̂i ≺+ ρ̂i+1 for i ∈ {1, . . . , n − 1}, but the + ⋆ reverse does not hold, as attested below: The inclusion ≺+ c ⊂ (≺ ) is proper.

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

11

Example 11. Consider the rules ρ1 : r(x, y), a(y) → b(x), ρ2 : b(x) → c(x), and ρ3 : c(x) → ∃v. 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 head(ρ3 ) is already satisfied for any match of ρ3 introduced by applying ρ1 + ⋆ and then ρ2 . Therefore, the relation ≺+ c is indeed a proper sub-relation of (≺ ) . □ − In Section 5 we further refine the composition of ≺+ c with ≺ and ≺ , and use it to introduce chain stratification. Afterwards, in Section 6, we examine how ≺+ c can be computed despite the fact that chains could be arbitrarily long.

5

Rule Selection for Chain-Stratified Rulesets

− □ − Having established that respecting ≺+ c ◦ (≺ ∪ ≺ ) prevents violation of ≺ □ and ≺ , we now take a closer look at the negative or restraint reliance after − + and ≺□ the chain’s last instance: We introduce relations ≺− c ⊂ c ⊂ ≺c ◦ ≺ + □ ≺c ◦ ≺ , and use them to demarcate a class of rulesets which we call (fully) chain-stratified. These subsume fully stratified rulesets [16].

Definition 13. 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 ∈ R, then we write ρ1 ≺□ c ρ. + □ Clearly, ρ1 ≺□ c ρ implies ρ1 ≺c ◦ ≺ ρ, but the reverse does not hold:

Example 12 (cont. of Ex. 10). The last instance ρ̂3 restrains both rules ρ4 : p(x, x) → ∃v.t(v, x, v) and ρ5 : q(x, y) → ∃v. t(x, y, v) but ρc only restrains ρ5 . + □ Respecting ≺□ c still prevents (≺c ◦≺ )-violations causing alternative matches.

Lemma 7. 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 ruleC (i) has an alternative match over dbC (f (n)) but not over dbC (f (n) − 1), then ρ̂1 ≺□ c ruleC (i). This is shown by obtaining a pair of databases from the offending chase and applying Definition 5. Negative reliances are treated similarly: Definition 14. A rule ρ negatively relies on a chain c = ρ̂1 . . . ρ̂n if ρc ≺− ρ. If ρ̂1 is an instance of ρ1 ∈ R, then we write ρ1 ≺− c ρ. Lemma 8. 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 matchC (i) is a match for ruleC (i) over dbC (f (n) − 1) but not over dbC (f (n)), then ρ̂1 ≺− c ruleC (i). With the above improvements, we can finally define our novel stratification condition, which we call chain stratification: Definition 15. A ruleset R is core chain-stratified if ⟨R, ≺□ c ⟩ is acyclic. It is □ (fully) chain-stratified if ⟨R, ≺− ∪ ≺ ⟩ is acyclic. c c

12

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

Corollary 9 (of Theorems 1 and 2, and Lemma 5). On a chain-stratified □ ruleset the result of any chase that respects ≺− c ∪ ≺c is generating, alternative match-free, and unique (up to isomorphism). If finite, it is a perfect core model. □ For chain-stratified rulesets, the rule precedence ≺− c ∪ ≺c induces a “stratification” where rules may belong to multiple strata, obtained by first computing the minimum-rank layering L0 . . . Ln of the precedence, and then forming strata S Si = j≤i Lj . Successively chasing fixpoints for S0 . . . Sn ensures that no new □ unsatisfied matches for any (≺− c ∪ ≺c )-predecessors of Si are added.

6

The Regular Language of Chains

We now address the issue of deciding whether there is an (arbitrarily long) decoupled chain connecting instances of two given rules. Enumerating the set chains(R) merely yields a semi-decision procedure, because a ruleset can have infinitely many chains. Therefore, we characterise chains(R) with a language LR and establish that LR is regular, which yields a decision procedure. Our restriction to decoupled chains (Section 4) is essential for this to work. We assign to each c ∈ chains(R) 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 R, but in bounded space that does not grow arbitrarily with (the body of) ρc . This requires some auxiliary notation. For ruleset R, the finite set variants(R) := {ρθ | ρ ∈ R, θ : var(ρ) → var(R)} is obtained by replacing variables in R by any combination of variables found in R. Further, let orig : instances(R) → variants(R) be an arbitrary but fixed mapping such that ρ̂ = orig(ρ̂)θorig(ρ̂) with injective variable renaming θorig(ρ̂) . Example 13 (cont. of Ex. 2). Let R = {ρ1 , ρ2 , ρ3 }. Then var(R) = {x, y, z, v} and, e.g., ρ̌a1 : t(v, z, y), q(v, z) → p(v, y) and ρ̌b1 : t(x, y, x), q(x, y) → p(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 orig(ρ̂1 ) = ρ̌b1 with the injection θorig(ρ̂1 ) : x 7→ x1 , y 7→ y1 , which yields ρ̂1 = orig(ρ̂1 )θorig(ρ̂1 ) . Moreover, given a set F of formulae ∃v. ψ where ψ is a conjunction of atoms, let parts(F) := {∃ṽ. ψ̃ | ∃v. ψ ∈ F , ψ̃ ⊆ ψ, ψ̃ ̸= ∅, ṽ = v ∩ var(ψ̃)}. Example 14. Consider the set parts(pieces(variants(R))) of “partial pieces of rule variants.” The rule a(x) → ∃v. r(x, v), b(v) has a single piece, and contributes three partial pieces: (1) ∃v. r(x, v), b(v), (2) ∃v. r(x, v), and (3) ∃v. b(v). Another variant of the same rule is a(x) → r(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). To understand how we label a chain c, consider the chain rule ρc and some rule ρ ∈ R. To check ρc ≺+ ρ, Definition 3 requires Ia and Ib such that: (i) the positive body of ρ matches Ib but not Ia (i.e., ρc contributed something relevant to Ib ); (ii) the negative body of ρ is not matched in Ib ; and (iii) applying

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

13

ρ adds something over Ib (match unsatisfied). To check these, we store three components: (C) pieces of ρc that contribute new facts when applying ρc (⇝ (i)); (S) partial pieces satisfied after applying ρc (⇝ (iii)); and (N) variants of rules inhibited by negative body atoms after applying ρc (⇝ (ii)). Now we can define the finite alphabet Σ := 2H × 2F × 2variants(R) where H := pieces(variants(R)) and F := parts(H). To define the labelling function ℓ, consider a chain c = ρ̂1 . . . ρ̂n with chain rule ρc , and let θn := θorig(ρ̂n ) ,
i.e., ρ̂n = orig(ρ̂n )θn . Moreover, let Ic := body+ (ρc ) ∪ head(ρc ) θn−1 ω, which represents the necessary facts in Ib when checking ρc ≺+ ρ for any ρ ∈ R (Definition 3), in the notation of Definition 8 with the fixed mapping ω. We define ℓ(c) = ⟨ℓC (c), ℓS (c), ℓN (c)⟩ where: ℓC (c) := {∃v.ψ̃ ∈ pieces(orig(ρ̂n )) | ψ̃θn ̸⊆ body+ (ρc )}

(4)

S

(5)

ℓ (c) := {∃ṽ.ψ̃ ∈ F | Ic |= ∃ṽ.ψ̃ω∀ } +

N

−

ℓ (c) := {ρ̌ ∈ variants(R) | Ic ∪ body (ρ̌)ω ∩ body (ρ̌)ω ̸= ∅}

(6)

where ω∀ is the restriction of ω to universal variables. Note that ℓC (c) contains all head pieces of ρc except possibly Datalog atoms. The main correctness property of ℓ is this: if ℓ(c1 ) = ℓ(c2 ) for chains c1 and c2 , then for all ρ ∈ R and all ≺ ∈ {≺+ , ≺− , ≺□ }, we have that ρc1 ≺ ρ iff ρc2 ≺ ρ. 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: Lemma 10. Let c1 , c2 ∈ chains(R) with ℓ(c1 ) = ℓ(c2 ). If c1 ρ̂1 ∈ chains(R) then there is ρ̂2 ∈ instances(R) (both ρ̂1 and ρ̂2 belong to the same ρ ∈ R), such that (i) c2 ρ̂2 ∈ chains(R)

and

(ii) ℓ(c1 ρ̂1 ) = ℓ(c2 ρ̂2 ) .

Part (i) largely follows from the correctness for ≺+ by Definitions 9 and 10. Part (ii) is easy to see for ℓC and ℓN ; for ℓS , it holds because F is closed under parts(variants(·)) and the instances added to the end of the chains are decoupled. The word function is w : chains(R) → Σ ∗ with c 7→ ℓ(c) for |c| = 1, c 7→ w(cpre )ℓ(c) for c = cpre ρ̂n . The language of chains is LR = {w(c) | c ∈ chains(R)}. Now given two words u, v ∈ LR with u|u| = v|v| , uw ∈ LR implies vw ∈ LR for any w ∈ Σ ∗ , which follows from an inductive application of Lemma 10. 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: Theorem 11. The language LR is regular. Algorithm 1 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 A4) for rules in the range of ≺− or ≺□ ; □ − □ this suffices since we search for ≺− c ∪ ≺c -cycles and ≺c ∪ ≺c only ranges over such rules. We then iteratively extend C and ≺ (A5) until a cycle is found (A6) or all chains have been considered and no cycle found (A17). For each ρc ≺+ ρ, we consider all concrete mappings η such that ρc η ≺≺+ ρ̂η (A9), if the η-specific

14

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

Algorithm 1: Is ruleset R chain-stratified? Grel := ⟨R, ≺+ , ≺− , ≺□ ⟩; // compute the reliance graph − □ 2 if Grel has no cycle via ≺ ∪ ≺ then : return “R is fully stratified” ; − □ □ 3 ≺ := ≺ ∪ ≺ ; // precedence from Grel (will approach ≺− c ∪ ≺c ) ′ ′ − ′ □ 4 C := {⟨ρ, ρ, ρ, ϵ⟩ | ρ ∈ R and there is ρ ∈ R with ρ ≺ ρ or ρ ≺ ρ in Grel }; + + 5 for ⟨ρ1 , ρn , ρc , w(cpre )⟩ ∈ C and ρ ∈ R with ρn ≺ ρ in Grel and ρc ≺ ρ : 6 if ≺ is cyclic then : return “R is not chain stratified”; 7 ρ̂ := injectively rename ρ, such that it does not use var(ρc ); 8 V := var(head(ρc ) ∪ body+ (ρ̂)); C := symbols(head(ρc ) ∪ body+ (ρ̂)); 9 for η : V → V ∪ C with ρc η ≺ ≺+ ρ̂η : 10 if ℓ(cη) ∈ w(cpre ) then : Continue; 11 ρcηρ̂η := (body+ (ρc ) ∪ head(ρc ) ∪ body+ (ρ̂))η → ∃var∃ (ρ̂)η. head(ρ̂)η; 12 C := C ∪ {⟨ρ1 , ρ, ρcηρ̂η , w(cpre )ℓ(cη)⟩}; 13 for ρ′ ∈ R with ρ ≺□ ρ′ in Grel : 14 if ρcηρ̂η ≺□ ρ′ then : ≺ := ≺ ∪ {⟨ρ1 , ρ′ ⟩} ; 15 for ρ′ ∈ R with ρ ≺− ρ′ in Grel : 16 if ρcηρ̂η ≺− ρ′ then : ≺ := ≺ ∪ {⟨ρ1 , ρ′ ⟩} ; 17 return “R is chain stratified”; 1

chain’s label was not encountered yet (A10). Since chains are extended stepwise, presence of a label in w(cpre ) means a label-equivalent chain was already considered (and all related restraints and negative reliances found). Then we construct the extended chain rule (A11), add the new chain (A12, this adds to the cases iterated in A5), and add new pairs to ≺ (A13–16). Keeping 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 10 generalises to chains with isomorphic labels.

7

Further Improving Chain Stratification

Chain stratification generalises full stratification, which controls the interaction of value invention and negation, and solves, e.g., Problem 2 (L8–L11) of Section 1. 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., Ia in Def. 3. If the Datalog rules RD ⊆ R entail ⊥ on these facts, then the reliance can be discarded [19]. For chains c, we could apply RD to Ic (see Section 6), but for Algorithm 1 to be correct, we also must ensure that the label (not the specific chain) determines if ⊥ is derived or not. We therefore consider additional formulae B to capture partial matches of Datalog rule bodies: B := parts({∃v. body+ (ρ̌) | ρ̌ ∈ variants(R)D , v ⊆ var∀ (ρ̌)}). In ℓ(c), we will replace ℓS (c)  ⊆ F (5) by ℓSD (c) ⊆ F ∪B. We convert sets S ⊆ F ∪B S to databases toDb(S) := ψ̃ω∀ µ∃ | ∃ṽ.ψ̃ ∈ S, µ∃ : v 7→ fresh(v, ∃ṽ.ψ̃) , using the mapping ω and an auxiliary injection fresh : var(S) × S → N \ (var(R)ω).

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

15

For chain c = ρ̂1 . . . ρ̂n with θi := θorig(ρ̂i ) , we recursively define ℓSD (c), where we use Prec := ∅ if n = 1 and Prec := toDb(ℓSD (ρ̂1 . . . ρ̂n−1 ))ω −1 θn−1 otherwise: ℓSD (c) := {∃ṽ.ψ̃ ∈ F ∪ B | chase((Prec ∪ body+ (ρ̂n ) ∪ head(ρ̂n ))θn−1 ω, RD ) |= ∃ṽ.ψ̃ω∀ }

(7)

Compared to (5), we replaced Ic by a chase result based on the previous chain label and the new final rule, which has a homomorphism to chase(Ic , RD ). Relying on the previous label lets us lift Lemma 10 and related correctness results to ℓSD . We also recast the extended label as a rule: S −1 ρD θn \ head(ρ̂n ) → ∃var∃ (ρ̂n ). head(ρ̂n ) c : toDb(ℓD (c))ω

(8)

≺+ ρ̂. An ∃-disjoint sequence c can be extended by ρ̂ under constraints if ρD c ≺ + D □D It is a chain if ⊥ ∈ / body (ρc ) and Definition 10 holds. We write ρ1 ≺c ρ2 − □ D ρ2 ) if there is c with ρD (respectively ρ1 ≺−D c ≺ ρ2 (respectively ρc ≺ ρ2 ). c Definition 16. R is chain-stratified under constraints if ≺−D ∪≺□D is acyclic. c c Definition 16 generalises chain stratification since only fewer chains are considered. Correctness is retained if the chase prioritises Datalog rules: Corollary 12. If R is chain-stratified under constraints, a chase that respects ≺D := ≺−D ∪ ≺□D ∪ (RD × (R \ RD )) is generating and alternative match-free. c c The relation ≺D is acyclic if ≺−D ∪ ≺□D is, since ≺D ranges over R \ RD . c c Example 15. We return to Problem 1 (L1–L7), denoting the respective rules ρ1 , . . . , ρ7 . For R = {ρ1 , ρ2 , ρ3 , ρ4 }, we find reliances ρ1 ≺− ρ2 , ρ3 ≺+ ρ3 , ρ4 ≺− ρ2 , and ρ ≺+ ρ4 ≺+ ρ for all ρ ∈ R (due to the all-variable triple ?x ?p ?y in L4). R is not fully stratified, e.g., due to ρ2 ≺+ ρ4 ≺+ ρ1 ≺− ρ2 . R is not chain stratified either. For clarity, we substitute constants from the image of ω directly. To construct a chain for ρ2 ρ4 ρ1 , consider instances ρ̂2 = ρ2 , ρ̂4 = ρ4 [?p/:examiner,?q/:participant,?x/?c,?y/?p], and ρ̂1 = ρ1 . Then ρ̂2 is a length-1 chain, and ρ̂2 ρ̂4 is a chain since ρ̂2 ≺≺+ ρ̂4 , with chain rule ρ2,4 : 12 {?c 13

:teacher ?p . :examiner rdfs:subPropertyOf :participant . ?c :examiner ?p} => {?c :participant ?p}.

− We have ρ2,4 ≺ ≺+ ρ̂1 , so ρ̂2 ρ̂4 ρ̂1 is a chain, hence ρ2 ≺+ c ρ1 . Similarly, ρ2,4,1 ≺ − ρ2 , so we have a cycle ρ2 ≺c ρ2 , and R is not chain stratified. However, the extended R = {ρ1 , . . . , ρ7 } is chain stratified under constraints, where RD = R \ {ρ2 }. The ≺+ -paths from ρ2 to ρ1 that do not revisit ρ2 or pass through ρ1 can be described by a regular expression ρ2 (ρ4 ρ∗3 )∗ ρ4 ρ1 , and each such path corresponds to one or more chains. Similarly, ρ2 (ρ4 ρ∗3 )∗ ρ4 , for ρ2 to ρ4 . All chains from ρ2 to ρ1 violate constraints ρ5 or ρ6 , and the chains from ρ2 to ρ4 that negatively rely on ρ2 violate constraint ρ7 . The above chain ρ̂2 ρ̂4 ρ̂1 will be discarded due to ρ5 . Since rdfs:subPropertyOf is transitive by ρ3 , longer

16

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

chains of the form ρ2 ρ+ 4 ρ1 entail the same constraint-violating fact. Any alternative chain from ρ2 [?p/rdf:type] to ρ1 via ρ4 [?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 ρ2 . Such chains are discarded due to ρ6 . Similarly, any chain starting like ρ2 ρ+ 4 ρ3 . . . violates ρ6 . All surviving chains of the form ρ2 ρ∗4 ρ4 [?q/rdf:type], whose chain rules negatively rely on ρ2 , are eliminated by ρ7 . The remaining chains (all of the form ρ2 ρ+ 4 ) are unproblematic. Considering chains is still crucial here. For a “full stratification under constraints” (following [19]), we would need to prevent ρ2 ≺+ ρ4 with a stronger constraint such as {:examiner rdfs:subPropertyOf ?q} => false, which would forbid useful triples, e.g., :examiner rdfs:subPropertyOf :teacher. Null awareness When building chain rules as in (2) (or (8) 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 V → N to var∃ (ρ̂k−1 ) and apply it to the chain rule. The latter may thus contain nulls, which can eliminate some irrelevant reliances. S Negation awareness Keeping negations of the atoms i∈{1,...,k} body− (ρ̂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 ℓN (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.

8

Implementation & Evaluation

We implement null- and negation-aware chain stratification under RD -closure in a Rust library5 and a PoC tool using it, which accepts Nemo [13] and VLog [21] syntax, as well as (a subset of) N3 syntax (via a Python transpiler). While 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. [9] in their analysis of core stratification, which consists of 201 piece-decomposed, negationfree rulesets with predicate symbols (not just triple).6 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. 5 6

Source code (ca. 13k LoC) available in the supplementary material statement. They correspond to a subset of the Oxford Ontology Repository, accessed 2025-12-01.

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

17

Overall, 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.

9

Conclusion

We 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 ≺+ c to establish new termination criteria. Finally, we hope that our insights can also contribute to ongoing standardisation activities of RDF rules. Acknowledgments. This work is supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in project number 389792660 (TRR 248, 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 Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), and in DAAD project 57616814 (SECAI, School of Embedded Composite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence. Supplemental Material Statement. The source code of our Rust implementation is published at https://gitlab.com/nkuechen/chaining-reliances/-/tree/iswc26. Refer 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.

References 1. Arndt, D., Mennicke, S.: Existential Notation3 Logic. Theory Pract. Log. Program. 25(3), 304–339 (2025). https://doi.org/10.1017/S1471068425000055, https://doi. org/10.1017/s1471068425000055

18

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

2. Baget, J.F., Leclère, M., Mugnier, M.L., Salvat, E.: On rules with existential variables: Walking the decidability line. Artificial Intelligence 175(9–10), 1620–1654 (2011) 3. Bellomarini, L., Sallinger, E., Gottlob, G.: The Vadalog system: Datalog-based reasoning for knowledge graphs. Proc. VLDB Endowment 11(9), 975–987 (2018). https://doi.org/10.14778/3213880.3213888 4. Cuenca Grau, B., Horrocks, I., Krötzsch, 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) 5. Cyganiak, R., Wood, D., Lanthaler, M. (eds.): RDF 1.1 Concepts and Abstract Syntax. W3C Recommendation (25 February 2014), available at http://www.w3. org/TR/rdf11-concepts/ 6. David, R., Habgood, D., Seaborne, A., Steyskal, S. (eds.): SHACL 1.2 Rules. W3C Working Draft (02 April 2026), available at https://www.w3.org/TR/2026/ WD-shacl12-rules-20260402/ 7. 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). pp. 149– 158. ACM (2008) 8. Ellmauthaler, S., Krötzsch, M., Mennicke, S.: Answering queries with negation over existential rules. In: Proc. 36th AAAI Conf. on Artificial Intelligence (AAAI’22). pp. 5626–5633 (2022). https://doi.org/10.1609/aaai.v36i5.20503 9. González, L., Ivliev, A., Krötzsch, 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ò, G., d’Amato, C. (eds.) Proc. 21st International Semantic Web Conference (ISWC 2022). LNCS, vol. 13489, pp. 267– 283. Springer (2022). https://doi.org/10.1007/978-3-031-19433-7_16 10. Hayes, P., Patel-Schneider, P.F. (eds.): RDF 1.1 Semantics. W3C Recommendation (25 February 2014), available at http://www.w3.org/TR/rdf11-mt/ 11. 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). https://doi.org/10.1145/3068333 12. 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://www.w3.org/Submission/SWRL/ 13. Ivliev, A., Gerlach, L., Meusel, S., Steinberg, J., Krötzsch, 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). pp. 743–754. IJCAI Organization (2024). https://doi.org/10.24963/kr. 2024/70 14. Kifer, M., Boley, H. (eds.): RIF Overview. W3C Working Group Note (22 June 2010), available at http://www.w3.org/TR/rif-overview/ 15. Konczak, K., Linke, T., Schaub, T.: Graphs and colorings for answer set programming. Theory Pract. Log. Program. 6(1-2), 61–106 (2006) 16. Krötzsch, 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). pp. 603–613. IJCAI (2020). https://doi.org/10.24963/kr.2020/60 17. Krötzsch, M.: Modern Datalog: Concepts, methods, applications. In: Artale, A., Bienvenu, M., García, 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). https://doi.org/10.4230/OASIcs.RW.2024/2025.7

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

19

18. Küchenmeister, N., Ivliev, A., Arndt, D., Krötzsch, 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). https://doi.org/tbd 19. Magka, D., Krötzsch, M., Horrocks, I.: Computing stable models for nonmonotonic existential rules. In: Rossi, F. (ed.) Proc. 23rd Int. Joint Conf. on Artificial Intelligence (IJCAI’13). pp. 1031–1038. AAAI Press/IJCAI (2013) 20. Nenov, Y., Piro, R., Motik, B., Horrocks, I., Wu, Z., Banerjee, J.: RDFox: A highlyscalable RDF store. In: et al., M.A. (ed.) Proc. 14th Int. Semantic Web Conf. (ISWC’15), Part II. LNCS, vol. 9367, pp. 3–20. Springer (2015). https://doi.org/ 10.1007/978-3-319-25010-6_1 21. Urbani, J., Jacobs, C., Krötzsch, 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). pp. 258–264. AAAI Press (2016). https://doi.org/10.1609/aaai.v30i1.9993 22. 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/

20

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

A

Proofs for Section 3

In the ensuing proofs, we will use the following additional notation: – matchesR (I) for the set of all matches of rules from R over database I. – unsatR (R) ⊆ matchesR (I) to collect all the unsatisfied matches over I. – homC (k) for µ∀ µ∃ in the extended match matchC (k) = ⟨ruleC (k), µ∀ µ∃ ⟩ applied in step k of chase C. − □ Theorem 1. If ≺+ t ◦ (≺ ∪ ≺ ) 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.

We will show a slightly stronger version of the theorem for ≺+ t ◦ ≺, assuming only that ≺− ⊆≺. (The specifics of ≺□ are irrelevant for the proof.) Proof (of contrapositive of Theorem 1). Let C be a chase sequence that violates ≺. Then there must be chase steps i ≤ k with ruleC (k) ≺ ruleC (i). In fact, i < k as there would otherwise be a self-loop in ≺+ c ◦ ≺. Select such ⟨i, k⟩ (lexicographic) minimally. Define the following sequence of indices: a1 := k ax+1 := min{j | matchC (ax ) ∈ matchesR (dbC (j))}

(9) if i < ax

(10)

This sequence is clearly strictly decreasing (and finite). Also, it has length |a| > 1. For all x < |a|, we have i < ax . Only a|a| may be smaller or equal to i. Due to the minimality of ⟨i, 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 ax that was already available in step j < ax must also be available in all intermediate steps. The second-to-last match matchC (a|a|−1 ) was already applicable in step a|a| ≤ i. We therefore clearly have matchC (a|a|−1 ) ∈ matchesR (dbC (i)). violates ruleC (k) ≺ ruleC (i)

i

chase seq. a|a|

k a1

... a3

a2

The sequence of rule instances t = ρ̂1 , . . . , ρ̂|a| with ρ̂x = ruleC (a|a|+1−x )homC (a|a|+1−x )ω −1

for x ∈ {1, . . . , |a|}

(11)

is a trail, because the chase C with step mapping f : {1, . . . , |a|} → stepsC , f

x 7− → a|a|+1−x fulfils the two conditions from Definition 7. Match correspondence

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

21

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 ax+1 being the minimal chase step where the match used at ax was available. This means that matchC (ax ) must map a body atom of ruleC (ax ) onto a fact added by applying matchC (ax+1 ), i.e. head(ρ̂x ) ∩ body+ (ρ̂x+1 ) ̸= ∅. We thus have ruleC (a|a| ) ≺+ t ruleC (a1 ). As we set a1 = k, we have ruleC (a1 ) = ruleC (k) and we hence ruleC (a1 ) ≺ ruleC (i). This gives ruleC (a|a| ) ≺+ t ◦ ≺ ruleC (i) and both rules were selectable in chase step i. We also know that matchC (a|a| ) ̸= matchC (i), because ≺+ t ◦ ≺ would otherwise have a self-loop. Hence, C disrespects ≺+ ◦ ≺, as match C (a|a| ) t should have been preferred over matchC (i) in chase step i. ⊔ ⊓ − □ Theorem 2. If ≺+ t ◦ (≺ ∪ ≺ ) is a precedence, then the result of every chase of I and R that respects it is unique (up to isomorphism).

Proof (of contrapositive of Theorem 2). Let C1 and C2 be two generating chases of (the same) ⟨I, R⟩ with non-isomorphic results. This can only be the case if there is (w.l.o.g) a match that is applied in C1 but never applied in C2 . Further, there must be such a match, whose application in C1 has added facts which are not present in C2 (‡). Select a minimal i ∈ stepsC1 , such that matchC1 (i) is such a match. All matches applied before i in C1 must therefore be applied at some point in C2 . Let i2 ∈ stepsC2 be the chase step S at which the last of them was applied. The database dbC1 (i − 1) = I0 ∪ k<i head(ruleC1 (k))homC1 (k) must homomorphically map into dbC2 (i2 ) (†). Thus, any unsatisfied match over dbC2 (i2 ) must either (1) also be unsatisfied over dbC1 (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 dbC1 (i − 1). The matchC1 (i) may either be (a) unsatisfied, (b) satisfied, or (c) invalidated7 over dbC2 (i2 ). If (a), then, there must be a k ≥ i2 , such that matchC1 (i) is no unsatisfied match over dbC2 (k) (due to fairness). Applying matchC2 (k) has either (b) satisfied matchC1 (i), or (c) invalidated it. In case (b), ruleC1 (i) cannot be Datalog, as satisfying it would otherwise not have added facts in C1 which C2 lacks (as is required by ‡). Either ruleC1 (i) has both Datalog and existential pieces, which makes it self-restraining. This would mean that C1 − □ does not respect the precedence ≺□ ⊆ ≺+ t ◦ (≺ ∪ ≺ ). Or ruleC1 (i) has only existential pieces, which means that there is an alternative match for matchC1 (i) over dbC2 (k), i.e. ruleC2 (k) ≺□ ruleC1 (i) by Definition 5. In case (c), ruleC2 (k) ≺− ruleC1 (i) by Definition 4. Similar to the proof of Theorem 1 above, we construct a sequence of chase steps from C2 like a1 := k ax+1 := min{j | matchC2 (ax ) ∈ matchesR (dbC2 (j))}

(12) (13)

It is finite, as it is clearly strictly decreasing and all sequence items are nonnegative. In fact, it ends with a|a| = 0. By (†) and because C2 is generating, we 7

by deriving a fact from body− (ruleC1 (i))homC1 (i)

22

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

must be able to find an x, such that either (1) matchC2 (ax ) ∈ unsatR (dbC1 (i−1)), or (2) there exists a ⟨ρ, µ⟩ ∈ unsatR (dbC1 (i − 1)) with appropriate step mapping for C2 witnessing that tpre = ρµω −1 . . . ruleC2 (ax )homC2 (ax )ω −1 is a trail. We then use ax . . . a1 to define a sequence of rule instances t and step mapping f . By Definition 7, C2 and f witness that t is a trail. So we now have that − □ ruleC2 (ax ) ≺+ t ruleC2 (k)(≺ ∪ ≺ )ruleC1 (i). If (1), there is an unsatisfied match − over dbC1 (i − 1) for ruleC2 (ax ) (and clearly also for ruleC (i)). As ≺+ t ◦ (≺ □ ∪ ≺ ) is acyclic by assumption, ruleC (i) ̸= ruleC2 (ax ). So C1 does not respect − ≺+ ∪ ≺□ ), as ruleC2 (ax ) should have been preferred over ruleC1 (i). If t ◦ (≺ + − □ (2), ρ ≺t ruleC2 (ax ) ≺+ t ruleC2 (k)(≺ ∪ ≺ )ruleC1 (i). The sequence tpre t is + − □ also a trail, i.e. ρ ≺t ruleC2 (k)(≺ ∪ ≺ )ruleC1 (i) and ⟨ρ, µ⟩ should have been − □ preferred over ruleC1 (i). Again, C1 disrespects ≺+ ⊓ ⊔ t ◦ (≺ ∪ ≺ ). Lemma 3. The ≺+ t relation is the smallest relation <, such that respecting < ◦ ≺ ensures non-violation of < ◦ ≺ for acyclic < ◦ ≺ with ≺− ⊆ ≺. + Proof. Let < ⊂ ≺+ t be a smaller relation. Then there must be some ρ1 ≺t ρ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 1, select i < k minimally, such that ruleC (k) ≺ ruleC (i) (in fact, ruleC (k) = ρ2 and ruleC (i) = ρ3 ), then construct the sequence (ax )x=1,...|a| , and the trail t = ρ1 , . . . , ρ|a| . In chase step i, both matchC (i) and matchC (a|a| ) are selectable, but not matchC (k). As ρ1 ̸< ρ2 , we do not have ruleC (a| a|) = ρ1 < ◦ ≺ ρ3 = ruleC (i), so C respects < ◦ ≺. ⊓ ⊔

Theorem 4. For ρ̂1 , ρ̂2 ∈ instances(R), it is undecidable whether ρ̂1 ρ̂2 is a trail. Proof (by reduction from the halting problem). Let M be a Turing machine with initial state q0 and single “accept” state qf and let w be a word. It is undecidable whether M has a finite run on w that reaches the “accept” state. – Turing machine M = ⟨Q, Σ, Γ, δ, q0 , qf ⟩ with set of states Q, input alphabet Σ, tape alphabet Γ ⊇ Σ, (partial) transition function δ : Q × Γ → Q × Γ × {L, R}, initial state q0 and final state qf . – Elements of Γ ∗ × Q × Γ ∗ are configurations of M . For δ(q, a) = ⟨q ′ , a′ , d⟩, write ⟨xa, q, by⟩ ⊢ ⟨xa′ b, q ′ , y⟩ iff d = R and ⟨xa, q, by⟩ ⊢ ⟨x, q ′ , a′ by⟩ iff d = L. – For word w ∈ Σ ∗ , a run of M is ⟨w, q0 , ϵ⟩ ⊢ . . .. If this run is finite and ends with qf , then M accepts w. Encode M and w into a ruleset R(M, w) with two designated rules ρ1 , ρ2 ∈ R(M, w), such that ρ1 ≺+ t ρ2 if and only if M holds and accepts w. In detail:

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

Input: ⟨M, w⟩ for word w ∈ Σ ∗ Output: R(M, w) ρ1 :

23

(constants in bold)

→ ∃t0 , x1 , . . . , x|w| . state(t0 , q0 ), pos(t0 , x1 ), tape(t0 , x1 , w1 ), next(x1 , x2 ), . . . , tape(t0 , x|w|−1 , w|w|−1 ), next(x|w|−1 , x|w| ), tape(t0 , x|w| , w|w| ) state(t, s) → ∃t′ . step(t, t′ ) tape(t, x, c) → ∃x′ . next(x, x′ ) tape(t, x, c), pos(t, x′ ), 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′ )

for δ(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′ )

for δ(s, c) = ⟨s′ , c′ , R⟩

ρ2 : state(t0 , q0 ), state(t, qf ) → accept() A restricted chase C of the I and R(M, w) is a faithful simulation, irrespective of I. (Even if I ̸= ∅ 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 I.) 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(t0 , q0 ) atoms occurring both in head(ρ1 ) and body+ (ρ2 ).) Otherwise, no chase with appropriate step mapping exists and t cannot be a trail. ⊓ ⊔

B

Proof for Section 4

Lemma 5. Every trail can be generalised by a decoupled chain. Proof. Let t = ρ̂1 . . . ρ̂n be a trail. By Definition 7, t is ∃-disjoint and there must be a witnessing chase C with step mapping f : {1, . . . , n} → stepsC , such that matchC (f (x)) = ⟨ρ̂x , ω⟩ and head(ρ̂x ) ∩ body+ (ρ̂x+1 ) ̸= ∅. For each i ∈ {1, . . . , n}, consider an injective replacement θ1 = id and for S i > 1 θi : var∀ (ρ̂i ) \ var(head(ρ̂i−1 )) → V \ ( j∈{1,...,i} var(ρ̂j )) of stale variables with fresh ones (as in Example 8). The sequence decoupled(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 V by identity in the usual way.) To show that decoupled(t) is a chain, by Definition 10, we have to show for each k ∈ {1, . . . , n − 1} that ρρ̂1 θ1 ...ρ̂k θk ≺≺+ ρ̂k+1 θk+1 . We have ρ̂i θi σ = ρ̂i for all i ∈ {1, . . . , n}, and hence also ρρ̂1 θ1 ...ρ̂i θi σ = ρρ̂1 ...ρ̂n for the corresponding chain rules (see Equation (2)). So ⟨ρi θi , ω⟩ ∈ S matchesR (Iω −1 θi ω) iff ⟨ρi , ω⟩ ∈ matchesR (I) and ⟨ρρ̂1 θ1 ...ρ̂i θi , ω⟩ ∈ matchesR ( j∈{1,...,i} Iω −1 θj ω) iff S ⟨ρρ̂1 ...ρ̂n , ω⟩ ∈ matchesR (I). Since Iω −1 θi ω ⊆ j∈{1,...,i} Iω −1 θi ω and none of

24

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

the negative body atoms of the matching rules can match S in any of the copies, we further have that matchesR (Iω −1 θi ω) ⊆ matchesR ( j∈{1,...,i} Iω −1 θj ω). Let k ∈ {1, . . . , n − 1} and define
Iδ := head(ρρ̂1 θ1 ...ρ̂k θk ) \ body+ (ρρ̂1 θ1 ...ρ̂k θk ) ω, S Ib := j∈{1,...,k} dbC (f (k))ω −1 θj ω, and Ia := Ib \ Iδ . Now consider the matches λ1 := ⟨ρρ̂1 θ1 ...ρ̂k θk , ω⟩ and λ2 := ⟨ρ̂k+1 θk+1 , ω⟩. We S have λ1 ∈ matchesR ( j∈{1,...,k} dbC (f (k))ω −1 θj ω) = matchesR (Ib ) (see above). Removal of Iδ cannot have removed the match, so λ1 ∈ matchesR (Ib \ Iδ ) = matchesR (Ia ). The match λ1 is unsatisfied over Ia , as Iδ is not contained in Ia . Thus, λ1 ∈ unsatR (Ia ) and the database Ib was obtained by applying λ1 to Ia . Analogously, we have λ2 ∈ unsatR (dbC (f (k))ω −1 θk ω), i.e. λ2 ∈ unsatR (Ib ). Also, λ2 ̸∈ matchesR (Ia ), as it requires facts from Iδ that are only present in Ib . Hence, λ2 ∈ unsatR (Ib ) \ matchesR (Ia ). ⊔ ⊓

C

Proofs for Section 5

Lemma 7. 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 ruleC (i) has an alternative match over dbC (f (n)) but not over dbC (f (n) − 1), then ρ̂1 ≺□ c ruleC (i). Proof. To show ρ̂1 ≺□ c ruleC (i), by Definition 13 we need to give a decoupled chain c that starts with ρ̂1 , such that ρc ≺□ ruleC (i). Obtain c ∈ chains(R) generalising t with σ, by injectively renaming stale variables as in Lemma 5. By Definition 5, we thus need to give databases Ia ⊆ Ib and mappings µ1 , µ2 , with ⟨ruleC (i), µ2 ⟩ ∈ unsatR (Ia′ ) and Ia = Ia′ ∪ head(ruleC (i))µ2 and ⟨ρc , µ1 ⟩ ∈ unsatR (Ia ) and Ib = Ib′ ∪ head(ρc )µ1 , such that there is alternative match for ⟨ruleC (i), µ2 ⟩ over Ib but not over Ib′ . Take Ia′ = dbC (i − 1) and Ia = dbC (i) with µ2 = homC (i). We clearly have ⟨ruleC (i), µ2 ⟩ ∈ unsatR (Ia′ ) and Ia = Ia′ ∪ head(ruleC (i))µ2 by Definition 1. Take Ib′ = dbC (f (n)−1) and Ib = dbC (f (n)). It + is clear that Ia ⊆ Ib , since ≤ f (n)−1. Recall that S  iS  by Equation (2), body (ρc ) = + i∈{1,...,n−1} head(ρ̂i ) and head(ρc ) = head(ρ̂n ). We i∈{1,...,n} body (ρ̂i ) ∪ now have: – body+ (ρc )σω ⊆ Ib′ and Ib′ ̸|= head(ρc )σω∀ , i.e. ⟨ρc , σω⟩ ∈ unsatR (Ib′ ), and – Ib = dbC (f (n) + 1) = dbC (f (n)) ∪ head(ruleC (f (n)))homC (f (n)) = Ib′ ∪ head(ρ̂n )ω = Ib′ ∪ head(ρc )ω. By assumption, we have an alternative match for ruleC (i) over Ib but not Ib′ . ⊔ ⊓ Lemma 8. 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 matchC (i) is a match for ruleC (i) over dbC (f (n) − 1) but not over dbC (f (n)), then ρ̂1 ≺− c ruleC (i).

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

25

Proof. Analogous to the above proof of Lemma 7, we show by Definition 14 ρ̂1 ≺− c ruleC (i) via chain c generalising t with σ as in Lemma 5. By Definition 4 we need to give database Ia and mappings µ1 , µ2 with ⟨ρc , µ1 ⟩ ∈ unsatR (Ia ) and Ib = Ia ∪ head(ρc )µ1 , such that ⟨ruleC (i), µ2 ⟩ ∈ unsatR (Ia ) \ unsatR (Ib ). This is the case for Ia = dbC (f (n) − 1), µ1 = σω and µ2 = homC (i). ⊔ ⊓

D

Proofs for Section 6

Lemma 10. Let c1 , c2 ∈ chains(R) with ℓ(c1 ) = ℓ(c2 ). If c1 ρ̂1 ∈ chains(R) then there is ρ̂2 ∈ instances(R) (both ρ̂1 and ρ̂2 belong to the same ρ ∈ R), such that (i) c2 ρ̂2 ∈ chains(R)

and

(ii) ℓ(c1 ρ̂1 ) = ℓ(c2 ρ̂2 ) .

We will use some auxiliary notation: – When 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. – For databases I1 and I2 and formula set F, we write I1 ≡F I2 , if for all formulae ∃v.ψ̃ ∈ F , we have that I1 |= ∃v.ψ̃ω∀ iff I2 |= ∃v.ψ̃ω∀ . – For database I, we write symbols(I) for the set of constants and nulls occurring in facts of I. S For formula set F, we write symbols(F) = ∃v.ψ∈F var∀ (∃v.ψ)ω for the set of constants and nulls injectively assigned to universal variables of F by ω. – We will apply variants(·) to formula sets, defined exactly like variants(R) (page 12) but using F instead of R. Proof. Let c1 and c2 be two decoupled chains with the same label. Then ℓC (c1 ) = ℓC (c2 ), ℓS (c1 ) = ℓS (c2 ), and ℓN (c1 ) = ℓN (c2 ). Let ρ̂n and ρ̂m be the last rule instances of c1 and c2 , respectively. Further, let θn and θm be the two (unique) injective mappings, such that ρ̂n = orig(ρ̂n )θn and ρ̂m = orig(ρ̂m )θm . Let ρ̂1 ∈ instances(R), such that c1 ρ̂1 is a decoupled chain. By Definition 11, c1 ρ̂1 is decoupled if and only if all variables from var(ρ̂1 ) \ var(head(ρ̂n )) are fresh w.r.t. c1 . By Definitions 10, c1 ρ̂1 is a chain if and only if ρc1 ≺≺+ ρ̂1 . Since θn is injective, we can apply its inverse on both sides and get ρc1 θn−1 ≺≺+ ρ̂1 θn−1 , which means by Definition 8 that, for the database I1 := (body+ (ρc1 ) ∪ head(ρc1 ) ∪ body+ (ρ̂1 ))θn−1 ω, we have (1.a) the intersection between the atom sets (head(ρc1 ) \ body+ (ρc1 ))θn−1 and body+ (ρ̂1 )θn−1 is non-empty, and (1.b) the database I1 does not satisfy ∃v. head(ρ̂1 )θn−1 ω∀ , and (1.c) none of the negative body atoms of ρ̂1 θn−1 are in I1 . Let θ1 be the (unique) injective mapping, such that ρ̂1 = orig(ρ̂1 )θ1 . To prove (i), we want to construct an instance ρ̂2 , such that c2 ρ̂2 is a chain, which is the case if and only if ρc2 ≺≺+ ρ̂2 . Let ρ̂2 := ρ̂1 θn−1 θm be that instance. −1 Since θm is injective, we can apply its inverse on both sides and get ρc2 θm ≺≺+ −1 −1 −1 −1 ρ̂2 θm . Unfolding ρ̂2 , the right-hand side becomes ρ̂2 θm = ρ̂1 θn θm θm = ρ̂1 θn−1 . −1 Unpacking Definition 8 for ρc2 θm ≺≺+ ρ̂1 θn−1 , we need to show for database + −1 I2 := (body (ρc2 ) ∪ head(ρc2 ) ∪ body+ (ρ̂2 ))θm ω, that

26

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

−1 (2.a) the intersection between the atom sets (head(ρc2 ) \ body+ (ρc2 ))θm and + −1 body (ρ̂1 )θn is non-empty, and (2.b) the database I2 does not satisfy ∃v. head(ρ̂1 )θn−1 ω∀ , and (2.c) none of the negative body atoms of ρ̂1 θn−1 are in I2 .

First, we derive (2.a): Recall that ℓC (c1 ) = ℓC (c2 ) means by Equation (4), that the pieces of orig(ρ̂n ), which are not contained in body+ (ρc1 ) under θn , are exactly the pieces of orig(ρ̂m ), which are not contained in body+ (ρc2 ) under θm . Also recall that head(ρc1 ) = head(orig(ρ̂n ))θn and head(ρc2 ) = head(orig(ρ̂m ))θm . −1 Therefore, (head(ρc1 ) \ body+ (ρc1 ))θn−1 = (head(ρc2 ) \ body+ (ρc2 ))θm . With this equality, (2.a) directly follows from (1.a). Next, we derive (2.b): Expanding Equation (5) at ℓS (c1 ) = ℓS (c2 ), we get that (body+ (ρc1 ) ∪ head(ρc1 ))ω |= ∃v. ψ̃(θn ω)∀ if and only if (body+ (ρc2 ) ∪ head(ρc2 ))ω |= ∃v. ψ̃(θm ω)∀ for all ∃v. ψ̃ ∈ F ⊆ parts(pieces(variants(R))). As θn and θm are both injective, we can apply their inverses to learn that I1 |= ∃v. ψ̃ω∀ if and only if I2 |= ∃v. ψ̃ω∀ . Using the forward direction of this equivalence, (2.b) follows from (1.b). The defining condition for ≡F is exactly this equivalence, so I1 ≡F I2 , which will later be needed to argue for (ii). Finally, we derive (2.c): By Equation (6), ℓN (c1 ) = ℓN (c2 ) says that a variant ρ̌ has a negative body atom falling into I1 under θn if and only if it has a negative body atom falling into I2 under θm . By (1.c), the variant orig(ρ̂1 ) = ρ̂1 θn−1 cannot be one of them, so (2.c) follows. Having (2.a)–(2.c), we conclude that c2 ρ̂2 is a chain. Note that c2 ρ̂2 might not be decoupled, if the variables from var(ρ̂1 ) \ var(head(ρ̂n )), which necessarily are fresh w.r.t. c1 , are not also S fresh w.r.t. c2 . If so, just take any injective mapping θ′ : stale(c2 ρ̂2 ) → V \ i∈{1,...,m} var(ρ̂i ), and c2 ρ̂2 θ′ is clearly decoupled. As θ′ acts only on the variables in ρ̂2 not shared with the head of c2 ’s final instance, ρc2 ≺ ≺+ ρ̂2 θ′ holds iff ρc2 ≺≺+ ρ̂2 (by an argument similar to the proof of Lemma 5), i.e. c2 ρ̂2 θ′ is a (decoupled) chain. To prove (ii), we first establish: Claim (‡). Let F be a formula set, such that parts(variants(F )) = F . Let I1 , I2 , and X be databases, such that (symbols(I1 ∪ I2 )) ∩ symbols(X) ⊆ symbols(F). Then I1 ≡F I2 implies that I1 ∪ X ≡F I2 ∪ X. Proof. Let databases I1 ≡F I2 , and X as well as formula set F be as in the claim. This means that I1 and I2 agree on satisfaction of formulae from F under ω∀ and that X uses only fresh symbols, except for symbols(F ). Let ∃v.ψ̃ be any formula from F. To prove the claim, we need to show that either both I1 ∪ X |= ∃v.ψ̃ω∀ and I2 ∪ X |= ∃v.ψ̃ω∀ or neither I1 ∪ X ̸|= ∃v.ψ̃ω∀ nor I2 ∪ X ̸|= ∃v.ψ̃ω∀ . In case that I1 |= ∃v.ψ̃ω∀ , then I2 must also satisfy it because of I1 ≡F I2 . As satisfaction for pieces is monotone, we directly get that I1 ∪ X |= ∃v.ψ̃ω∀ and I2 ∪ X |= ∃v.ψ̃ω∀ . Consider the case that I1 ̸|= ∃v.ψ̃ω∀ . By I1 ≡F I2 , we must also have I2 ̸|= ∃v.ψ̃ω∀ . Suppose that I2 ∪ X |= ∃v.ψ̃ω∀ . So there exists a mapping µ∃ : v → C ∪N such that ψ̃ω∀ µ∃ ⊆ I2 ∪X. It remains to show that I1 ∪X |= ∃v.ψ̃ω∀ .

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

27

The image of µ∃ can be separated into three disjoint sets A = symbols(F) and B = symbols(X) \ A and finally C = symbols(I2 ) \ A. Accordingly, we can ˙ B ∪v ˙ C where vS = {v ∈ v | µ∃ (v) ∈ S} for a split v into three disjoint sets vA ∪v set S. And finally, we can split µ∃ into three separate mappings µA ∃ : vA → A, C : A B C 8 : µB v → B, and µ v → C, such that µ = µ ◦ µ ◦ µ . B C ∃ ∃ ∃ ∃ ∃ ∃ As ψ̃ω∀ µ∃ ⊆ I2 ∪ X, we can write ψ̃ as the disjoint union of two sets ψ̃1 and ψ̃2 , such that ψ̃1 ω∀ µ∃ ⊆ I2 and ψ̃2 ω∀ µ∃ ⊆ X. Clearly, the image of existentials from the first set is µ∃ [var∃ (ψ̃1 )] ⊆ symbols(I2 ) = A ∪ C and the image of existentials from the second set is µ∃ [var∃ (ψ̃2 )] ⊆ symbols(X) = A ∪ B. So we C A B have ψ̃1 ω∀ µA ∃ µ∃ ⊆ I2 and ψ̃2 ω∀ µ∃ µ∃ ⊆ X. Let ρ̌ be a variant with ∃v. ψ̃ ∈ parts(ρ̌). Applying the variable mapping −1 : −1 (µA ) var(R) → var(R) yields the variant ρ̌(µA ). The pieces of the ∃ω ∃ω A −1 A −1 formula ∃vC . ψ̃1 (µ∃ ω ) are subformulae of ρ̌(µ∃ ω ) ∈ variants(F). Since each of them is satisfied by I2 (with µC ∃ ) they must also be satisfied by I1 , i.e. we ′ C′ : −1 must be able to find a µ∃ vC → symbols(I1 ), such that ψ̃1 (µA )ω∀ µC ∃ω ∃ = ′ ′ C A B C ψ̃1 ω∀ µA ⊔ ⊓ ∃ µ∃ ⊆ I1 . Thus, I1 ∪ X |= ∃v. ψ̃ω∀ with µ∃ µ∃ µ∃ . For (ii), we need to show that ℓ(c1 ρ̂1 ) = ℓ(c2 ρ̂2 ). We will show this for the three components of the label separately. Clearly, we have ℓC (c1 ρ̂1 ) = ℓC (c2 ρ̂2 ), because the final instances ρ̂1 and ρ̂2 both correspond to the same variant orig(ρ̂1 ). In (1.a) and (2.a) we thus identified the same non-empty intersection between the body of this variant and the heads of the chain rules minus their bodies. As noted, ℓS (c1 ) = ℓS (c2 ) gives I1 ≡F I2 . Since parts(variants(·)) is idempotent and the set F used for computing ℓS is parts(H) (or with RD -closure parts(H ∪ B)), and H and B are closed under variants(·), it fulfils the requirement of the claim ‡. The variables used universally in F are from var(R), i.e. X may share only symbols var(R)ω with the union of I1 and I2 . Note that symbols(I1 ∪ I2 ) = (symbols(I1 ) ∪ symbols(I2 )). The set of facts X = (body+ (orig(ρ̂1 ))∪head(orig(ρ̂1 )))ω meets the conditions for claim ‡, since the instance is decoupled w.r.t. both chains c1 and c2 . So we find that I1 ∪X ≡F I2 ∪X by (‡). This set X is exactly the set of facts that is added to the respective databases for computing ℓS (c1 ) and ℓS (c2 ). Lastly, we clearly have ℓN (c1 ρ̂1 ) = ℓN (c2 ρ̂2 ), as the fact set X which adds to the databases are again identical. ⊔ ⊓ Theorem 11. The language LR is regular. Claim (†). Let w1 , w2 ∈ LR be two words with the same final letter. For any v ∈ Σ ∗ , w1 v ∈ LR iff w2 v ∈ LR . 8

For a function f : A → B, we call f id : A ∪ B → A ∪ B with x 7→ f (x) for x ∈ A and x 7→ x for x ∈ B \ A the identity extension of f . Given two functions f : A1 → B and ˙ 2 → B for the composition g : A2 → B where A1 ∩ A2 = ∅, we write f ◦ g : A1 ∪A f id ◦ g id of their identify extensions.

28

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

Proof (by induction on |v|). For the induction base, the length of v is zero, i.e. v = ϵ (the empty word) and w2 v = w2 . By assumption w2 ∈ LR and so directly w2 v ∈ LR . The induction hypothesis (IH) is that for any word v ′ ∈ Σ ∗ and symbol c ∈ Σ, w1 v ′ ∈ LR ⇐⇒ w2 v ′ ∈ LR implies w1 v ′ c ∈ LR ⇐⇒ w2 v ′ c ∈ LR . For the induction step, let v = v ′ c for v ′ ∈ Σ ∗ and c ∈ Σ. If v ′ = ϵ, the final letter of w1 v ′ is the final letter of w1 and the final letter of w2 v ′ is the final letter of w2 , which are the same by assumption. Otherwise, the final letter of both w1 v ′ and w2 v ′ is the final letter of v ′ . Therefore, w1 v ′ and w2 v ′ have identical final letters in both cases and hence correspond to equi-labelled chains. Applying Lemma 10 finishes the induction. ⊔ ⊓ – For sets S and T , an equivalence relation ∼ over S distinguishes elements based on a predicate p : S → T , if x ∼ y iff p(x) = p(y) for all x, y ∈ S. – For a language L ⊆ Σ ∗ , the extensions of a word w ∈ L is the set of all v ∈ Σ ∗ for which wv ∈ L. – By 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. Proof (of Theorem 11). We define an equivalence relation over words in the language LR based on their final letters ∼LR := {⟨w(c1 ), w(c2 )⟩ | c1 , c2 ∈ chains(R), ℓ(c1 ) = ℓ(c2 )}.

(14)

Clearly, ∼LR has at most |Σ|-many equivalence classes, which is finitely many as the alphabet is finite. By (†), two words from LR that share the same label (= ˆ final letter), i.e. are ∼LR -equivalent, have the same extensions. Hence, ∼LR ∪(Σ ∗ \LR )2 meets the conditions of Myhill-Nerode, which makes LR a regular language. ⊔ ⊓ Claim. For c1 , c2 ∈ chains(R) with ℓ(c1 ) = ℓ(c2 ), we have ρc1 ≺□ ρ iff ρc2 ≺□ ρ and ρc1 ≺− ρ iff ρc2 ≺− ρ. Proof. To compute ρci ≺□ ρ (see Definition 5) and ρci ≺− ρ (see Definition 4) for i ∈ {1, 2}, it suffices to examine unifiable subsets of head(ρ) or body− (ρ) with head(ρci ) (c.f. efficient algorithms of [9]). Remaining checks concern the satisfaction of the heads of the involved rules on representative databases. Let ρ̂ni be the final instances in ci , with unique θni , such that ρ̂ni = orig(ρ̂ni )θni . Again, we can equivalently test for ρci θn−1 ≺□ ρθn−1 and ρci θn−1 ≺− ρθn−1 (as θni is i i i i + −1 revertible and θni is injective). These will involve (body (ρci ) ∪ head(ρci ))θn−1 ω, i and we stated before that these are ≡F -equivalent due to ℓS (c1 ) = ℓS (c2 ) (see proof of Lemma 10 (i)) and satisfy the same rule heads. ⊔ ⊓

Stratified Negation in RDF Rules: A Correct Approach (Extended Version)

E

29

Details on Introductory Example

We will now revisit the introductory examples (cf. Section 1, Problems 1 and 2). Here, we refer to the N3 rule in line i by ρi . Figure 1 depicts a graphical representation of the reliance relations between these rules. Evidently, this yields an acyclic graph for L8–L11 on the right, which means that RP2 = {ρ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. RP1 = {ρ1 , ρ2 , ρ3 , ρ4 } and R′P1 = RP1 ∪ {ρ5 , ρ6 , ρ7 } are not fully stratified. Below, we will examine RP1 and R′P1 in detail, to see that — while neither is chain-stratified either (see Example 15) — R′P1 is chain-stratified under constraints (as defined in Section 7).

ρ1

ρ3

ρ5 ρ6

≺− ρ2

ρ4

ρ7

ρ8 ≺□ ρ9

ρ10 ≺− ρ11

≺− Figure 1. Reliance graph of L1–L7 (left) and L8–L11 (right); dashed lines are ≺+

Let us first rewrite L1–L7 in more compact syntax and using fewer variables. ρ1 : ρ2 :

t(?x, pa, ?y) → t(?y, ty, St)

ρ3 : ρ4 :

t(?p, spo, ?y), t(?y, spo, ?q) → t(?p, spo, ?q)

t(?x, te, ?y), ¬t(?y, ty, St) → t(?x, ex, ?y) t(?p, spo, ?q), t(?x, ?p, ?y) → t(?x, ?q, ?y)

ρ5 : ρ6 :

t(ex, spo, pa) → ⊥

ρ7 :

t(ex, spo, ty) → ⊥

t(ex, spo, spo) → ⊥

There 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 1 will consider the following chains in the given order: ρ2 , ρ4 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ) → t(?x, ?q1 , ?y) • chain accepted • ≺− ρ2 rejected because it would require ?q1 7→ ty, ?y 7→ St, violating constraint ρ7 ρ2 , ρ4 , ρ1 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, pa), t(?x, pa, ?y) → t(?y, ty, St) • chain rejected because of constraint ρ5 ρ2 , ρ4 , ρ2 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, te), t(?x, te, ?y) → t(?x, ex, ?y) • chain rejected because the head is already entailed

30

N. Küchenmeister, A. Ivliev, D. Arndt, M. Krötzsch

ρ2 , ρ4 , ρ3 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, spo), t(?x, spo, ?y), t(?y, spo, ?z) → t(?x, spo, ?z) • chain rejected because of constraint ρ6 ρ2 , ρ4 , ρ4 : [?p/?q1 , ?q/?q2 ] : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, ?q2 ) → t(?x, ?q2 , ?y) • chain accepted • ≺− ρ2 rejected because it would require ?q2 7→ ty, ?y 7→ St, such that ρ3 derives t(ex, spo, ty), violating constraint ρ7 [?q1 /spo, ?p/?x, ?q/?y] : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, spo), t(?x, spo, ?y), t(?x1 , ?x, ?y1 ) → t(?x1 , ?y, ?y1 ) • chain rejected because of constraint ρ6 ρ2 , ρ4 , ρ4 , ρ1 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, pa), t(?x, pa, ?y) → t(?y, ty, St) • chain rejected because ρ3 derives t(ex, spo, pa), violating constraint ρ5 ρ2 , ρ4 , ρ4 , ρ2 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, te), t(?x, te, ?y) → t(?x, ex, ?y) • chain rejected because the head is already entailed ρ2 , ρ4 , ρ4 , ρ3 : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, spo), t(?x, spo, ?y), t(?y, spo, ?z) → t(?x, spo, ?z) • chain rejected because ρ3 derives t(ex, spo, spo), violating constraint ρ6 ρ2 , ρ 4 , ρ 4 , ρ 4 : [?p/?q2 , ?q/?q3 ] : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, ?q2 ), t(?x, ?q2 , ?y), t(?q2 , spo, ?q3 ) → t(?x, ?q3 , ?y) • chain accepted (...but continuing like this will repeat label) • ≺− ρ2 rejected because it would require ?q3 7→ ty, ?y 7→ St, such that two ρ3 applications derive t(ex, spo, ty), violating constraint ρ7 [?q2 /spo, ?p/?x, ?q/?y] : t(?x, te, ?y), t(?x, ex, ?y), t(ex, spo, ?q1 ), t(?x, ?q1 , ?y), t(?q1 , spo, spo), t(?x, spo, ?y), t(?x1 , ?x, ?y1 ) → t(?x1 , ?y, ?y1 ) • chain rejected because ρ3 derives t(ex, spo, spo), violating constraint ρ6

None of these passed the conditions in A14 or A16 of the algorithm, so no new edges were added to ≺. Therefore, A6 will not find cycles and A17 is reached, concluding that R′P1 indeed is chain-stratified under constraints.