# Answering Queries with Negation over Existential Rules††thanks: This paper
is the technical report for the paper with the same title appearing at the
36th AAAI Conference on Artificial Intelligence (AAAI 2022).

Stefan Ellmauthaler, Markus Krötzsch, Stephan Mennicke

###### Abstract

Ontology-based query answering with existential rules is well understood and
implemented for positive queries, in particular conjunctive queries. For
queries with negation, however, there is no agreed-upon semantics or standard
implementation. This problem is unknown for simpler rule languages, such as
Datalog, where it is intuitive and practical to evaluate negative queries over
the least model. This fails for existential rules, which instead of a single
least model have multiple _universal models_ that may not lead to the same
results for negative queries. We therefore propose _universal core models_ as
a basis for a meaningful (non-monotonic) semantics for queries with negation.
Since cores are hard to compute, we identify syntactic conditions (on rules
and queries) under which our core-based semantics can equivalently be obtained
for other universal models, such as those produced by practical chase
algorithms. Finally, we use our findings to propose a semantics for a broad
class of existential rules with negation.

## Introduction

Existential rules are a prominent approach in knowledge representation, due to
theoretical and practical advances in ontology-based query answering (Baget et
al. 2009; Calì, Gottlob, and Lukasiewicz 2009), but also because of
applications in many other domains, such as data exchange and integration
(Fagin et al. 2005). Answering conjunctive queries (CQs) over sets of
existential rules is often the main goal, where a CQ is entailed if it is
satisfied by all models of the given rules. This is often implemented using
_universal models_ , which is a class of models each representing all positive
query answers, such that one such model suffices to answer CQs (Deutsch, Nash,
and Remmel 2008).

However, for queries that ask for the absence of facts (i.e., queries
incorporating negated atoms), universal models cannot be used because
different universal models may yield different query answers. This is a major
problem, since negation is an important feature in real-world queries, and a
semantic prerequisite for supporting negation in rule bodies, which can be
viewed as a recursive generalisation of negative queries. The severity of this
limitation is further aggravated by the fact that no such problems exist for
Datalog, where negative queries can safely be evaluated over the unique least
model. This can be further generalised by considering _stratified negation_ in
rule bodies, which yields an intuitive and implementable non-monotonic
semantics (Abiteboul, Hull, and Vianu 1994). But even this basic form of
negation is not safe to use with existential rules.

What makes this problem challenging is that we are looking for a non-monotonic
form of negation, where the absence of positive evidence is sufficient to
entail negative information. Indeed, under the classical first-order semantics
of negation, no negated queries are ever entailed by a set of existential
rules. However, it is not immediate when a non-monotonic semantics should
allow for additional, non-classical consequences, and several distinct
approaches have been proposed for existential rules (Magka, Krötzsch, and
Horrocks 2013; Baget et al. 2014; Gottlob et al. 2014; Alviano, Morak, and
Pieris 2017; Krötzsch 2020). Our goal for this paper is to provide a semantics
that agrees with the widely used and generally accepted semantics of Datalog
with stratified negation for rules without existentials, but which also
respects the classical reading of existential quantifiers as mere statements
of existence of certain elements without any commitment to their identity (in
contrast to logic programming approaches that use function terms for referring
to distinguished objects).

We therefore propose to evaluate negations with respect to universal models
that are _cores_ , an algebraic property that, intuitively speaking, ensures
that they contain no redundant structures. Many good practical and theoretical
results have been obtained for core models (Fagin, Kolaitis, and Popa 2005;
Deutsch, Nash, and Remmel 2008; Carral et al. 2018; Krötzsch 2020), but
computing cores from arbitrary structures is expensive (Hell and Nešetřil
1992).

CoreModels$\sqsubseteq$RestrictedChases$\subseteq$Chases$\subseteq$UniversalModelsBNCQThm.
1$\supseteq$(Effectively)Core-Safe BNCQThm. 3 (Thm. 4)$\supseteq$Affection-
SafeBNCQThm. 2$\supseteq$BCQ

Figure 1: Summary of Results

We therefore ask if our core-based semantics for negation can also be computed
using other kinds of universal models, which are easier to compute in
practice. It turns out that this is possible if we restrict the shape of the
queries that we want to answer, and we define several classes of “safe”
queries that can be evaluated over broader classes of models. Our results are
summarised in Figure 1, which illustrates the inverse relationship between the
generality of the query language and the specificity of the models that one
can use to compute them. The (restricted) _chase_ refers to a widely
implemented type of reasoning algorithm, such that the respective query
classes could be evaluated in practice (Nenov et al. 2015; Benedikt et al.
2017; Bellomarini, Sallinger, and Gottlob 2018; Carral et al. 2019). The
symbol $\sqsubseteq$ expresses that core models can be embedded into every
restricted chase, although no such chase is necessarily equal to the core
(hence no $\subseteq$). For any of the given query fragments, we provide
concrete syntactic definitions that can be decided in practice.

Our final contribution is the extension of our approach to existential rules
with negations in their bodies. This is technically more challenging than mere
query answering, and even the eager computation of cores during reasoning
cannot guarantee a unique semantics (Krötzsch 2020). We focus on cases where
rules can be stratified in a certain sense, but our conditions significantly
generalise classical stratification (Abiteboul, Hull, and Vianu 1994) and the
recent _full stratification_ for existential rules (Krötzsch 2020).
Nevertheless, we can still find a unique “perfect” model that can be used in
query answering, making our approach a valid generalisation of the _perfect
core model semantics_ (Krötzsch 2020).

## Preliminaries

We consider a first-order signature with disjoint sets of _constants_
$\mathbf{C}$, _(labelled) nulls_ $\mathbf{N}$, _variables_ $\mathbf{V}$, and
_predicates_ $\mathbf{P}$. A _term_ $t$ is an element of
$\mathbf{C}\cup\mathbf{N}\cup\mathbf{V}$. Lists of terms are denoted
$\boldsymbol{t}=t_{1},t_{2},\ldots,t_{n}$ with $n=|\boldsymbol{t}|$, and
treated as sets when order is irrelevant. Each predicate $p\in\mathbf{P}$ has
an _arity_ $\text{{\sf ar}}(p)\in\mathbb{N}$. An _atom_ is an expression
$p(\boldsymbol{t})$ with $p\in\mathbf{P}$ and $\text{{\sf
ar}}(p)=|\boldsymbol{t}|$. An atom $p(\boldsymbol{t})$ is _ground_ if
$\boldsymbol{t}\subseteq\mathbf{C}$. An _interpretation_ $\mathcal{I}$ is a
set of atoms without variables. A database $\mathcal{D}$ is a finite set of
ground atoms.

#### Rules and Queries

An _(existential) rule_ $r$ is a formula

$\displaystyle r=\forall\boldsymbol{x},\boldsymbol{y}.\
\varphi[\boldsymbol{x},\boldsymbol{y}]\to\exists\boldsymbol{z}.\
\psi[\boldsymbol{y},\boldsymbol{z}],$ (1)

where $\varphi$ and $\psi$ are conjunctions of atoms using only terms from
$\mathbf{C}$ or from the mutually disjoint lists of variables
$\boldsymbol{x},\boldsymbol{y},\boldsymbol{z}\subseteq\mathbf{V}$. We call
$\varphi$ the _body_ (denoted $\text{{\sf body}}(r)$), $\psi$ the _head_
(denoted $\text{{\sf head}}(r)$), and $\boldsymbol{y}$ the _frontier_ of $r$.
For ease of notation we may treat conjunctions of atoms as sets, and we omit
universal quantifiers in rules. We require that all variables in
$\boldsymbol{y}$ actually occur in $\varphi$ (_safety_).111This requirement
can be relaxed, but it simplifies presentation. A rule is _Datalog_ if it has
no existential quantifiers.

A _normal Boolean conjunctive query_ (BNCQ) is a formula
$q=\exists\boldsymbol{x}.\varphi\wedge\psi$, where $\varphi$ is a conjunction
of atoms with variables from $\boldsymbol{x}$, and $\psi$ is a conjunction of
negated atoms $\text{{\bf not}\,}p(\boldsymbol{t})$ using only variables that
occur in $\varphi$ (_safety_). We write $q^{+}$ ($q^{-}$) for the set of all
non-negated atoms in $\varphi$ ($\psi$). If $q^{-}=\emptyset$, then $q$ is a
_boolean conjunctive query_ (BCQ).

#### Models and Entailment

Given a set of atoms $\mathcal{A}$ and an interpretation $\mathcal{I}$, a
_homomorphism_ $h:\mathcal{A}\to\mathcal{I}$ is a function that maps the terms
occurring in $\mathcal{A}$ to (the variable-free) terms occurring in
$\mathcal{I}$, such that: (i) for all $c\in\mathbf{C}$, $h(c)=c$; (ii) for all
$p\in\mathbf{P}$, $p(\boldsymbol{t})\in\mathcal{A}$ only if
$p(h(\boldsymbol{t}))\in\mathcal{I}$, where $h(\boldsymbol{t})$ is the list of
$h$-images of the terms $\boldsymbol{t}$. If $h$ satisfies (ii) with “only if”
strengthened to “iff”, $h$ is a _strong homomorphism_. An _embedding_ is an
injective strong homomorphism, and an _isomorphism_ is a bijective strong
homomorphism (i.e., surjective embedding). We apply homomorphisms to a formula
by applying them individually to all of its atoms.

A _match_ of a rule $r$ in an interpretation $\mathcal{I}$ is a homomorphism
$h:\text{{\sf body}}(r)\to\mathcal{I}$. A match $h$ of $r$ in $\mathcal{I}$ is
_satisfied_ if there is a homomorphism $h^{\prime}:\text{{\sf
head}}(r)\to\mathcal{I}$, such that $h\subseteq h^{\prime}$. We call
$h^{\prime}$ an _extension of $h$_. Rule $r$ is _satisfied_ by $\mathcal{I}$,
written $\mathcal{I}\models r$, if every match of $r$ in $\mathcal{I}$ is
satisfied. A set of rules $\Sigma$ is satisfied by $\mathcal{I}$, written
$\mathcal{I}\models\Sigma$, if $\mathcal{I}\models r$ for all $r\in\Sigma$. We
call $\mathcal{I}$ a _model_ of $\Sigma$ and database $\mathcal{D}$ if
$\mathcal{I}\models\Sigma$ and $\mathcal{D}\subseteq\mathcal{I}$. A BNCQ $q$
is _satisfied_ by $\mathcal{I}$, written $\mathcal{I}\models q$, if there is a
homomorphism $h:q^{+}\to\mathcal{I}$ with $h(q^{-})\cap\mathcal{I}=\emptyset$.
Note, a BNCQ $q$ with $q^{+}\cap q^{-}\neq\emptyset$ can never be satisfied.
Herein we consider only BNCQs $q$ that are _non-trivial_ in this sense.

#### Universal Models and the Chase

A model $\mathcal{U}$ of $\mathcal{D}$ and $\Sigma$ is _universal_ if there is
a homomorphism $\mathcal{U}\to\mathcal{M}$ for every model $\mathcal{M}$ of
$\mathcal{D}$ and $\Sigma$. Universal models can be computed with _the chase_
(Deutsch, Nash, and Remmel 2008). In this paper, we will mainly deal with the
_restricted chase_ (also known as _standard chase_).

######  Definition 1.

Let $\mathcal{D}$ be a database and $\Sigma$ a set of rules. A sequence
$\mathcal{D}^{0},\mathcal{D}^{1},\ldots$ is called a _(restricted) chase
sequence of $\mathcal{D}$ and $\Sigma$_ iff

  1. 1.

$\mathcal{D}^{0}=\mathcal{D}$,

  2. 2.

for every $\mathcal{D}^{i+1}$ ($i\geq 0$) there is a rule $r\in\Sigma$ of the
form (1) and a match $h$ for $r$ in $\mathcal{D}^{i}$ with

    1. (a)

$h$ is an unsatisfied match for $r$ in $\mathcal{D}^{i}$ and

    2. (b)

there is an extension $h^{\star}:\text{{\sf head}}(r)\to\mathcal{D}^{i+1}$ of
$h$, such that $h^{\star}(z)$ is a fresh null for each $z\in\boldsymbol{z}$,
and

  3. 3.

if $h$ is a match for some rule $r\in\Sigma$ in $\mathcal{D}^{i}$ ($i\geq 0$),
then $h$ is satisfied in some $\mathcal{D}^{j}$ with $j\geq i$ (fairness).

$r$ is _applicable in $\mathcal{D}^{i}$_ if it has an unsatisfied match in
$\mathcal{D}^{i}$. Chase sequence
$\mathcal{D}^{0},\mathcal{D}^{1},\ldots,\mathcal{D}^{k}$ is called
_terminating_ if $\mathcal{D}^{k}$ is a model of $\Sigma$ and $\mathcal{D}$.
We call $\mathcal{D}^{\infty}:=\bigcup_{i\geq 0}\mathcal{D}^{i}$ a _chase of
$\Sigma$ and $\mathcal{D}$_.

Other chase variants, like the Skolem/semi-oblivious or the oblivious chase,
mainly differ in the respective definitions of rule applicability (2. (a) in
Definition 1).

#### Influence of Existential Quantifiers

For some of the upcoming notions, it is useful to have rule sets $\Sigma$
where each rule makes use of a distinct set of variables than all the other
rules. We say that $\Sigma$ is _renamed-apart_. Every rule set can be
rewritten to an equivalent renamed-apart rule set.

The _positions_ in a predicate $p\in\mathbf{P}$ are the pairs
$\langle{p,1}\rangle,\ldots,\langle{p,\text{{\sf ar}}(p)}\rangle$, and we will
refer to terms _at_ a certain position in an atom, set of atoms, or other
formula. $\text{{\sf Var}}(X)$ ($\text{{\sf Var}}_{\exists}(X)$/$\text{{\sf
Var}}_{\forall}(X)$) denotes the set of all (existentially
quantified/universally quantified) variables in a rule or rule set $X$. We
reproduce the following definition from Krötzsch and Rudolph (2011) to obtain
a structure allowing for syntactic reasoning of the influence of existential
quantifiers within the chase.

######  Definition 2.

Let $\Sigma$ be a renamed-apart rule set. For $x\in\text{{\sf Var}}(\Sigma)$,
let $\Pi^{B}_{x}$ ($\Pi^{H}_{x}$) be the sets of all positions at which $x$
occurs in the body (head) of a (necessarily unique) rule in $\Sigma$. If
$x\in\text{{\sf Var}}_{\exists}(\Sigma)$, then $\Omega_{x}$ is the smallest
set of positions such that (1) $\Pi^{H}_{x}\subseteq\Omega_{x}$ and (2) for
all $y\in\text{{\sf Var}}_{\forall}(\Sigma)$, $\Pi^{B}_{y}\subseteq\Omega_{x}$
implies $\Pi^{H}_{y}\subseteq\Omega_{x}$. The set of _jointly affected_
positions is $\bigcup_{x\in\text{{\sf Var}}_{\exists}(\Sigma)}\Omega_{x}$. For
$x,y\in\text{{\sf Var}}_{\exists}(\Sigma)$, we write $x\leadsto y$ if the
(unique) rule of $y$ has a frontier variable $z$ with
$\Pi^{B}_{z}\subseteq\Omega_{x}$.

The relation $x\leadsto y$ states that nulls created for $x$ potentially
enable rule applications that create nulls for $y$. Of particular interest is
the transitive and reflexive closure $\leadsto^{*}$. Starting from a set of
existentially quantified variables, we seek all positions at which a null
might occur that is directly or indirectly influenced by a variable in this
set.

######  Definition 3.

Let $\Sigma$ be a renamed-apart rule set and let $V\subseteq\text{{\sf
Var}}_{\exists}(\Sigma)$. A position $\pi$ is _$V$ -influenced_ if there are
$x\in V$ and $y$ with $x\leadsto^{*}y$ such that $\pi\in\Omega_{y}$.

Note that _jointly affected_ is the same as $\text{{\sf
Var}}_{\exists}(\Sigma)$-influenced. Virtually any chase variant (restricted,
Skolem, and oblivious) is _compatible_ with jointly affected positions,
meaning that nulls in chases $\mathcal{D}^{\infty}$ only occur in $\text{{\sf
Var}}_{\exists}(\Sigma)$-influenced positions.

######  Proposition 1.

For renamed-apart rule set $\Sigma$ and database $\mathcal{D}$ with
(Skolem/oblivious/restricted) chase $\mathcal{D}^{\infty}$, if
$p(t_{1},\ldots,t_{\text{{\sf ar}}(p)})\in\mathcal{D}^{\infty}$ and
$t_{i}\in\mathbf{N}$ ($1\leq i\leq\text{{\sf ar}}(p)$), then
$\langle{p,i}\rangle$ is $\text{{\sf Var}}_{\exists}(\Sigma)$-influenced.

###### Proof.

We prove the claim for a slight adaptation of the restricted chase, removing
condition 2. (a) from Definition 1 to obtain the required generality. In fact,
the resulting chase procedure is an upper bound for all the chase variants.
Let $\mathcal{D}^{\infty}$ be such a chase with
$p(t_{1},\ldots,t_{n})\in\mathcal{D}^{\infty}$ and $t_{i}\in\mathbf{N}$
($1\leq i\leq n$). Then $p(t_{1},\ldots,t_{n})$ must have been introduced at
some chase step $\mathcal{D}^{k}$ by rule $r_{k}\in\Sigma$ with
$p(u_{1},\ldots,u_{n})\in\text{{\sf head}}(r)$ and match $h_{k}$
($h_{k}^{\star}(u_{i})=t_{i}$). Furthermore, $t_{i}$ must have been introduced
at some chase step $\mathcal{D}^{k_{0}}$ ($k_{0}\leq k$) by some rule $r_{0}$
with existential variable $z\in\text{{\sf Var}}_{\exists}(r_{0})$ at position
$\langle{q,j}\rangle$, and match $h_{0}$ with $h_{0}^{\star}(z)=t_{i}$. Since
$t_{i}$ eventually occurs at position $\langle{p,i}\rangle$, $k-k_{0}$ is an
upper bound for the number of rules different from $r$ to have carried $t_{i}$
from $\mathcal{D}^{k_{0}}$ to $\mathcal{D}^{k}$. If $k=k_{0}$, then $r_{0}=r$
and $u_{i}=z$. By $z\leadsto^{*}z$ and $\langle{p,i}\rangle\in\Omega_{z}$ it
follows that $\langle{p,i}\rangle$ is $\text{{\sf
Var}}_{\exists}(\Sigma)$-influenced. If $k>k_{0}$, then there is a maximal set
of atoms
$\\{r_{1}(\boldsymbol{v_{1}}),\ldots,r_{m}(\boldsymbol{v_{m}})\\}\subseteq\text{{\sf
body}}(r)$ with $u_{i}$ occurring at positions in
$\\{\langle{r_{1},j_{1}}\rangle,\ldots,\langle{r_{m},j_{m}}\rangle\\}=\Pi_{u_{i}}^{B}$.
By an inductive argument, it holds that $\Pi_{u_{i}}^{B}\subseteq\Omega_{z}$,
which implies that $\Pi_{u_{i}}^{H}\subseteq\Omega_{z}$. Finally,
$\langle{p,i}\rangle\in\Pi_{u_{i}}^{H}\subseteq\Omega_{z}$ and, therefore,
$\langle{p,i}\rangle$ is jointly affected. Thus, $\langle{p,i}\rangle$ is
$\text{{\sf Var}}_{\exists}(\Sigma)$-influenced. ∎

## Answering BNCQs on Core Models

A BCQ is entailed by rule set $\Sigma$ and database $\mathcal{D}$ if it is
satisfied by all models of $\Sigma$ and $\mathcal{D}$. Moreover, every
universal model of $\Sigma$ and $\mathcal{D}$ satisfies exactly the BCQs that
are entailed in this sense. Neither condition is appropriate to define
entailment of BNCQs that may use negation. On the one hand, no such query is
satisfied in all models since there is always a model where every BCQ is true.
On the other hand, different universal models do not satisfy the same BNCQs.

######  Example 1.

Take for instance the database $\mathcal{D}=\\{a(1,2),b(2,2)\\}$ together with
an empty rule set. Of course, $\mathcal{D}$ is a universal model, but so is
$\mathcal{U}:=\mathcal{D}\cup\\{a(1,n)\\}$ (where $n\in\mathbf{N}$). As
mentioned above, all BCQs evaluate with the same result on $\mathcal{D}$ or
$\mathcal{U}$. However, for BNCQ $q=\exists x,y.\ a(x,y)\wedge\neg b(y,y)$ we
get $\mathcal{U}\models q$ while $\mathcal{D}\not\models q$.

Models that are _cores_ have been suggested as the appropriate model for
defining the semantics of queries that may depend on negative information
(Deutsch, Nash, and Remmel 2008; Baget et al. 2014). This suggestion is
substantiated by the fact that cores are unique up to isomorphism and that
isomorphic structures cannot be distinguished by first-order (FO) queries
(see, e.g., the _Isomorphism Lemma_ by Ebbinghaus, Flum, and Thomas (1994)).
Indeed, if a universal model is a core, then it satisfies fewer BNCQs than any
other model (see also Theorem 1 below), resulting in the most “cautious”
notion of non-monotonic entailment.

######  Definition 4.

A finite interpretation $\mathcal{I}$ is a _core_ if every homomorphism
$h:\mathcal{I}\to\mathcal{I}$ is an isomorphism. A _core model_ of a rule set
$\Sigma$ and a database $\mathcal{D}$ is a finite universal model of $\Sigma$
and $\mathcal{D}$ that is a core.

If $\Sigma$ and $\mathcal{D}$ have any finite universal model, then they admit
a finite core, which is unique up to isomorphism (Deutsch, Nash, and Remmel
2008). The situation is more complicated on infinite structures, which admit
several non-equivalent definitions of core (Bauslaugh 1995) and where core
models might fail to exist altogether (Carral et al. 2018). We therefore focus
on cases with finite models $\mathcal{M}$ and their unique cores, which we
denote $\mathsf{core}(\mathcal{M})$. Many conditions have been studied to
recognise cases where finite universal models are guaranteed to exist (Cuenca
Grau et al. 2013). In the rest of the paper we study the notion of _core
entailments_ for BNCQs, being those entailments we obtain when evaluating the
query on _the_ core model.

######  Definition 5.

A rule set $\Sigma$ and database $\mathcal{D}$ _core-entail_ a BNCQ $q$,
written $\Sigma,\mathcal{D}\models_{c}q$, if $\Sigma$ and $\mathcal{D}$ have a
core model $\mathcal{C}$ satisfying $q$.

#### Important Assumption

Throughout this paper, we only consider pairs of rule sets $\Sigma$ and
databases $\mathcal{D}$ that have a (finite) core model. Definition 5 does not
apply to other cases.

Again considering Example 1, $\mathcal{D}$ is not just any universal model,
but the core model. Hence, $\Sigma,\mathcal{D}\not\models_{c}q$ for the query
$q$ in the example, as one might intuitively expect. As shown in Example 1,
such non-entailments are not preserved in arbitrary (universal) models, but it
turns out that entailments are. This is a consequence of the fact that core
models are embedded in all universal models in the following sense.

######  Lemma 1.

Let $\Sigma$ be a rule set and $\mathcal{D}$ a database with core model
$\mathcal{C}$ and arbitrary universal model $\mathcal{U}$. (1) If
$h:\mathcal{C}\to\mathcal{U}$ is a homomorphism, it is an embedding. We call
$h(\mathcal{C})$ the _core instance of $\mathcal{U}$_ and denote it by
$\mathcal{U}_{c}$. (2) Every homomorphism
$h:\mathcal{U}_{c}\to\mathcal{U}_{c}$ is an isomorphism.

###### Proof.

On (1), since $\mathcal{U}$ is a universal model and $\mathcal{C}$ a (core)
model of $\Sigma$ and $\mathcal{D}$, there is a homomorphism
$h^{\prime}:\mathcal{U}\to\mathcal{C}$. Note, $h^{\prime}\circ
h:\mathcal{C}\to\mathcal{C}$ is an isomorphism as $\mathcal{C}$ is a core. We
show that $h$ is an embedding, i.e., $h$ is injective and strong. For
injectivity, let $u$ and $t$ be distinct terms occurring in $\mathcal{C}$. If
$h(u)=h(t)$, it follows that $h^{\prime}\circ h(u)=h^{\prime}\circ h(t)$,
which contradicts the assumption that $h^{\prime}\circ h$ is an isomorphism.
For showing that $h$ is strong, let $\boldsymbol{u}$ be a list of terms in
$\mathcal{C}$ and $p(h(\boldsymbol{u}))\in\mathcal{U}$. We need to show that
$p(\boldsymbol{u})\in\mathcal{C}$. As $h^{\prime}\circ h$ is an isomorphism on
$\mathcal{C}$, its inverse is also an isomorphism. Hence, $p(h^{\prime}\circ
h(\boldsymbol{u}))\in\mathcal{C}$ and $p((h^{\prime}\circ
h)^{-1}\circ(h^{\prime}\circ h)(\boldsymbol{u}))\in\mathcal{C}$ allow for the
conclusion $p(\boldsymbol{u})\in\mathcal{C}$.

Towards (2), there is an isomorphism $i:\mathcal{C}\to\mathcal{U}_{c}$ by the
argumentation above. Let $h:\mathcal{U}_{c}\to\mathcal{U}_{c}$ be a
homomorphism. Define $j:=i^{-1}\circ(h\circ i)$ (i.e.,
$j:\mathcal{C}\to\mathcal{C}$). Since $\mathcal{C}$ is a core, $j$ is an
isomorphism. Hence, $h$ must be an isomorphism. ∎

Based on the core instance, we can now show that core entailments of BNCQs
carry over to all universal models.

######  Theorem 1.

For every rule set $\Sigma$, database $\mathcal{D}$, and BNCQ $q$, if
$\Sigma,\mathcal{D}\models_{c}q$, then $\mathcal{U}\models q$ for all
universal models $\mathcal{U}$ of $\Sigma$ and $\mathcal{D}$.

###### Proof.

Let $\mathcal{C}$ be a core model of $\Sigma$ and $\mathcal{D}$. The core
instance $\mathcal{U}_{c}\subseteq\mathcal{U}$ preserves all FO-queries,
including BNCQs. We conclude that for all BNCQ $q$, $\mathcal{C}\models q$
implies $\mathcal{U}\models q$. ∎

In fact, up to minor variations, the core model is the only model with this
property: the only other models for which BNCQ satisfaction is preserved in
all universal models are those that can be embedded into the core model.
However, it turns out that _some_ BNCQs allow us to consider broader classes
of models for checking core entailment, as we will see in the following
sections.

## Affection-Safe BNCQs

In spite of its appealing semantics, core entailment has the practical
disadvantage that core models are difficult to compute. This difficulty seems
unavoidable if we want minimality in the sense of Theorem 1. However, this
does not mean that core entailment of BNCQs does always require us to compute
the core model. For example, BNCQs without negation can equivalently be
answered in any universal model. We show that similar results can also be
obtained for more interesting classes of BNCQs, and how these classes can be
effectively recognised.

This requires us to look at more specific classes of models. Indeed, we can
readily see that entailment over _all_ universal models does often not
coincide with core entailment since core-non-entailments are not preserved
across universal models: every BNCQ $q$ whose positive part is entailed is
also true in some universal model, unless its negative part is a logical
consequence (in this case, the non-entailment of $q$ is a first-order logical
consequence). This can be shown by adding redundant structures where $q$ is
satisfied, as in Example 1, but taking arbitrary rule sets into account.

######  Proposition 2.

Consider a rule set $\Sigma$ and database $\mathcal{D}$. For every BNCQ $q$
such that (a) $\Sigma,\mathcal{D}\models{q}^{+}$ and (b)
$\Sigma,\mathcal{D}\not\models{q}^{+}\wedge a(\boldsymbol{t})$ for all
$a(\boldsymbol{t})\in{q}^{-}$, there is a universal model $\mathcal{U}$ of
$\Sigma$ and $\mathcal{D}$ with $\mathcal{U}\models q$.

###### Proof.

Define $\mathcal{D}^{+}:=\mathcal{D}\cup\\{p(\nu(\boldsymbol{u}))\mid
p(\boldsymbol{u})\in{q}^{+}\\}$ with $\nu(t)=t$ for all $t\in\mathbf{C}$ and
$\nu(t)$ a fresh null for all $t\in\mathbf{V}$. Now let $\mathcal{U}$ be a
chase over $\Sigma$ and $\mathcal{D}^{+}$ (e.g., some restricted chase). By
construction, $\mathcal{U}$ is a model of $\Sigma$ and $\mathcal{D}$, and
$\nu$ is a match $\nu:{q}^{+}\to\mathcal{U}$. By safety, $\nu$ is defined for
$\text{{\sf Var}}({q}^{-})$.

Now for any $\alpha=a(\boldsymbol{t})\in{q}^{-}$, let $\mathcal{U}_{\alpha}$
be a universal model of $\Sigma$ and $\mathcal{D}$ such that
$\mathcal{U}_{\alpha}\not\models{q}^{+}\wedge\alpha$, which exists due to (b).
Due to (a), there is a match $\nu^{\prime}:{q}^{+}\to\mathcal{U}_{\alpha}$
such that $\nu^{\prime}(\alpha)\notin\mathcal{U}_{\alpha}$ (using (b)). Since,
moreover, $\mathcal{D}\subseteq\mathcal{U}_{\alpha}$, we find that there is a
homomorphism $h:\mathcal{D}^{+}\to\nu^{\prime}({q}^{+})\cup\mathcal{D}$. By
soundness of the chase, $h$ extends to a homomorphism
$h^{\prime}:\mathcal{U}\to\mathcal{U}_{\alpha}$. Since $\mathcal{U}_{\alpha}$
is universal, this shows that $\mathcal{U}$ is universal. By construction,
$h^{\prime}(\nu(\alpha))=\nu^{\prime}(\alpha)\notin\mathcal{U}_{\alpha}$, and
hence $\nu(\alpha)\notin\mathcal{U}$. Applying the same reasoning to all
$\alpha\in{q}^{-}$, we find that $\nu$ shows $\mathcal{U}\models q$. ∎

Hence, only limited classes of BNCQs can be evaluated over arbitrary universal
models. This, however, is due to some universal models containing unmotivated
clutter that users might intuitively not expect. In particular, the universal
models that are computed by chase procedures are not of this form, and can
only produce nulls in jointly affected positions (Proposition 1). Therefore,
if all variables in ${q}^{-}$ are bound to some position in ${q}^{+}$ that is
not jointly affected, then these variables can only match constants.

######  Definition 6.

Let $\Sigma$ be a rule set. A BNCQ $q$ is _affection-safe w.r.t. $\Sigma$_ if
every variable in ${q}^{-}$ occurs at a position in ${q}^{+}$ that is not
jointly affected.

Since all common (e.g., restricted, Skolem, oblivious) chases are compatible
with joint affection, we can use their outputs to answer affection-safe BNCQs.

######  Theorem 2.

For every rule set $\Sigma$, database $\mathcal{D}$, and affection-safe BNCQ
$q$, we have $\Sigma,\mathcal{D}\models_{c}q$ iff $\mathcal{M}\models q$ for
some222The restricted chase, e.g., can yield distinct chase results depending
on rule application order. Any of them can be used here. chase $\mathcal{M}$
computed for $\Sigma$ and $\mathcal{D}$ by a chase procedure compatible with
jointly affected positions (Proposition 1).

###### Proof.

The “only if” direction follows from Theorem 1. For the “if” direction, let
$\mathcal{M}$ be as in the claim. By Proposition 1, terms $t$ at positions
$\langle{a,i}\rangle$ in $\mathcal{M}$ that are not jointly affected are
constants. Let $\mathcal{C}$ be the core model of $\Sigma$ and $\mathcal{D}$.
By universality, there are homomorphisms $h_{1}:\mathcal{M}\to\mathcal{C}$ and
$h_{2}:\mathcal{C}\to\mathcal{M}$. Suppose $\mathcal{M}\models q$ by a match
$h:{q}^{+}\to\mathcal{M}$ with $h({q}^{-})\cap\mathcal{M}=\emptyset$, but
$\Sigma,\mathcal{D}\not\models_{c}q$. Since $h_{1}\circ
h({q}^{+})\subseteq\mathcal{C}$, this means $h_{1}\circ
h({q}^{-})\neq\emptyset$. Hence there is $p(\boldsymbol{t})\in{q}^{-}$ with
$p(h_{1}\circ h(\boldsymbol{t}))\in\mathcal{C}\setminus\mathcal{M}$, and
therefore $p(h_{2}\circ h_{1}\circ h(\boldsymbol{t}))\in\mathcal{M}$. As
$h(\boldsymbol{t})$ contains only constants, this implies
$p(h(\boldsymbol{t}))\in\mathcal{M}$, contradicting our assumption that
$\mathcal{M}\models q$. ∎

## Core-Safe BNCQs

Affection safety ensures that chase-based models only entail negative BNCQ
atoms if they match null-free facts, which always agree across all universal
models. We now relax this requirement based on the recent notion of
_restraints_ (Krötzsch 2020), which allow us to identify a larger set of
“safe” positions to bind to. The next example, adopted from Alviano, Morak,
and Pieris (2017), illustrates the problem:

######  Example 2.

Take as database $\mathcal{D}=\\{p(\text{A}),f(\text{B},\text{A})\\}$
(mnemonics: parent, father-of, equal) and rules

$\displaystyle f(x,y)$ $\displaystyle\rightarrow e(x,x)$ (2) $\displaystyle
p(x)$ $\displaystyle\rightarrow\exists y.\ f(y,x)\wedge e(y,y)$ (3)

We can obtain two restricted chases on
$\Sigma=\\{\eqref{eq:equali},\eqref{eq:redu}\\}$ and $\mathcal{D}$:
$\mathcal{U}_{1}=\mathcal{D}\cup\\{e(\text{B},\text{B})\\}$ and
$\mathcal{U}_{2}=\mathcal{D}\cup\\{f(n,\text{A}),e(n,n),e(\text{B},\text{B})\\}$.
For $\mathcal{U}_{1}$, we only apply (2) for match
$h_{1}=\\{x\mapsto\text{B},y\mapsto\text{A}\\}$; then (3) is satisfied. For
$\mathcal{U}_{2}$, we apply (3) for match $h_{2}=\\{x\mapsto\text{A}\\}$, and
then rule (2) for match $h_{1}$. The BNCQ $q=\exists x_{1},x_{2},y.\
f(x_{1},y)\wedge f(x_{2},y)\wedge\neg e(x_{1},x_{2})$ is such that
$\mathcal{U}_{1}\not\models q$ and $\mathcal{U}_{2}\models q$. Since
$\mathcal{U}_{1}$ is the core model of $\Sigma$ and $\mathcal{D}$, we obtain
$\Sigma,\mathcal{D}\not\models_{c}q$.

Arguably, the construction of $\mathcal{U}_{2}$ should not have applied (3)
with the extended match $h_{2}^{\star}=\\{x\mapsto\text{A},y\mapsto n\\}$,
because $\mathcal{U}_{2}$ eventually does not need $n$ to satisfy (3). Indeed,
$h_{2}^{+}=\\{x\mapsto\text{A},y\mapsto\text{B}\\}$ would be another way to
extend $h_{2}$ to satisfy (3). Functions that remap heads of prior rule
applications to alternative structures in a chase are called _alternative
matches_ , and they can be shown to occur whenever a restricted chase fails to
produce a core (Krötzsch 2020).

######  Definition 7.

Let $\mathcal{I}_{a}\subseteq\mathcal{I}_{b}$ be interpretations such that
$\mathcal{I}_{a}$ is obtained from applying rule $r$ for extended match
$h^{\star}$. A homomorphism $h^{\prime}:h^{\star}(\text{{\sf
head}}(r))\to\mathcal{I}_{b}$ is an _alternative match of $h$_ if

  * •

$h^{\prime}(t)=t$ for all terms $t$ in $h^{\star}(\text{{\sf body}}(r))$, and

  * •

there is a null $n$ in $h^{\star}(\text{{\sf head}}(r))$ that does not occur
in $h^{\prime}(h^{\star}(\text{{\sf head}}(r)))$.

The occurrence of alternative matches in a restricted chase is associated with
structures that do not occur in the core (Krötzsch 2020). Such structures
could lead to additional BNCQ matches. Since alternative matches involve
nulls, affection safety can mitigate this by forcing variables in negative
atoms to match constants. However, it is more general and still safe if we
merely restrict to elements that are not directly or indirectly related to
potential alternative matches. The existence of alternative matches in a real
chase is undecidable, but we can (over)approximate such matches by considering
chase-like interactions of pairs of rules. Based on this approach of defining
_restraints_ between rules (Krötzsch 2020), we can identify existential
variables that are at risk of producing redundant structures:

######  Definition 8.

A rule $r_{1}$ _restrains_ rule $r_{2}$, written
$r_{1}\mathrel{\prec^{\Box}}{}r_{2}$, if there are interpretations
$\mathcal{I}_{a}\subseteq\mathcal{I}_{b}$ and a function $h_{2}$ where

  1. 1.

$\mathcal{I}_{b}$ is obtained by applying $r_{1}$ for match $h_{1}$,

  2. 2.

$\mathcal{I}_{a}$ is obtained by applying $r_{2}$ for match $h_{2}$,

  3. 3.

$h_{2}$ has an alternative match $h^{\prime}{:}\;h_{2}^{\star}(\text{{\sf
head}}(r_{2}))\,{\to}\,\mathcal{I}_{b}$, and

  4. 4.

$h_{2}$ has no alternative match $h_{2}^{\star}(\text{{\sf
head}}(r_{2}))\to\mathcal{I}_{b}\setminus h_{1}^{\star}(\text{{\sf
head}}(r_{1}))$.

In this situation, a variable $x\in\text{{\sf Var}}_{\exists}(r_{2})$ is
_restrained_ if $h_{2}^{\star}(x)$ does not occur in
$h^{\prime}(h_{2}^{\star}(\text{{\sf head}}(r_{2})))$. We write $R_{\Sigma}$
for the set of all restrained variables of a rule set $\Sigma$.

Variables in $R_{\Sigma}$ may produce nulls that are not represented in the
core model. Moreover, such nulls may be involved in further rule applications
that derive additional structures that deviate from the core. To find
positions of elements that are certain to agree with the core, we therefore
consider all positions that are influenced by restrained variables in the
sense of Definition 3.

######  Definition 9.

Let $\Sigma$ be a rule set. A position $\pi$ is _core-safe (w.r.t. $\Sigma$)_
if it is not $R_{\Sigma}$-influenced. A BNCQ $q$ is _core-safe w.r.t.
$\Sigma$_ if every variable in ${q}^{-}$ occurs at a core-safe position in
${q}^{+}$.

Reconsidering query $q$ of Example 2, we find that $q$ is not core-safe w.r.t.
the given rule set. Positions
$\langle{e,1}\rangle,\langle{e,2}\rangle,\langle{f,1}\rangle$ are not core-
safe and variables $x_{1}$ and $x_{2}$ both occur at $\langle{f,1}\rangle$ in
${q}^{+}$. This explains why this example admits restricted chase sequences on
which the entailment of $q$ disagrees with the core model. Indeed, for core-
safe BNCQs, this problem can never occur:

######  Theorem 3.

For every rule set $\Sigma$, database $\mathcal{D}$, core-safe BNCQ $q$, and
restricted chase $\mathcal{M}$ of $\Sigma$ and $\mathcal{D}$, we find that
$\Sigma,\mathcal{D}\models_{c}q$ iff $\mathcal{M}\models q$.

The “only if” direction is again clear from Theorem 1. The proof for the “if”
direction is given below. The key insight is that terms at core-safe positions
in a chase $\mathcal{M}$ must belong to the core instance $\mathcal{M}_{c}$ of
$\mathcal{M}$ (cf. Lemma 1). This is a similar situation as for affection-
safety, where we showed that variables at affection-safe positions much be
instantiated with constants, which therefore occur in the core.

######  Lemma 2.

For a restricted chase $\mathcal{M}$ of rule set $\Sigma$ and database
$\mathcal{D}$, and core instance $\mathcal{M}_{c}$ of $\mathcal{M}$, if a term
$t$ occurs at a core-safe position in $\mathcal{M}$, then $t$ occurs in
$\mathcal{M}_{c}$.

###### Proof.

Let $\mathcal{C}$ be a core model of $\Sigma$ and $\mathcal{D}$. Let
$h_{1}:\mathcal{M}\to\mathcal{C}$ be a homomorphism (existence by
$\mathcal{M}$ being universal) and $h_{2}:\mathcal{C}\to\mathcal{M}_{c}$ be
the isomorphism for which $h_{2}^{-1}$ agrees with $h_{1}$, i.e.,
$h_{2}^{-1}(t)=u$ if $h_{1}(t)=u$. The existence of an isomorphism $i$ is
ensured by Lemma 1. Furthermore, consider the restriction
$h^{\prime}_{1}:\mathcal{M}_{c}\to\mathcal{C}$ of $h_{1}$ to
$\mathcal{M}_{c}$. By Lemma 1 (2), $i\circ
h^{\prime}_{1}:\mathcal{M}_{c}\to\mathcal{M}_{c}$ is an isomorphism. Set
$h_{2}:=(h^{\prime}_{1})^{-1}$, which is an isomorphism since $(i^{-1}\circ
i\circ h^{\prime}_{1})=h^{\prime}_{1}$ is an isomorphism.

We subsequently analyse the homomorphism $h^{\prime}:=h_{2}\circ h_{1}$. With
respect to the choice of $h_{2}$, we show that if $t$ occurs at a core-safe
position in $\mathcal{M}$, then $h^{\prime}(t)=t$. By induction on the chase
sequence of $\mathcal{M}$ (i.e., $\mathcal{M}^{0},\mathcal{M}^{1},\ldots$).

Base:

Since $\mathcal{M}^{0}=\mathcal{D}\subseteq\mathcal{M}_{c}$, every term $t$ in
$\mathcal{M}^{0}$ is a constant and $h^{\prime}(t)=t$ because $h^{\prime}$ is
homomorphism.

Hypothesis:

For $k\in\mathbb{N}$, $h^{\prime}(t)=t$ for every term $t$ in
$\mathcal{M}^{k}$ that occurs at a core-safe position.

Step:

We consider the step from $\mathcal{M}^{k}$ to $\mathcal{M}^{k+1}$ by rule
$r\in\Sigma$ and (unsatisfied) match $h$ with
$\mathcal{M}^{k+1}=\mathcal{M}^{k}\cup h^{\star}(\text{{\sf head}}(r))$. Let
$a(\boldsymbol{t})\in\text{{\sf head}}(r)$ and $\langle{a,i}\rangle$ be core-
safe ($i\in\\{1,\ldots,|\boldsymbol{t}|\\}$). We distinguish two cases for
$h^{\star}(t_{i})=u$: If $u\in\mathbf{C}$, $h^{\prime}(u)=u$ because
$h^{\prime}$ is homomorphism. If $u\in\mathbf{N}$, $t_{i}\in\mathbf{V}$ and we
distinguish two more cases, namely (a) $t_{i}$ is a universally quantified
(i.e., frontier) variable and (b) $t_{i}$ is an existentially quantified
variable of $r$.

In case (a), $t_{i}$ occurs at a core-safe position in $\text{{\sf body}}(r)$
by Lemma 3 (1). Thus, the induction hypothesis guarantees $h^{\prime}(u)=u$.

For case (b), we show that $u\neq h^{\prime}(u)$ implies an alternative match
$\hat{h^{\prime}}$ of $h$. If $h(x)=t$ for a non-frontier body variable $x$ of
$r$, $\hat{h^{\prime}}(t)=t$. Otherwise, $\hat{h^{\prime}}(t)=h^{\prime}(t)$.
First, we show that $\hat{h^{\prime}}(t)=t$ for all terms $t$ occurring in
$h(\text{{\sf body}}(r))$: If $t\in\mathbf{C}$, the claim follows from
$h^{\prime}$ being a homomorphism. If $t\in\mathbf{N}$, there must have been
(i) a non-frontier variable $x$ with $h(x)=t$ or (ii) a frontier variable $y$
in $r$ with $h(y)=t$. In case (i), $\hat{h^{\prime}}(t)=t$ by definition. In
case (ii), $y$ occurs at a core-safe position in $\text{{\sf body}}(r)$ by
Lemma 3 (2). Thus, the induction hypothesis ensures that
$\hat{h^{\prime}}(t)=h^{\prime}(t)=t$.

By the choice of $h_{2}$, if $h^{\prime}(u)\neq u$, then $u\notin\text{{\sf
range}}(h^{\prime})$. Thus, $h^{\prime}(u)$ is an alternative to $u$, that
does not occur in $h^{\prime}(h^{\star}(\text{{\sf head}}(r)))$.
$\hat{h^{\prime}}$ is an alternative match for $h$ in $\mathcal{M}$. But then
$t_{i}\in R_{\Sigma}$ and $\langle{a,i}\rangle\in\Omega_{t_{i}}$,
contradicting our assumption that $\langle{a,i}\rangle$ is core-safe.

Hence, every term in a core-safe position in $\mathcal{M}$ also occurs in
$\mathcal{M}_{c}$. ∎

###### Proof of Theorem 3.

For the remaining “if” direction, suppose $\mathcal{M}\models q$. Then there
is a homomorphism $h:{q}^{+}\to\mathcal{M}$ with
$h({q}^{-})\cap\mathcal{M}=\emptyset$. For core model $\mathcal{C}$ of
$\Sigma$ and $\mathcal{D}$ and core instance $\mathcal{M}_{c}$ of
$\mathcal{M}$, let $h_{1}:\mathcal{M}\to\mathcal{C}$ /
$h_{2}:\mathcal{C}\to\mathcal{M}_{c}$ be the respective
homomorphism/isomorphism (by Lemma 1).

Let $r(\mathbf{t})\in{q}^{-}$. We show that
$r(h(\mathbf{t}))\notin\mathcal{M}$ implies
$r(h_{1}(h(\mathbf{t})))\notin\mathcal{C}$. Every variable in $\mathbf{t}$
occurs in at least one core-safe position in ${q}^{+}$ (by core-safety of
$q$). Thus, every term in $\mathbf{u}=h(\mathbf{t})$ occurs in
$\mathcal{M}_{c}$ by Lemma 2. Since $r(\mathbf{u})\notin\mathcal{M}$ (and
$r(\mathbf{u})\notin\mathcal{M}_{c}$), $r(h_{1}(\mathbf{u}))\notin\mathcal{C}$
because, otherwise, $r(h_{2}(h_{1}(\mathbf{u})))\in\mathcal{M}_{c}$, which
contradicts $r(\mathbf{u})\notin\mathcal{M}_{c}$ (therefore,
$\notin\mathcal{M}$) because $h_{2}\circ h_{1}$ is an isomorphism on
$\mathcal{M}_{c}$ (by Lemma 1 (2)). ∎

Core-safe BNCQs therefore are a significant generalisation of affection-safe
BNCQs, at the cost of requiring the use of the restricted chase – or any other
correct chase procedure that ensures that its results are subsets of some
restricted chase. In practice, this includes chase implementations that use
specific strategies to decide the order in which rules are applied, e.g., by
prioritising Datalog rules (which never introduce unnecessary nulls) (Urbani
et al. 2018). Since Definition 8 identifies restrained variables under the
assumption that rule $r_{1}$ might be applied before rule $r_{2}$, the fact
that some rule application orders are generally impossible (or simply did not
happen in a specific run) allows us to consider more variables _effectively
core-safe_.

######  Definition 10.

Let $\Sigma$ be a rule set, $\mathcal{D}$ a database, and
$S=\mathcal{D}^{0},\mathcal{D}^{1},\mathcal{D}^{2},\ldots$ a restricted chase
sequence with $\mathcal{D}^{i-1}\xrightarrow{r_{i},h_{i}}\mathcal{D}^{i}$ for
$i\geq 1$, $r_{i}\in\Sigma$ and (unsatisfied) match $h_{i}$. A variable $x\in
R_{\Sigma}$ is _effectively restrained in $S$_ if there are $j<k$, such that
$x$ occurs in rule $r_{j}$ and $r_{k}\mathrel{\prec^{\Box}}r_{j}$. The set of
all effectively restrained variables in $S$ is denoted $R_{S}$.

A position $\langle{a,i}\rangle$ is _effectively core-safe w.r.t. $S$_ if it
is not $R_{S}$-influenced. A BNCQ $q$ is _effectively core-safe w.r.t. $S$_ if
every variable $x$ in ${q}^{-}$ occurs at an effectively core-safe position in
${q}^{+}$.

Effective core safety marks even more positions as safe for BNCQs to query
for.

######  Theorem 4.

For every rule set $\Sigma$, database $\mathcal{D}$, restricted chase sequence
$S=\mathcal{D}^{0},\mathcal{D}^{1},\mathcal{D}^{2},\ldots$ over $\Sigma$ and
$\mathcal{D}$ with chase result $\mathcal{M}=\bigcup_{i\geq
0}\mathcal{D}^{i}$, and BNCQ $q$ that is effectively core-safe for $S$, it
holds that $\Sigma,\mathcal{D}\models_{c}q$ iff $\mathcal{M}\models q$.

###### Proof sketch.

Similar argumentation as for the proof of Theorem 3. In particular, terms at
effectively core-safe positions do occur in the core instance
$\mathcal{M}_{c}$ of $\mathcal{M}$ (cf. Lemma 2). ∎

Our results put BNCQ answering under core entailment semantics into reach for
practical implementations. Indeed, chase procedures, including the restricted
chase, are supported by efficient implementations, and the computation of
restraints is of the same complexity as the application of a single rule,
namely $\Sigma_{2}^{\mathsf{P}}$-complete (Krötzsch 2020). This may at first
seem harder than computing the core, which is known to be DP-complete (Fagin,
Kolaitis, and Popa 2005), but the crucial difference is that the worst-case
complexity of core computation refers to the size of the whole chase (often
millions of facts), whereas for rule applications and restraint checking, it
is about the size of a single rule (typically dozens of facts). This may
explain why no general implementation of the core chase is available today.

## Rules with Negation

We turn our attention to _normal rules_ , which admit negated atoms in their
bodies and can naturally be viewed as a recursive generalisation of BNCQ
answering. Using our previous insights, we first define a chase-based
semantics for such rules in cases where rule bodies are core-safe. We then
generalise this by _stratifying_ rule sets in a way that is compatible with
restraints, generalising the notion of _full stratification_ for normal
existential rules (Krötzsch 2020). This yields a unique and well-defined
semantics that we call _perfect core semantics_.

A _normal existential rule_ is an expression
$r=\forall\boldsymbol{x},\boldsymbol{y}.\
\varphi[\boldsymbol{x},\boldsymbol{y}]\wedge\chi[\boldsymbol{x},\boldsymbol{y}]\to\exists\boldsymbol{z}.\
\psi[\boldsymbol{y},\boldsymbol{z}]$, such that
$\exists\boldsymbol{x},\boldsymbol{y}.\
\varphi[\boldsymbol{x},\boldsymbol{y}]\wedge\chi[\boldsymbol{x},\boldsymbol{y}]$
is a BNCQ, and $\psi[\boldsymbol{y},\boldsymbol{z}]$ is a conjunction of
atoms. We use $\text{{\sf body}}^{+}(r)$ and $\text{{\sf body}}^{-}(r)$ for
the sets of all atoms in $\varphi$ and $\chi$. A _match_ of $r$ in an
interpretation $\mathcal{I}$ is a homomorphism $h:\text{{\sf
body}}^{+}(r)\to\mathcal{I}$ with $h(\text{{\sf
body}}^{-}(r))\cap\mathcal{I}=\emptyset$. Other notions are as defined for
rules without negation.

The restricted chase procedure of Definition 1 can then directly be applied to
normal rules. This does not in general lead to a sound reasoning algorithm,
since a rule might be applicable due to the absence of a negated atom that is
inferred later on in the chase. Chase sequences where this does not happen
have been called _generating_ and can be used to define a kind of stable model
semantics for normal existential rules (Baget et al. 2014).

A well-known approach to obtain generating chase sequences is _stratification_
, where rules are partitioned into a sequence of sets (“strata”) such that
rules in higher strata cannot derive facts that occur negatively in rules of
lower strata. For (normal) existential rules, stratifications have been
defined using three relations between rules: _positive reliances_
$r_{1}\mathrel{\prec^{+}}r_{2}$ express that $r_{1}$ might derive facts that
allow $r_{2}$ to be applied, _negative reliances_
$r_{1}\mathrel{\prec^{-}}r_{2}$ express that $r_{1}$ might derive facts that
prevent a possible application of $r_{2}$ since they occur in $\text{{\sf
body}}^{-}(r_{2})$, and _restraints_ $r_{1}\mathrel{\prec^{\Box}}r_{2}$ are as
in Definition 8 with the additional condition that $h_{1}$ and $h_{2}$ are
also matches (for normal rules) with respect to $\mathcal{I}_{b}$. Formal
definitions of these notions for normal rules are provided in the appendix.

######  Example 3.

Consider the rules (mnemonics: parent, father-of, male, child-of, adult,
older-than-3, tired)

$\displaystyle p(x)$ $\displaystyle\to\exists v.\ f(x,v)\wedge m(v)$ (4)
$\displaystyle f(x,y)$ $\displaystyle\to m(y)\wedge c(y,x)$ (5) $\displaystyle
f(x,y)\wedge\text{{\bf not}\,}a(x)\wedge\text{{\bf not}\,}o(x)$
$\displaystyle\to t(y)$ (6) $\displaystyle a(x)$ $\displaystyle\to o(x)$ (7)

We have $\eqref{ex_nl_mc}\mathrel{\prec^{\Box}}\eqref{ex_nl_fm}$,
$\eqref{ex_nl_fm}\mathrel{\prec^{+}}\eqref{ex_nl_mc}$, and
$\eqref{ex_nl_fm}\mathrel{\prec^{+}}\eqref{ex_nl_t}$. There are no other
relations, in particular
$\eqref{ex_nl_o}\not\mathrel{\prec^{-}}\eqref{ex_nl_t}$ since
$\eqref{ex_nl_o}$ is only applicable in cases where $\eqref{ex_nl_t}$ is not
applicable anyway.

For a set of normal rules $\Sigma$, let $R_{\Sigma}$ denote the set of
restrained variables as of Definition 8, modified for normal rules as
mentioned above. The set of $R_{\Sigma}$-influenced and core-safe positions is
defined as before, ignoring negated atoms in rules. Then a rule $r\in\Sigma$
is _core-safe_ if every variable in $\text{{\sf body}}^{-}(r)$ occurs on a
core-safe position in $\text{{\sf body}}^{+}(r)$. A first simple observation
highlights a case where the restricted chase can safely be applied to normal
rules:

######  Proposition 3.

Let $\Sigma$ be a set of normal rules such that (1) all rules in $\Sigma$ are
core-safe and (2) there is no negative reliance
$r_{1}\mathrel{\prec^{-}}r_{2}$ between any rules $r_{1},r_{2}\in\Sigma$. Then
every restricted chase sequence over $\Sigma$ and any database $\mathcal{D}$
is generating and yields a model of $\Sigma$ and $\mathcal{D}$. Moreover, all
of these models are homomorphically equivalent.

The full proof of this result is included in the appendix.

######  Example 4.

Let $\Sigma$ denote the set of rules in Example 3. We find that
$R_{\Sigma}=\\{v\\}$ because of
$\eqref{ex_nl_mc}\mathrel{\prec^{\Box}}\eqref{ex_nl_fm}$, such that
$R_{\Sigma}$-influenced positions are $\langle{f,2}\rangle$,
$\langle{m,1}\rangle$, $\langle{c,1}\rangle$, $\langle{t,1}\rangle$. Hence,
(6) is core-safe, and Proposition 3 applies.

For a database $\mathcal{D}=\\{p(A),f(A,B)\\}$, we can obtain the restricted
chases $\mathcal{U}_{1}=\mathcal{D}\cup\\{m(B),c(B,A),t(B)\\}$ (by applying
(5) before (4)) and
$\mathcal{U}_{2}=\mathcal{U}_{1}\cup\\{f(A,n),m(n),c(n,A),t(n)\\}$ (by
applying (4) before (5)). Though distinct, they are homomorphically equivalent
and $\mathcal{U}_{1}$ is their unique core.

Example 4 also illustrates a case that is covered by Proposition 3 but is not
in scope of the previously defined _full stratification_ , which we recall and
adapt next. As opposed to traditional stratifications, the definition of
Krötzsch (2020) effectively allows some rules (esp. those that are not the
target of any $\mathrel{\prec^{-}}$ or $\mathrel{\prec^{\Box}}$) to appear in
multiple strata.

######  Definition 11.

For a set $\Sigma$ of normal rules, a list
$\mathcal{S}=\langle{\Sigma_{1},\ldots,\Sigma_{n}}\rangle$ with
$\Sigma=\bigcup_{i=1}^{n}\Sigma_{n}$ is a _quasi stratification_ if, for all
rules $r_{1}\in\Sigma_{i}$ and $r_{2}\in\Sigma_{j}$,

  1. 1.

if $r_{1}\mathrel{\prec^{+}}r_{2}$ then $i\leq j$,

  2. 2.

if $r_{1}\mathrel{\prec^{-}}r_{2}$ then $i<j$,

  3. 3.

if $r_{1}\mathrel{\prec^{\Box}}r_{2}$ then $i\leq j$.

A quasi stratification $\mathcal{S}$ is a _full stratification_ if $i<j$ holds
in case (3); it is a _core-safe stratification_ if all rules in $\Sigma_{k}$
are core-safe for $\Sigma_{k}$ for all $k\in\\{1,\ldots,n\\}$.

######  Example 5.

The rules of Example 3 do not admit a full stratification due to the cycle
$\eqref{ex_nl_mc}\mathrel{\prec^{\Box}}\eqref{ex_nl_fm}\mathrel{\prec^{+}}\eqref{ex_nl_mc}$,
but they can be a stratum in a core-safe stratification. We add further rules

$\displaystyle f(x,y)$ $\displaystyle\rightarrow e(y,y)$ (8) $\displaystyle
f(x,y_{1})$ $\displaystyle\wedge f(x,y_{2})\wedge\text{{\bf
not}\,}e(y_{1},y_{2})\rightarrow d(y_{1},y_{2})$ (9)

Then $\eqref{ex_nl_fm}\mathrel{\prec^{+}}\eqref{ex_strats_e}$ and
$\eqref{ex_strats_e}\mathrel{\prec^{-}}\eqref{ex_strats_d}$. Rule (9) is not
core-safe in the set of all rules. A possible core-safe stratification is
$\mathcal{S}=\langle{\\{\eqref{ex_nl_fm},\eqref{ex_nl_mc},\eqref{ex_nl_t},\eqref{ex_nl_o}\\},\\{\eqref{ex_strats_e}\\},\\{\eqref{ex_strats_d}\\}}\rangle$.

Full stratifications have been used to define the _perfect core model_ , as
the unique model obtained by conducting a (necessarily generating) chase that
proceeds stratum by stratum. Core-safe stratification is strictly more
general, since the stricter condition $i<j$ in case (3) implies that
$R_{\Sigma_{k}}$ is empty for every stratum $\Sigma_{k}$, so that its rules
are core-safe. A suitable chase procedure for rule sets that are core-safe
stratified is given next.

######  Definition 12.

Let $\Sigma$ be a normal rule set with core-safe stratification
$\mathcal{S}=\langle{\Sigma_{1},\ldots,\Sigma_{n}}\rangle$, and let
$\mathcal{D}$ be a database. The _core-safe chase sequence_ for $\mathcal{S}$
and $\mathcal{D}$ is a list
$\mathcal{C}^{0},\mathcal{C}^{1},\ldots,\mathcal{C}^{n}$ such that

  * •

$\mathcal{C}^{0}=\mathcal{D}$, and

  * •

for every $i\in\\{1,\ldots,n\\}$, $\mathcal{C}^{i}$ is the core of a
restricted chase over $\Sigma_{i}$ and $\mathcal{C}^{i-1}$, provided that this
core is finite.

If such a sequence exists, $\mathcal{C}^{n}$ is called the _core-safe chase_
of $\Sigma$ and $\mathcal{D}$ w.r.t. $\mathcal{S}$, and we denote it by
$\mathcal{S}(\mathcal{D})$.

Note that each stratum $\Sigma_{i}$ satisfies the conditions of Proposition 3
since $\mathcal{S}$ is a core-safe stratification. Hence, the required
restricted chase exists and, since it is finite, has a unique core. In
practice, one can ensure the necessary finiteness by using acyclicity
conditions that guarantee chase termination (Cuenca Grau et al. 2013).

######  Example 6.

Consider the stratification $\mathcal{S}$ of Example 5 and the database
$\mathcal{D}=\\{p(A),f(A,B)\\}$. The core $\mathcal{C}^{1}$ of the restricted
chase over the first stratum was computed as $\mathcal{U}_{1}$ in Example 4.
$\mathcal{C}^{2}$ then is simply $\mathcal{C}^{0}\cup\\{e(B,B)\\}$, and
$\mathcal{C}^{3}=\mathcal{C}^{2}$ is the resulting core-safe chase.

Example 6 admits other core-safe stratifications, leading to different core-
safe chase sequences, but the final result is the same for all of them. The
main result of this section is that this is a general property of the core-
safe chase, so that we obtain a unique model that provides a semantics of the
underlying rule sets.

######  Theorem 5.

For rule set $\Sigma$ and database $\mathcal{D}$ with core-safe
stratifications $\mathcal{S}$ and $\mathcal{S}^{\prime}$,
$\mathcal{S}(\mathcal{D})$ is isomorphic to
$\mathcal{S}^{\prime}(\mathcal{D})$.

In the proof (see the appendix), we compare core-safe stratifications up to
simple transformations. In particular, we consider splitting and merging of
strata in a stratification to show that the resulting core-safe chases are
isomorphic. The rest of the proof is concerned with showing that all pairs of
core-safe stratifications can be transformed into one another by only
sequences of splitting and merging operations. Moreover, we find that core-
safe models generalise the perfect core models that are based on full
stratifications:

######  Proposition 4.

If a rule set is fully stratified and has a finite perfect core model, then
the latter is isomorphic to its core-safe model.

Together with Theorem 5, the previous result justifies that we call our
semantics for core-safe stratified rule sets the _perfect core semantics_ ,
since it generalises the eponymous semantics of Krötzsch (2020) without giving
up on the uniqueness of the model.

## Discussion and Conclusion

We have investigated how to answer normal Boolean conjunctive queries (BNCQs)
on sets of existential rules, and we proposed the use of core models as a
semantic reference point for this task. Arguably, cores are both intuitive and
mathematically appealing for defining a non-monotonic “negation as failure”
semantics, since they satisfy existential rules but at the same time minimise
the amount of inferences and avoid redundancies. Approaches of truth
minimisation are the basis for most non-monotonic semantics, but are much less
obvious when giving up the syntactic Herbrand semantics of logic programming.

Nevertheless, our approach also has limitations. One of them is the difficulty
of computing cores in practice, which we have addressed by identifying cases
where this can be avoided. This leads to practical procedures, which in fact
have already been implemented, though implementers are often not aware that
the method is not sound for arbitrary negative queries or stratified negation
in existential rules (Carral et al. 2019). Our core-safe chase still requires
certain core constructions (after each stratum), which might not be practical.
A possible approach to address this would be to investigate in more detail
whether the intermediate non-core structures are truly problematic for
evaluating the following rules and queries.

A more general limitation is that cores only behave well if universal models
are finite, whereas rule sets with infinite models may have several distinct
universal cores or no core that is a universal model at all (Carral et al.
2018). In this sense, the question which semantic reference point to choose in
general remains open.

## Acknowledgments

This work is partly supported by Deutsche Forschungsgemeinschaft (DFG, German
Research Foundation) in project number 389792660 (TRR 248, Center for
Perspicuous Systems), by the Bundesministerium für Bildung und Forschung
(BMBF, Federal Ministry of Education and Research) in the Center for Scalable
Data Analytics and Artificial Intelligence (ScaDS.AI), and by the Center for
Advancing Electronics Dresden (cfaed).

## References

  * Abiteboul, Hull, and Vianu (1994) Abiteboul, S.; Hull, R.; and Vianu, V. 1994.  _Foundations of Databases_.  Addison Wesley.
  * Alviano, Morak, and Pieris (2017) Alviano, M.; Morak, M.; and Pieris, A. 2017.  Stable Model Semantics for Tuple-Generating Dependencies Revisited.  In (Sallinger, den Bussche, and Geerts 2017), 377–388.
  * Baget et al. (2014) Baget, J.-F.; Garreau, F.; Mugnier, M.-L.; and Rocher, S. 2014.  Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation.  In Konieczny, S.; and Tompits, H., eds., _Proceedings of the 15th International Workshop on Non-Monotonic Reasoning (NMR 2014)_ , volume 1843-14-01 of _INFSYS Research Report_ , 176–184. TU Wien.
  * Baget et al. (2009) Baget, J.-F.; Leclère, M.; Mugnier, M.-L.; and Salvat, E. 2009.  Extending Decidable Cases for Rules with Existential Variables.  In Boutilier, C., ed., _Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI’09)_ , 677–682. IJCAI.
  * Bauslaugh (1995) Bauslaugh, B. L. 1995.  Core-like properties of infinite graphs and structures.  _Discrete Math._ , 138(1): 101–111.
  * Bellomarini, Sallinger, and Gottlob (2018) Bellomarini, L.; Sallinger, E.; and Gottlob, G. 2018.  The Vadalog System: Datalog-based Reasoning for Knowledge Graphs.  _Proceedings of the VLDB Endowment_ , 11(9): 975–987.
  * Benedikt et al. (2017) Benedikt, M.; Konstantinidis, G.; Mecca, G.; Motik, B.; Papotti, P.; Santoro, D.; and Tsamoura, E. 2017.  Benchmarking the Chase.  In (Sallinger, den Bussche, and Geerts 2017), 37–52.
  * Calì, Gottlob, and Lukasiewicz (2009) Calì, A.; Gottlob, G.; and Lukasiewicz, T. 2009.  A general datalog-based framework for tractable query answering over ontologies.  In Paredaens, J.; and Su, J., eds., _Proceedings of the 28th Symposium on Principles of Database Systems (PODS’09)_ , 77–86. ACM.
  * Carral et al. (2019) Carral, D.; Dragoste, I.; González, L.; Jacobs, C.; Krötzsch, M.; and Urbani, J. 2019.  VLog: A Rule Engine for Knowledge Graphs.  In Ghidini et al., C., ed., _Proceedings of the 18th International Semantic Web Conference (ISWC’19, Part II)_ , volume 11779 of _LNCS_ , 19–35. Springer.
  * Carral et al. (2018) Carral, D.; Krötzsch, M.; Marx, M.; Ozaki, A.; and Rudolph, S. 2018.  Preserving Constraints with the Stable Chase.  In Kimelfeld, B.; and Amsterdamer, Y., eds., _Proceedings of the 21st International Conference on Database Theory (ICDT’18)_ , volume 98 of _LIPIcs_ , 12:1–12:19. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik.
  * Cuenca Grau et al. (2013) Cuenca Grau, B.; Horrocks, I.; Krötzsch, M.; Kupke, C.; Magka, D.; Motik, B.; and Wang, Z. 2013.  Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies.  _Journal of Artificial Intelligence Research_ , 47: 741–808.
  * Deutsch, Nash, and Remmel (2008) Deutsch, A.; Nash, A.; and Remmel, J. B. 2008.  The Chase Revisited.  In Lenzerini, M.; and Lembo, D., eds., _Proceedings of the 27th Symposium on Principles of Database Systems (PODS’08)_ , 149–158. ACM.
  * Ebbinghaus, Flum, and Thomas (1994) Ebbinghaus, H.-D.; Flum, J.; and Thomas, W. 1994.  _Semantics of First-Order Languages_ , 27–57.  New York, NY: Springer New York.  ISBN 978-1-4757-2355-7.
  * Fagin et al. (2005) Fagin, R.; Kolaitis, P. G.; Miller, R. J.; and Popa, L. 2005.  Data exchange: semantics and query answering.  _Theoretical Computer Science_ , 336(1): 89–124.
  * Fagin, Kolaitis, and Popa (2005) Fagin, R.; Kolaitis, P. G.; and Popa, L. 2005.  Data exchange: Getting to the core.  _ACM Trans. Database Syst._ , 30(1): 174–210.
  * Gottlob et al. (2014) Gottlob, G.; Hernich, A.; Kupke, C.; and Lukasiewicz, T. 2014.  Stable Model Semantics for Guarded Existential Rules and Description Logics.  In Baral, C.; De Giacomo, G.; and Eiter, T., eds., _Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR’14)_ , 258–267. AAAI Press.
  * Hell and Nešetřil (1992) Hell, P.; and Nešetřil, J. 1992.  The core of a graph.  _Discrete Math._ , 109: 117–126.
  * Krötzsch (2020) Krötzsch, M. 2020.  Computing Cores for Existential Rules with the Standard Chase and ASP.  In Calvanese, D.; Erdem, E.; and Thielscher, M., eds., _Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020)_ , 603–613. IJCAI.
  * Krötzsch and Rudolph (2011) Krötzsch, M.; and Rudolph, S. 2011.  Extending Decidable Existential Rules by Joining Acyclicity and Guardedness.  In Walsh, T., ed., _Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI’11)_ , 963–968. AAAI Press/IJCAI.
  * Magka, Krötzsch, and Horrocks (2013) Magka, D.; Krötzsch, M.; and Horrocks, I. 2013.  Computing Stable Models for Nonmonotonic Existential Rules.  In Rossi, F., ed., _Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13)_ , 1031–1038. AAAI Press/IJCAI.
  * Nenov et al. (2015) Nenov, Y.; Piro, R.; Motik, B.; Horrocks, I.; Wu, Z.; and Banerjee, J. 2015.  RDFox: A Highly-Scalable RDF Store.  In Arenas, M.; Corcho, Ó.; Simperl, E.; Strohmaier, M.; d’Aquin, M.; Srinivas, K.; Groth, P. T.; Dumontier, M.; Heflin, J.; Thirunarayan, K.; and Staab, S., eds., _Proceedings of the 14th International Semantic Web Conference (ISWC’15), Part II_ , volume 9367 of _LNCS_ , 3–20. Springer.
  * Sallinger, den Bussche, and Geerts (2017) Sallinger, E.; den Bussche, J. V.; and Geerts, F., eds. 2017.  _Proceedings of the 36th Symposium on Principles of Database Systems (PODS’17)_. ACM.
  * Urbani et al. (2018) Urbani, J.; Krötzsch, M.; Jacobs, C. J. H.; Dragoste, I.; and Carral, D. 2018\.  Efficient Model Construction for Horn Logic with VLog: System description.  In Galmiche, D.; Schulz, S.; and Sebastiani, R., eds., _Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR’18)_ , volume 10900 of _LNCS_ , 680–688. Springer.

##  Appendix A Appendix

The following lemma is a technical preliminary to the proof of Lemma 2.

######  Lemma 3.

Let $\Sigma$ be a rule set and $r\in\Sigma$ with
$a(\boldsymbol{t})\in\text{{\sf head}}(r)$ and $\langle{a,i}\rangle$ ($1\leq
i\leq|\boldsymbol{t}|$) being core-safe. In a chase step from some
$\mathcal{M}$ by rule $r$ and unsatisfied match $h$:

  1. 1.

If $y$ is a frontier variable of $r$ occurring at $\langle a,i\rangle$ and
$h(y)\in\mathbf{N}$, then $y$ occurs at a core-safe position in $\text{{\sf
body}}(r)$.

  2. 2.

If $z$ is an existentially quantified variable of $r$ occurring at position
$\langle a,i\rangle$, then $z\notin R_{\Sigma}$ and all frontier variables of
$r$ occur at core-safe positions in $\text{{\sf body}}(r)$.

###### Proof.

We prove both items separately.

  1. 1.

Suppose $y$ occurs only at non-core-safe positions in $\text{{\sf body}}(r)$.
Then there must be variables $x,z\in\text{{\sf Var}}_{\exists}(\Sigma)$ with
$x\in R_{\Sigma}$, $x\leadsto^{*}z$, and $\Pi_{y}^{B}\subseteq\Omega_{z}$ (by
an inductive argument using the fact that $h(y)$ occurs in all positions in
$\Pi_{y}^{B}$). By Definition 2, $\Pi_{y}^{H}\subseteq\Omega_{z}$, which
contradicts the assumption that $\langle{a,i}\rangle$ is a core-safe position.

  2. 2.

Suppose $z\in R_{\Sigma}$, then $z\leadsto^{*}z$ and $\langle
a,i\rangle\in\Omega_{z}$, contradicting our assumption that $\langle
a,i\rangle$ is core-safe. If there is a frontier variable $y$ occurring only
at non-core-safe positions in $\text{{\sf body}}(r)$, then there are variables
$x,v\in\text{{\sf Var}}_{\exists}(\Sigma)$ with $x\in R_{\Sigma}$,
$x\leadsto^{*}v$, $\Pi_{y}^{B}\subseteq\Omega_{v}$. But then $v\leadsto z$ and
$\langle{a,i}\rangle$ is not core-safe since $x\leadsto^{*}z$ and
$\langle{a,i}\rangle\in\Omega_{z}$.∎

For a thorough understanding of the upcoming proofs, we repeat the formal
definitions of positive reliance ($\mathrel{\prec^{+}}$), negative reliance
($\mathrel{\prec^{-}}$), restraints ($\mathrel{\prec^{\Box}}$) for normal
existential rules, and fully stratified rule sets by Krötzsch (2020). For a
normal rule $r=\forall\boldsymbol{x},\boldsymbol{y}.\
\varphi[\boldsymbol{x},\boldsymbol{y}]\wedge\chi[\boldsymbol{x},\boldsymbol{y}]\rightarrow\exists\boldsymbol{z}.\
\psi[\boldsymbol{y},\boldsymbol{z}]$, by ${r}^{+}$ we denote the existential
rule $\forall\boldsymbol{x},\boldsymbol{y}.\
\varphi[\boldsymbol{x},\boldsymbol{y}]\rightarrow\exists\boldsymbol{z}.\
\psi[\boldsymbol{x},\boldsymbol{y}]$. A match $h$ for rule ${r}^{+}$ is
_generating for $r$_ on instance $\mathcal{I}$ if
$p(h(\boldsymbol{t}))\notin\mathcal{I}$ for all
$p(\boldsymbol{t})\in\text{{\sf body}}^{-}(r)$. A chase sequence
$\mathcal{D}^{0},\mathcal{D}^{1},\mathcal{D}^{2},\ldots$ is generating if for
all $i>0$, $\mathcal{D}^{i}$ was obtained by applying rule $r$ for match $h$
implies that $h$ is generating for $r$ in $\mathcal{D}^{\infty}$.

For existential rules $r_{1}$ and $r_{2}$ (without negated body atoms),
$r_{1}$ _positively relies on_ $r_{2}$ (denoted
$r_{1}\mathrel{\prec^{+}}r_{2}$) if there are instancen
$\mathcal{I}_{a}\subseteq\mathcal{I}_{b}$ and a function $h_{2}$ such that

  1. 1.

$\mathcal{I}_{b}$ is obtained from $\mathcal{I}_{a}$ by applying $r_{1}$ for
match $h_{1}$,

  2. 2.

$h_{2}$ is an unsatisfied match for $r_{2}$ on $\mathcal{I}_{b}$, and

  3. 3.

$h_{2}$ is not a match for $r_{2}$ on $\mathcal{I}_{b}$.

For normal rules $r_{1}$ and $r_{2}$, $r_{1}$ positively relies on $r_{2}$
(also denoted by $r_{1}\mathrel{\prec^{+}}r_{2}$) if
${r_{1}}^{+}\mathrel{\prec^{+}}{r_{2}}^{+}$. Similarly, $r_{1}$ restrains
$r_{2}$ (also denoted $r_{1}\mathrel{\prec^{\Box}}r_{2}$) if
${r_{1}}^{+}\mathrel{\prec^{\Box}}{r_{2}}^{+}$ by instances
$\mathcal{I}_{a}\subseteq\mathcal{I}_{b}$ and matches $h_{1}$ and $h_{2}$, as
required by Definition 8, such that the matches are generating for rules
$r_{1}/r_{2}$ on $\mathcal{I}_{b}$.

For normal rules $r_{1}$ and $r_{2}$, we say that $r_{1}$ _negatively relies
on_ $r_{2}$ (denoted $r_{1}\mathrel{\prec^{-}}r_{2}$) if there are instances
$\mathcal{I}_{a}\subseteq\mathcal{I}_{b}$ such that

  1. 1.

$\mathcal{I}_{b}$ is obtained by applying ${r_{1}}^{+}$ for match $h_{1}$,

  2. 2.

$\mathcal{I}_{a}$ is obtained by applying ${r_{2}}^{+}$ for match $h_{2}$,

  3. 3.

$h_{2}$ is not generating for $r_{2}$ on $\mathcal{I}_{b}$, and

  4. 4.

$h_{2}$ is generating for $r_{2}$ on $\mathcal{I}_{b}\setminus
h_{1}(\text{{\sf head}}(r_{1}))$.

### Proof of Proposition 3

###### Proof.

Let $S=\mathcal{D}^{0},\mathcal{D}^{1},\mathcal{D}^{2},\ldots$ be a restricted
chase sequence of $\Sigma$ and $\mathcal{D}$, and let $\mathcal{D}^{\infty}$
be its respective chase. If $\mathcal{D}^{\infty}$ is not a model of $\Sigma$
and $\mathcal{D}$, there must be a rule $r\in\Sigma$ with an unsatisfied match
$h:\text{{\sf body}}(r)\to\mathcal{D}^{\infty}$, contradicting fairness (3. of
Definition 1) of the chase procedure.

Suppose, $S$ was not generating. Then there would be an instance
$\mathcal{D}^{i}$ ($i>0$) in $S$ that is obtained by applying a rule $r$ for
match $h$ on $\mathcal{D}^{i-1}$, so that $h$ is not generating for $r$ on
$\mathcal{D}^{\infty}$. As $h$ is generating for $r$ w.r.t.
$\mathcal{D}^{i-1}$, there must be a first instance $\mathcal{D}^{j}$ $(j\geq
i)$ in $S$ for which $h$ is not generating, obtained from applying some rule
$r^{\prime}$ for match $h^{\prime}$ to $\mathcal{D}^{j-1}$. In particular, $h$
is generating for $r$ w.r.t. $\mathcal{D}^{j-1}$. But that means,
$r^{\prime}\mathrel{\prec^{-}}r$, contradicting assumption (2).

Let $\mathcal{M}_{1},\mathcal{M}_{2}$ be two chases of $\Sigma$ and
$\mathcal{D}$, and $\mathcal{M}_{1}^{0},\mathcal{M}_{1}^{1},\ldots$ be the
chase sequence to obtain $\mathcal{M}_{1}$. We show that there is a
homomorphism from $\mathcal{M}_{1}^{i}$ to $\mathcal{M}_{2}$ for all
$i\in\\{0,1,\ldots\\}$, providing $\mathcal{M}_{1}\to\mathcal{M}_{2}$.
$\mathcal{M}_{2}\rightleftarrows\mathcal{M}_{1}$ is obtained by a symmetric
argument.

Base:

For $i=0$, we have $\mathcal{M}_{1}^{0}=\mathcal{D}\subseteq\mathcal{M}_{2}$.
The identity on $\mathcal{D}$, $\mathsf{id}_{\mathcal{D}}$, is a homomorphism.

Step:

For $i>0$ with $\mathcal{M}_{1}^{i}$ obtained from $\mathcal{M}_{1}^{i-1}$ by
applying rule $r$ for match $h$, so that there is a homomorphism
$h_{i-1}:\mathcal{M}_{1}^{i-1}\to\mathcal{M}_{2}$ (by induction hypothesis).
We need to extend $h_{i-1}$ to $h_{i}:\mathcal{M}_{1}^{i}\to\mathcal{M}_{2}$.
Since $h$ is a match for $r$ in $\mathcal{M}_{1}^{i}$ and $h_{i-1}$ is a
homomorphism, $h^{\prime}=h_{i}\circ h$ is a match for $\text{{\sf
body}}^{+}(r)$ in $\mathcal{M}_{2}$. If $h^{\prime}$ is a match for $r$ in
$\mathcal{M}_{2}$, then there is an extension $h^{\prime\star}$ with
$h^{\prime\star}(\text{{\sf head}}(r))\subseteq\mathcal{M}_{2}$ and we can use
$h^{\prime\star}$ to define $h_{i}$ as follows:

$h_{i}:=h_{i-1}\cup\\{(h^{\star}(x),h^{\prime\star}(x))\mid x\in\text{{\sf
Var}}_{\exists}(r)\\}\text{.}$

It remains to be shown that $h^{\prime}$ is a match for $r$ in
$\mathcal{M}_{2}$. If $\text{{\sf body}}^{-}(r)=\emptyset$, the claim follows
immediately since $\text{{\sf body}}(r)=\text{{\sf body}}^{+}(r)$. If
$\text{{\sf body}}^{-}(r)\neq\emptyset$, we need to show that for all
$p(\boldsymbol{x})\in\text{{\sf body}}^{-}(r)$,
$p(h^{\prime}(\boldsymbol{x}))\notin\mathcal{M}_{2}$.

Towards a contradiction, suppose there is some $p(\boldsymbol{x})\in\text{{\sf
body}}^{-}(r)$ with $p(h^{\prime}(\boldsymbol{x}))\in\mathcal{M}_{2}$. Let us
denote $h^{\prime}(\boldsymbol{x})$ by $\boldsymbol{u}$ and
$h(\boldsymbol{x})$ by $\boldsymbol{t}$. Then
$p(\boldsymbol{u})\in\mathcal{D}$ because $\Sigma$ is
$\mathrel{\prec^{-}}$-free (by assumption (2)) and there is a $p$-atom in
$\text{{\sf body}}^{-}(r)$. Furthermore, since
$p(\boldsymbol{t})\notin\mathcal{M}_{1}^{i-1}$ and
$h_{i-1}(\boldsymbol{t})=\boldsymbol{u}$, there is at least one fresh null in
$\boldsymbol{t}$ because otherwise, $\boldsymbol{t}=\boldsymbol{u}$ due to the
(inductive) construction of $h_{i-1}$. In the course of constructing
$h_{i-1}$, these fresh nulls must have been introduced by some rule
applications, whereas $\mathcal{M}_{2}$ provides satisfying assignments for
these nulls with terms from the input instance $\mathcal{D}$. Hence, there
must be rules in $\Sigma$ that have been applied to add properties to
$\boldsymbol{u}$ in order to admit a homomorphism from $\boldsymbol{t}$ to
$\boldsymbol{u}$. These rules certainly restrain the rules that produced the
fresh nulls in $\boldsymbol{t}$, or have been influenced by non-core null
insertions. Thus, $\boldsymbol{t}$ contains at least one null that does not
belong to the core instance of $\mathcal{M}_{1}$. But this contradicts the
assumption (1), that $\Sigma$ is core-safe, since at least $r$ is not core-
safe. Hence, the assumption that $p(\boldsymbol{u})\in\mathcal{M}_{2}$ is
wrong and $h^{\prime}$ is a match for $r$ in $\mathcal{M}_{2}$. ∎

### Proof of Theorem 5

We subsequently abstract from the actual contents of a quasi stratification
and treat it as a list of subsets of $\Sigma$ that meets certain requirements,
which we assert by binary relations $\mathrel{\preceq}$ and
$\mathrel{\not\approx}$ over $\Sigma$. Thereby $\mathrel{\preceq}$ is the
transitive and reflexive closure of all positive and negative reliances in
$\Sigma$, as well as restraints over $\Sigma$ (i.e.,
$\mathrel{\preceq}:=(\mathrel{\prec^{+}}\cup\mathrel{\prec^{-}}\cup\mathrel{\prec^{\Box}})^{*}$),
whereas $\mathrel{\not\approx}:=\mathrel{\prec^{-}}$. A core-safe quasi
stratification in this framework is a sequence of rule subsets
$\mathcal{S}=\langle{\Sigma_{1},\Sigma_{2},\ldots,\Sigma_{k}}\rangle$ of
$\Sigma$ respecting $\mathrel{\preceq}$ and $\mathrel{\not\approx}$, such that
for all $r_{1}\in\Sigma_{i}$ and $r_{2}\in\Sigma_{j}$, (1)
$r_{1}\mathrel{\preceq}r_{2}$ implies $i\leq j$, and (2)
$r_{1}\mathrel{\not\approx}r_{2}$ implies $i\neq j$. Note,
$r_{1}\mathrel{\prec^{-}}r_{2}$ implies $r_{1}\mathrel{\preceq}r_{2}$ and
$r_{1}\mathrel{\not\approx}r_{2}$, implementing the requirement that $r_{1}$
must occur in a strictly earlier stratum. Throughout the rest of this section
we call a core-safe quasi stratification just a stratification. We may further
assume a rule set $\Sigma$ to be given as a structure
$\langle{\Sigma,\mathrel{\preceq},\mathrel{\not\approx}}\rangle$.

######  Definition 13.

For rule set $\Sigma$, a stratification
$\mathcal{S}=\langle{\Sigma_{1},\ldots,\Sigma_{k}}\rangle$ is in _standard
form_ if for all $i\in\\{1,\ldots,k\\}$ and rules $r_{1},r_{2}\in\Sigma_{i}$,
$r_{1}\mathrel{\preceq}r_{2}$.

######  Proposition 5.

If any stratification of a rule set $\Sigma$ exists, then there is one in
standard form.

###### Proof.

If we view $\langle{\Sigma,\mathrel{\preceq}}\rangle$ as a graph structure, we
can identify its strongly connected components, which we subsequently call
$\mathrel{\preceq}$-SCCs. Take all $\mathrel{\preceq}$-SCCs as the components
of a standard form stratification. A stratification exists if every
$\mathrel{\preceq}$-SCC $\Sigma_{i}$ is $\mathrel{\not\approx}$-free, which
means that there are no rules $r_{1},r_{2}\in\Sigma_{i}$ with
$r_{1}\mathrel{\not\approx}r_{2}$ (Abiteboul, Hull, and Vianu 1994). The set
of all $\mathrel{\preceq}$-SCCs of $\Sigma$ forms a partially ordered set (by
$\mathrel{\preceq}$), from which one topological ordering can be chosen as the
required stratification in standard form. ∎

######  Definition 14.

For rule set $\Sigma$ and stratification
$\mathcal{S}=\langle{\Sigma_{1},\ldots,\Sigma_{i-1},\Sigma_{i},\Sigma_{i+1},\ldots,\Sigma_{k}}\rangle$,
define

$\displaystyle\mathsf{split}_{i}(\mathcal{S},\Sigma^{l},\Sigma^{r})$
$\displaystyle:=\langle{\Sigma_{1},\ldots,\Sigma_{i-1},\Sigma^{l},\Sigma^{r},\Sigma_{i+1},\ldots,\Sigma_{k}}\rangle$

for non-empty subsets $\Sigma^{l},\Sigma^{r}$ of $\Sigma_{i}$ with
$\Sigma_{i}=\Sigma^{l}\cup\Sigma^{r}$, and

$\displaystyle\mathsf{merge}_{i}(\mathcal{S})$
$\displaystyle:=\langle{\Sigma_{1},\ldots,\Sigma_{i-1},\Sigma_{i}\cup\Sigma_{i+1},\ldots,\Sigma_{k}}\rangle\text{.}$

A split/merge is _valid_ if the result is a stratification.

Split and merge operations can be concatenated in an operation sequence
$\sigma=o_{1};\ldots;o_{n}$ ($n\in\mathbb{N}$). The operation of $\sigma$
applied to a stratification $\mathcal{S}$ works as follows: First, $o_{1}$ is
applied to $\mathcal{S}$ yielding a stratification $\mathcal{S}_{1}$.
Operation $o_{i}$ for $i>1$ is applied to the result of the previous step
(i.e., $\mathcal{S}_{i-1}$). Note,
$\mathsf{merge}_{i}(\mathsf{split}_{i}(\mathcal{S},\Sigma^{l},\Sigma^{r}))=\mathcal{S}$
and
$\mathsf{split}_{i}(\mathsf{merge}_{i}(\mathcal{S}),\Sigma_{i},\Sigma_{i+1})=\mathcal{S}$.

######  Proposition 6.

For every stratification $\mathcal{S}$ of rule set $\Sigma$, a stratification
$\mathcal{S}^{\prime}$ in standard form can be reached by a sequence of valid
split operations.

###### Proof.

Let $S$ be a $\mathrel{\preceq}$-SCC of $\Sigma$. Note, there must be a
stratum $\Sigma_{i}$ of $\mathcal{S}$ with $S\subseteq\Sigma_{i}$. This holds
for every $\mathrel{\preceq}$-SCCs of $\Sigma$. Thus, it is sufficient to
iterate over all strata and extract their SCCs via splitting, while
maintaining the order $\mathrel{\preceq}$. $\mathrel{\not\approx}$ can never
be violated after splitting a stratum. ∎

######  Proposition 7.

Let $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ be two standard form
stratifications of $\Sigma$. Then there is a sequence of valid split/merge
operations on $\mathcal{S}_{1}$ to yield $\mathcal{S}_{2}$.

###### Proof.

Merge independent strata and split them in reverse order. Since both standard
form stratifications obey $\mathrel{\preceq}$ and $\mathrel{\not\approx}$ on
$\Sigma$, this procedure terminates successfully. ∎

######  Lemma 4.

Let $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ be two stratifications of rule set
$\Sigma$. Then we can transform $\mathcal{S}_{1}$ into $\mathcal{S}_{2}$ by
sequences of valid split/merge operations.

###### Proof.

By Proposition 6, we obtain standard form stratifications
$\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ just by valid
sequences of split operations $\sigma_{1}$ and $\sigma_{2}$. By Proposition 7,
there is a valid operation sequence $\sigma^{\prime}$, transforming
$\mathcal{S}_{1}^{\prime}$ into $\mathcal{S}_{2}^{\prime}$. Thus, we obtain a
sequence $\sigma$ of valid operations by
$\sigma_{1};\sigma^{\prime};\sigma_{2}^{-1}$, where $\sigma_{2}^{-1}$ is the
dual of $\sigma_{2}$, replacing every $\mathsf{split}_{i}(\ldots)$ by
$\mathsf{merge}_{i}(\ldots)$ and reversing the order of the operation
sequence. ∎

Hence, the set of all stratifications forms an equivalence class under valid
transformations. Next, we show that the result of a single stratum is unique
(up to isomorphisms). Therefore, we first show that the chase on a single
stratum produces a unique model up to homomorphisms, from which the claim
directly follows (homomorphically equivalent models have the same core up to
isomorphisms). The following claim generalizes Proposition 3 in that we assume
an input instance $\mathcal{I}$ (with or without nulls) that is core, instead
of an input database $\mathcal{D}$.

######  Lemma 5.

Let $\Sigma$ be a set of normal rules such that (1) all rules are core-safe
w.r.t. $\Sigma$ and (2) $\Sigma$ is $\mathrel{\not\approx}$-free. Then every
restricted chase sequence over $\Sigma$ and any core instance $\mathcal{I}$ is
generating and a yields a model of $\Sigma$ and $\mathcal{D}$. All of these
models are equivalent up to homomorphisms.

###### Proof.

The proof is almost the same as for Proposition 3, except that in the part
where we show that every two chases are homomorphically equivalent, we need to
distinguish fresh nulls (i.e., the ones that have been produced throughout the
chase) from those nulls already present in $\mathcal{I}$. Otherwise, the exact
same argumentation works here as well. ∎

######  Corollary 1.

Let $\Sigma$ be a set of normal rules adhering to the restriction of Lemma 5
and $\mathcal{I}$ a core instance. Then cores are unique for all chases over
$\Sigma$ and $\mathcal{I}$.

Next we show a general result about valid splitting and merging: The result of
a split/merge operation on a rule set yields the same core. As a notational
convention in this proof we abbreviate the fact that an instance $\mathcal{J}$
was obtained by applying rule $r$ for match $h$ on $\mathcal{I}$ by
$\mathcal{I}\xrightarrow{r,h}\mathcal{J}$.

######  Lemma 6.

Let $\Sigma$ be a set of rules, so that
$\mathcal{S}_{0}=\langle{\Sigma}\rangle$ is a core-safe quasi stratification.
Furthermore, let $\mathcal{S}=\langle{\Sigma_{1},\Sigma_{2}}\rangle$ be a
valid split of $\langle{\Sigma}\rangle$. For every core instance
$\mathcal{I}$, we have $\mathcal{S}_{0}(\mathcal{I})$ is isomorphic to
$\mathcal{S}(\mathcal{I})$.

###### Proof.

We know already that the chases of $\Sigma$ and $\mathcal{I}$ have a unique
core by Corollary 1 (due to Lemma 5). We will therefore look at the core-safe
chase sequence of $\mathcal{S}$, which is a sequence of the three core models
$\mathcal{C}_{0},\mathcal{C}_{1},\mathcal{C}_{3}$.
$\mathcal{C}_{0}=\mathcal{I}$. $\mathcal{C}_{1}$ is the core of a restricted
chase sequence $\mathcal{I}^{0},\mathcal{I}^{1}\ldots\mathcal{I}^{m}$ of
$\Sigma_{1}$ and $\mathcal{I}$, where $\mathcal{I}^{0}=\mathcal{I}$, and
$\mathcal{I}^{i-1}\xrightarrow{r_{i},h_{i}}\mathcal{I}^{i}$ for an unsatisfied
match $h_{i}$ of $r_{i}\in\Sigma_{1}$ for $0<i\geq m$. Since $\mathcal{C}_{1}$
is the core of $\mathcal{I}_{m}$, there is a homomorphism
$c_{1}:\mathcal{I}^{m}\to\mathcal{C}_{1}$. Second, we get the chase sequence
$\mathcal{J}^{0},\mathcal{J}^{1},\ldots,\mathcal{J}^{n}$ of $\Sigma_{2}$ and
$\mathcal{C}_{1}$, where $\mathcal{J}^{0}=\mathcal{C}_{1}$, and
$\mathcal{J}^{j-1}\xrightarrow{r_{m+j},h_{m+j}}\mathcal{J}^{j}$ for
$r_{m+j}\in\Sigma_{2}$ and unsatisfied match $h_{m+j}$. Analogously to $c_{1}$
there is a homomorphism $c_{2}:\mathcal{J}^{n}\to\mathcal{C}_{2}$.

#### Simulation:

We can use the chase sequences above as a starting point for a chase sequence
$\mathcal{K}^{0},\mathcal{K}^{1},\ldots$ of $\Sigma$ and $\mathcal{I}$. The
first $m$ steps use the rule applications of the first chase sequence. In
particular we have $\mathcal{K}^{i-1}\xrightarrow{r_{i},h_{i}}\mathcal{K}^{i}$
($0<i\leq m$). For every $i>0$, $\mathcal{K}^{i}=\mathcal{I}^{i}$ may not hold
because the injection of fresh nulls cannot be controlled. However,
$\mathcal{K}^{i}$ and $\mathcal{I}^{i}$ are surely isomorphic. Therefore, we
will not distinguish $\mathcal{K}$-instances from $\mathcal{I}$-instances and
go on with the proof as if
$\mathcal{K}^{0},\ldots,\mathcal{K}^{m}=\mathcal{I}^{0},\ldots,\mathcal{I}^{m}$.
Note, $\mathcal{K}^{m}$ is a model of $\Sigma_{1}$ and $\mathcal{I}$ (by Lemma
5) and since $\langle{\Sigma}\rangle$ and
$\langle{\Sigma_{1},\Sigma_{2}}\rangle$ are core-safe quasi stratifications,
$\Sigma_{1}$ is satisfied in all further steps of the chase sequence. Since
$\mathcal{C}_{1}\subseteq\mathcal{I}^{m}=\mathcal{K}^{m}$, we can continue
with the second chase sequence as follows:
$\mathcal{K}^{m}\mathcal{K}^{m+1}\ldots\mathcal{K}^{m+n}$ is the sequence
where $\mathcal{K}^{m+j-1}\xrightarrow{r_{m+j},h_{m+j}}\mathcal{K}^{m+j}$
($0<j\leq n$).
$\mathcal{K}^{0}\ldots\mathcal{K}^{m}\mathcal{K}^{m+1}\ldots\mathcal{K}^{m+n}$
is an initial chase sequence of $\Sigma$ and $\mathcal{I}$. As for the first
chase sequence, we will further assume that
$\mathcal{J}^{j}\subseteq\mathcal{K}^{m+j}$ ($0\leq j\leq n$), although the
injection of nulls in $\mathcal{K}$-instances may differ from those in
$\mathcal{J}$-instances (isomorphism argument). Since we did not have a core
construction step on $\mathcal{K}^{m}$, there may be unsatisfied matches for
rules in $\Sigma$ in $\mathcal{K}^{m+n}$, which we will show to refer to non-
core structures only.

#### Stuttering:

Let $\mathcal{K}^{m+n+1},\mathcal{K}^{m+n+2},\ldots$ be a continuation of the
initial chase sequence $\mathcal{K}^{0}\ldots\mathcal{K}^{m+n}$ of $\Sigma$
and $\mathcal{I}$. Recall that every chase step subsequent to
$\mathcal{K}^{m+n}$ stems from a rule application $r\in\Sigma_{2}$. By
induction on $i\geq 0$, we show that there is a homomorphism
$\mathcal{K}^{m+n+i}\to\mathcal{C}_{2}$.

Base:

For $i=0$, we have $\mathcal{K}^{m+n+i}=\mathcal{K}^{m+n}$ for which we take

$c_{0}(t):=\left\\{\begin{array}[]{ccl}c_{2}(c_{1}(t))&&\text{if $t$ is a term
of $\mathcal{C}_{1}$}\\\ c_{2}(t)&&\text{otherwise.}\end{array}\right.$

As $\mathcal{K}^{m+n}=\mathcal{I}^{m}\cup\mathcal{J}^{n}$,
$c_{0}(\mathcal{K}^{m+n})=\mathcal{C}_{2}$.

Step:

For $\mathcal{K}^{i-1}\xrightarrow{r,h}\mathcal{K}^{i}$ ($m+n<i$), let
$c:\mathcal{K}^{j-1}\to\mathcal{C}_{2}$ be the homomorphism by induction
hypothesis. By $h^{\prime}=c\circ h$ we obtain a match for $r$ in
$\mathcal{C}_{2}$ because $c$ is a homomorphism and $\text{{\sf body}}(r)$ is
a core-safe BNCQ (cf. proof of Proposition 3). $h^{\prime}$ is already
satisfied in $\mathcal{C}_{2}$, which means there is an extension
$h^{\prime\star}$ of $h^{\prime}$ with $h^{\prime\star}(\text{{\sf
head}}(r))\subseteq\mathcal{C}_{2}$. Define
$c^{\prime}=c\cup\\{(h^{\star}(x),h^{\prime\star}(x))\mid x\in\text{{\sf
Var}}_{\exists}(\rho)\\}$ as the homomorphism
$\mathcal{K}^{m+n+j}\to\mathcal{C}_{2}$.

Finally, since finiteness of $\mathcal{C}_{2}$ is enforced by Definition 12,
there the chase sequence $\mathcal{K}^{0},\mathcal{K}^{1},\ldots$ is
terminating at some instance $\mathcal{K}^{m+n+p}$ for $p\geq 0$, for which we
have $\mathcal{K}^{m+n+p}\to\mathcal{C}_{2}$, making $\mathcal{C}_{2}$ the
core of $\mathcal{K}^{m+n+p}$. ∎

###### Proof of Theorem 5.

Let $\mathcal{S}$ and $\mathcal{S}^{\prime}$ be two core-safe quasi
stratifications. $\mathcal{S}$ can be transformed into $\mathcal{S}^{\prime}$
by only valid split/merge operations (by Lemma 4). Each one of these
transformations produces a stratification with an equivalent core-safe chase
()up to isomorphisms) by Lemma 6. By transitivity of equivalence up to
isomorphisms, $\mathcal{S}(\mathcal{D})$ and
$\mathcal{S}^{\prime}(\mathcal{D})$ are isomorphic core models of $\Sigma$ and
$\mathcal{D}$. ∎