literals. Each such special atom is supported by a group of ground instances
of its aggregate elements.

######  Definition 20.

Let $P$ be an aggregate program, $(I,J)$ be a four-valued interpretation, and
${G}^{\epsilon}$ and ${G}^{\eta}$ be subsets of ground instances of rules in
${P}^{\epsilon}$ and ${P}^{\eta}$, respectively.

We define $\textnormal{{Propagate}}_{P}^{I,J}({G}^{\epsilon},{G}^{\eta})$ as
the set of all atoms of form $\alpha\sigma$ such that
$\epsilon_{r,a}({G}^{\epsilon},\sigma)\cup G\neq\emptyset$ and
$J\models{\pi_{G}}(a\sigma)_{I}$ with $G=\eta_{r,a}({G}^{\eta},\sigma)$ where
$\alpha$ is an atom of form (20) for aggregate $a$ in rule $r$ and $\sigma$ is
a ground substitution for $r$ mapping all global variables in $a$ to ground
terms.

An atom $\alpha\sigma$ is only considered if $\sigma$ warrants ground rules in
${G}^{\epsilon}$ or ${G}^{\eta}$, signaling that the application of $\alpha$
to the empty set is feasible when applying $\sigma$ or that there is a non-
empty set of ground aggregate elements of $\alpha$ obtained after applying
$\sigma$, respectively. If this is the case, it is checked whether the set $G$
of aggregate element instances warrants that ${\pi_{G}}(a\sigma)$ admits
stable models between $I$ and $J$.

######  Example 24.

We show how to propagate aggregates using the sets $G_{1}$ to $G_{4}$ and
their associated formulas from Example 23. Suppose that
$I=J=F\cup\\{\mathit{controls}(c_{1},c_{2})\\}$ using $F$ from Example 20.

Observe that $J\models{\pi_{G_{1}}}(a\sigma_{1})_{I}$,
$J\models{\pi_{G_{2}}}(a\sigma_{2})_{I}$,
$J\models{\pi_{G_{3}}}(a\sigma_{3})_{I}$, and
$J\not\models{\pi_{G_{4}}}(a\sigma_{4})_{I}$. Thus, we get
$\textnormal{{Propagate}}_{P}^{I,J}({G}^{\epsilon},{G}^{\eta})=\\{\alpha_{a,r}(c_{1},c_{2}),\alpha_{a,r}(c_{1},c_{3}),\alpha_{a,r}(c_{3},c_{4})\\}$.

The function Assemble yields an $\mathcal{R}$-program in which aggregate
placeholder atoms of form (20) have been replaced by their corresponding
$\mathcal{R}$-formulas.

######  Definition 21.

Let $P$ be an aggregate program, and ${G}^{\alpha}$ and ${G}^{\eta}$ be
subsets of ground instances of rules in ${P}^{\alpha}$ and ${P}^{\eta}$,
respectively.

We define $\textnormal{{Assemble}}({G}^{\alpha},{G}^{\eta})$ as the
$\mathcal{R}$-program obtained from ${G}^{\alpha}$ by replacing

  * •

all comparisons by $\top$ and

  * •

all atoms of form $\alpha\sigma$ by the corresponding formulas
${\pi_{G}}(a\sigma)$ with $G=\eta_{r,a}({G}^{\eta},\sigma)$ where $\alpha$ is
an atom of form (20) for aggregate $a$ in rule $r$ and $\sigma$ is a ground
substitution for $r$ mapping all global variables in $a$ to ground terms.

######  Example 25.

We show how to assemble aggregates using the sets $G_{1}$ to $G_{3}$ for
aggregate atoms that have been propagated in Example 24. Therefore, let
${G}^{\alpha}$ be the program consisting of the following rules:

$\displaystyle\mathit{controls}(c_{1},c_{2})\leftarrow{}$
$\displaystyle\alpha_{a,r}(c_{1},c_{2})\wedge{}\mathit{company}(c_{1})\wedge\mathit{company}(c_{2})\wedge
c_{1}\neq c_{2},$ $\displaystyle\mathit{controls}(c_{3},c_{4})\leftarrow{}$
$\displaystyle\alpha_{a,r}(c_{3},c_{4})\wedge{}\mathit{company}(c_{3})\wedge\mathit{company}(c_{4})\wedge
c_{3}\neq c_{4},\text{\ and\ }$
$\displaystyle\mathit{controls}(c_{1},c_{3})\leftarrow{}$
$\displaystyle\alpha_{a,r}(c_{1},c_{3})\wedge{}\mathit{company}(c_{1})\wedge\mathit{company}(c_{3})\wedge
c_{1}\neq c_{3}.$

Then, program $\textnormal{{Assemble}}({G}^{\alpha},{G}^{\eta})$ consists of
the following rules:

$\displaystyle\mathit{controls}(c_{1},c_{2})\leftarrow{}$
$\displaystyle{\pi_{G_{1}}}(a\sigma_{1})\wedge{}\mathit{company}(c_{1})\wedge\mathit{company}(c_{2})\wedge\top,$
$\displaystyle\mathit{controls}(c_{3},c_{4})\leftarrow{}$
$\displaystyle{\pi_{G_{2}}}(a\sigma_{2})\wedge{}\mathit{company}(c_{3})\wedge\mathit{company}(c_{4})\wedge\top,\text{\
and\ }$ $\displaystyle\mathit{controls}(c_{1},c_{3})\leftarrow{}$
$\displaystyle{\pi_{G_{3}}}(a\sigma_{3})\wedge{}\mathit{company}(c_{1})\wedge\mathit{company}(c_{3})\wedge\top.$

The next result shows how a (non-ground) aggregate program $P$ is transformed
into a (ground) $\mathcal{R}$-program $\pi_{J}(P)^{I,J}$ in the context of
certain and possible atoms $(I,J)$ via the interplay of grounding
${P}^{\epsilon}$ and ${P}^{\eta}$, deriving aggregate placeholders from their
ground instances ${G}^{\epsilon}$ and ${G}^{\eta}$, and finally replacing them
in ${G}^{\alpha}$ by the original aggregates’ contents.

######  Proposition 32.

Let $P$ be an aggregate program, $(I,J)$ be a finite four-valued
interpretation, ${G}^{\epsilon}=\mathrm{Inst}^{I,J}({P}^{\epsilon})$,
${G}^{\eta}=\mathrm{Inst}^{I,J}({P}^{\eta})$,
$\mathit{J\\!A}=\textnormal{{Propagate}}_{P}^{I,J}({G}^{\epsilon},{G}^{\eta})$,
and ${G}^{\alpha}=\mathrm{Inst}^{I,J\cup\mathit{J\\!A}}({P}^{\alpha})$.

Then,

  1. (a)

$\textnormal{{Assemble}}({G}^{\alpha},{G}^{\eta})=\pi_{J}(P)^{I,J}$ and

  2. (b)

$H({G}^{\alpha})=T_{\pi(P)_{I}}(J)$.

Property (b) highlights the relation of the possible atoms contributed by
${G}^{\alpha}$ to a corresponding application of the immediate consequence
operator. In fact, this is the first of three such relationships between
grounding algorithms and consequence operators.

1 function  _$\textnormal{{GroundComponent}}(P,I,J)$_

2
$({G}^{\alpha},{G}^{\epsilon},{G}^{\eta},f,\mathit{J\\!A},\mathit{J\\!A}^{\prime},J^{\prime})\leftarrow(\emptyset,\emptyset,\emptyset,\textnormal{{t}},\emptyset,\emptyset,\emptyset)$;

3 repeat

// ground aggregate elements

4
${G}^{\epsilon}\leftarrow{G}^{\epsilon}\cup\bigcup_{r\in{P}^{\epsilon}}\textnormal{{GroundRule}}^{I,J}_{r,f,J^{\prime}}(\iota,B(r))$;

5
${G}^{\eta}\leftarrow{G}^{\eta}\cup\bigcup_{r\in{P}^{\eta}}\textnormal{{GroundRule}}^{I,J}_{r,f,J^{\prime}}(\iota,B(r))$;

// propagate aggregates

6
$\mathit{J\\!A}\leftarrow\textnormal{{Propagate}}_{P}^{I,J}({G}^{\epsilon},{G}^{\eta})$;

// ground remaining rules

7
${G}^{\alpha}\leftarrow{G}^{\alpha}\cup\bigcup_{r\in{P}^{\alpha}}\textnormal{{GroundRule}}^{I,J\cup\mathit{J\\!A}}_{r,f,J^{\prime}\cup\mathit{J\\!A}^{\prime}}(\iota,B(r))$;

8
$(f,\mathit{J\\!A}^{\prime},J^{\prime},J)\leftarrow(\textnormal{{f}},\mathit{J\\!A},J,J\cup
H({G}^{\alpha}))$;

9

10 until  _$J^{\prime}=J$_ ;

11 return $\textnormal{{Assemble}}({G}^{\alpha},{G}^{\eta})$;

12

Algorithm 2 Grounding Components

Let us now turn to grounding components of instantiation sequences in
Algorithm 2. The function GroundComponent takes an aggregate program $P$ along
with two sets $I$ and $J$ of ground atoms. Intuitively, $P$ is a component in
a (refined) instantiation sequence and $I$ and $J$ form a four-valued
interpretation $(I,J)$ comprising the certain and possible atoms gathered
while grounding previous components (although their roles get reversed in
Algorithm 3). After variable initialization, GroundComponent loops over
consecutive rule instantiations in ${P}^{\alpha}$, ${P}^{\epsilon}$, and
${P}^{\eta}$ until no more possible atoms are obtained. In this case, it
returns in Algorithm 2 the $\mathcal{R}$-program obtained from ${G}^{\alpha}$
by replacing all ground aggregate placeholders of form (20) with the
$\mathcal{R}$-formula corresponding to the respective ground aggregate. The
body of the loop can be divided into two parts: Algorithms 2 to 2 deal with
aggregates and Algorithms 2 and 2 care about grounding the actual program. In
more detail, Algorithms 2 and 2 instantiate programs ${P}^{\epsilon}$ and
${P}^{\eta}$, whose ground instances, ${G}^{\epsilon}$ and ${G}^{\eta}$, are
then used in Algorithm 2 to derive ground instances of aggregate placeholders
of form (20). The grounded placeholders are then added via variable
$\mathit{J\\!A}$ to the possible atoms $J$ when grounding the actual program
${P}^{\alpha}$ in Algorithm 2, where $J^{\prime}$ and
$\mathit{J\\!A}^{\prime}$ hold the previous value of $J$ and $\mathit{J\\!A}$,
respectively. For the next iteration, $J$ is augmented in Algorithm 2 with all
rule heads in ${G}^{\alpha}$ and the flag $f$ is set to false. Recall that the
purpose of $f$ is to ensure that initially all rules are grounded. In
subsequent iterations, duplicates are omitted by setting the flag to false and
filtering rules whose positive bodies are a subset of the atoms
$J^{\prime}\cup\mathit{J\\!A}^{\prime}$ used in previous iterations.

While the inner workings of Algorithm 2 follow the blueprint given by
Proposition 32. its outer functionality boils down to applying the stable
operator of the corresponding ground program in the context of the certain and
possible atoms gathered so far.

######  Proposition 33.

Let $P$ be an aggregate program, $(\mathit{I\\!C},\mathit{J\\!C})$ be a finite
four-valued interpretation, and
$J=S_{\pi(P)}^{\mathit{J\\!C}}(\mathit{I\\!C})$.

Then,

  1. (a)

$\textnormal{{GroundComponent}}(P,\mathit{I\\!C},\mathit{J\\!C})$ terminates
iff $J$ is finite.

If $J$ is finite, then

  1. (b)

$\textnormal{{GroundComponent}}(P,\mathit{I\\!C},\mathit{J\\!C})=\pi_{\mathit{J\\!C}\cup
J}(P)^{\mathit{I\\!C},\mathit{J\\!C}\cup J}$ and

  2. (c)

$H(\textnormal{{GroundComponent}}(P,\mathit{I\\!C},\mathit{J\\!C}))=J$.

1 function  _$\textnormal{{Ground}}(P)$_

2 let ${({P}_{i})}_{i\in\mathbb{I}}$ be a refined instantiation sequence for
$P$;

3 $(F,G)\leftarrow(\emptyset,\emptyset)$;

4 foreach  _$i\in\mathbb{I}$_ do

5 let ${P}_{i}^{\prime}$ be the program obtained from ${P}_{i}$ as in
Definition 13;

6 $F\leftarrow
F\cup\textnormal{{GroundComponent}}({P}_{i}^{\prime},H(G),H(F))$;

7 $G\leftarrow G\cup\textnormal{{GroundComponent}}({P}_{i},H(F),H(G))$;

8

9 return $G$;

10

Algorithm 3 Grounding Programs

Finally, Algorithm 3 grounds an aggregate program by iterating over the
components of one of its refined instantiation sequences. Just as Algorithm 2
reflects the application of a stable operator, function Ground follows the
definition of an approximate model when grounding a component (cf. Definition
13). At first, facts are computed in Algorithm 3 by using the program stripped
from rules being involved in a negative cycle overlapping with the present or
subsequent components. The obtained head atoms are then used in Algorithm 3 as
certain context atoms when computing the ground version of the component at
hand. The possible atoms are provided by the head atoms of the ground program
built so far, and with roles reversed in Algorithm 3. Accordingly, the whole
iteration aligns with the approximate model of the chosen refined
instantiation sequence (cf. Definition 14), as made precise next.

Our grounding algorithm computes implicitly the approximate model of the
chosen instantiation sequence and outputs the corresponding ground program; it
terminates whenever the approximate model is finite.

######  Theorem 34.

Let $P$ be an aggregate program, ${({P}_{i})}_{i\in\mathbb{I}}$ be a refined
instantiation sequence for $P$, and $(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$
and $(I_{i},J_{i})$ be defined as in 15 and 16.

If ${({P}_{i})}_{i\in\mathbb{I}}$ is selected by Algorithm 3 in Algorithm 3,
then we have that

  1. (a)

the call $\textnormal{{Ground}}(P)$ terminates iff
$\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})$ is finite, and

  2. (b)

if $\mathit{AM}({({P}_{i})}_{i\in\mathbb{I}})$ is finite, then
$\textnormal{{Ground}}(P)=\bigcup_{i\in\mathbb{I}}\pi_{\mathit{J\\!C}_{i}\cup
J_{i}}({P}_{i})^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(I_{i},J_{i})}$.

As already indicated by Theorem 29, grounding is governed by the series of
consecutive approximate models $(I_{i},J_{i})$ in (16) delineating the stable
models of each ground program in a (refined) instantiation sequence. Whenever
each of them is finite, we also obtain a finite grounding of the original
program. Note that the entire ground program is composed of the ground
programs of each component in the chosen instantiation sequence. Hence,
different sequences may result in different overall ground programs.

Most importantly, our grounding machinery guarantees that an obtained finite
ground program has the same stable models as the original non-ground program.

######  Corollary 35 (Main result).

Let $P$ be an aggregate program.

If $\textnormal{{Ground}}(P)$ terminates, then $P$ and
$\textnormal{{Ground}}(P)$ have the same well-founded and stable models.

######  Example 26.

${P}_{5,1}^{\prime}=\emptyset$

(a) $I_{5,1}=I_{4}\cup H(\textnormal{{GC}}({P}_{5,1}^{\prime},J_{4},I_{4}))$

(b) $J_{5,1}=J_{4}\cup
H(\textnormal{{GC}}(\vphantom{{P}_{5,1}^{\prime}}{P}_{5,1},I_{5,1},J_{4}))$

(c) $I_{5,2}=I_{5,1}\cup
H(\textnormal{{GC}}({P}_{5,2}^{\prime},J_{5,1},I_{5,1}))$

(d) $J_{5,2}=J_{5,1}\cup
H(\textnormal{{GC}}(\vphantom{{P}_{5,2}^{\prime}}{P}_{5,2},I_{5,2},J_{5,1}))$

(e) $I_{6}=I_{5,2}\cup H(\textnormal{{GC}}({P}_{6}^{\prime},J_{5,2},I_{5,2}))$

(f) $J_{6}=J_{5,2}\cup
H(\textnormal{{GC}}(\vphantom{{P}_{6}^{\prime}}{P}_{6},I_{6},J_{5,2}))$

(g) $I_{7}=I_{6}\cup H(\textnormal{{GC}}({P}_{7}^{\prime},J_{6},I_{6}))$

(h) $J_{7}=J_{6}\cup
H(\textnormal{{GC}}(\vphantom{{P}_{7}^{\prime}}{P}_{7},I_{7},J_{6}))$

Table 1: Grounding of components ${P}_{5,1}$, ${P}_{5,2}$, ${P}_{6}$, and
${P}_{7}$ from Example 19 where
$\textnormal{{GC}}=\textnormal{{GroundComponent}}$.

The execution of the grounding algorithms on Example 19 is illustrated in
Table 1. Each individual table depicts a call to GroundComponent where the
header above the double line contains the (literals of the) rules to be
grounded and the rows below trace how nested calls to GroundRule proceed. The
rules in the header contain the body literals in the order as they are
selected by GroundRule with the rule head as the last literal. Calls to
GroundRule are depicted with vertical lines and horizontal arrows. A vertical
line represents the iteration of the loop in Algorithms 1 to 1. A horizontal
arrow represents a recursive call to GroundRule in Algorithm 1. Each row in
the table not marked with $\times$ corresponds to a ground instance as
returned by GroundRule. Furthermore, because all components are stratified, we
only show the first iteration of the loop in Algorithms 2 to 2 of Algorithm 2
as the second iteration does not produce any new ground instances.

Grounding components ${P}_{1}$ to ${P}_{4}$ results in the programs
$F=G=\\{u(1)\leftarrow\top,u(2)\leftarrow\top,v(2)\leftarrow\top,v(3)\leftarrow\top\\}$.
Since grounding is driven by the sets of true and possible atoms, we focus on
the interpretations $I_{i}$ and $J_{i}$ where $i$ is a component index in the
refined instantiation sequence. We start tracing the grounding starting with
$I_{4}=J_{4}=\\{u(1),u(2),v(2),v(3)\\}$.

The grounding of ${P}_{5,1}$ is depicted in Tables 1(a) and 1(b). We have
$\mathcal{E}=\\{b/1\\}$ because predicate $b/1$ is used in the head of the
rule in ${P}_{5,2}$. Thus,
$\textnormal{{GroundComponent}}(\emptyset,J_{4},I_{4})$ in Algorithm 3 returns
the empty set because ${P}_{5,1}^{\prime}=\emptyset$. We get $I_{5,1}=I_{4}$.
In the next line, the algorithm calls
$\textnormal{{GroundComponent}}({P}_{5,1},I_{5,1},J_{4})$ and we get
$J_{5,1}=\\{p(1),p(2)\\}$. Note that at this point, it is not known that
$q(1)$ is not derivable and so the algorithm does not derive $p(1)$ as a fact.

The grounding of ${P}_{5,2}$ is given in Tables 1(c) and 1(d). This time, we
have $\mathcal{E}=\emptyset$ and ${P}_{5,2}={P}_{5,2}^{\prime}$. Thus, the
first call to GroundRule determines $q(3)$ to be true while the second call
additionally determines the possible atom $q(2)$.

The grounding of ${P}_{6}$ is illustrated in Tables 1(e) and 1(f). Note that
we obtain that $x$ is possible because $p(1)$ was not determined to be true.

The grounding of ${P}_{7}$ is depicted in Tables 1(g) and 1(h). Note that,
unlike before, we obtain that $y$ is false because $q(3)$ was determined to be
true.

Furthermore, observe that the choice of the refined instantiation sequence
determines the output of the algorithm. In fact, swapping ${P}_{5,1}$ and
${P}_{5,2}$ in the sequence would result in $x$ being false and $y$ being
possible.

$\displaystyle u(1)$ $\displaystyle u(2)$ $\displaystyle v(2)$ $\displaystyle
v(3)$ $\displaystyle p(1)$
$\displaystyle\leftarrow{\neg}q(1)\wedge{\color[rgb]{0.00,0.40,0.13}u(1)}$
$\displaystyle p(2)$
$\displaystyle\leftarrow{\neg}q(2)\wedge{\color[rgb]{0.00,0.40,0.13}u(2)}$
$\displaystyle q(2)$
$\displaystyle\leftarrow{\neg}p(2)\wedge{\color[rgb]{0.00,0.40,0.13}v(2)}$
$\displaystyle q(3)$
$\displaystyle\leftarrow{\color[rgb]{0.00,0.40,0.13}{\neg}p(3)}\wedge{\color[rgb]{0.00,0.40,0.13}v(3)}$
$\displaystyle x$ $\displaystyle\leftarrow{\neg}p(1)$ Table 2: Grounding of
Example 19 as output by gringo.

To conclude, we give the grounding of the program as output by gringo in Table
2. The grounder furthermore omits the true body literals marked in green.

######  Example 27.

We illustrate the grounding of aggregates on the company controls example in
Example 10 using the grounding sequence ${({P}_{i})}_{1\leq i\leq 9}$ and the
set of facts $F$ from Example 20. Observe that the grounding of components
${P}_{1}$ to ${P}_{8}$ produces the program $\\{a\leftarrow\top\mid a\in
F\\}$. We focus on how component ${P}_{9}$ is grounded. Because there are no
negative dependencies, the components ${P}_{9}$ and ${P}_{9}^{\prime}$ in
Algorithm 3 of Algorithm 3 are equal. To ground component ${P}_{9}$, we use
the rewriting from Example 21.

Table 3: Tracing grounding of component ${P}_{9}$ where $c=\mathit{company}$,
$o=\mathit{owns}$, and $s=\mathit{controls}$.

The grounding of component ${P}_{9}$ is illustrated in Table 3, which follows
the same conventions as in Example 26. Because the program is positive, the
calls in Algorithms 3 and 3 in Algorithm 3 proceed in the same way and we
depict only one of them. Furthermore, because this example involves a
recursive rule with an aggregate, the header consists of five rows separated
by dashed lines processed by Algorithm 2. The first row corresponds to
${P}^{\epsilon}_{9}$ grounded in Algorithm 2, the second and third to
${P}^{\eta}_{9}$ grounded in Algorithm 2, the fourth to aggregate propagation
in Algorithm 2, and the fifth to ${P}^{\alpha}_{9}$ grounded in Algorithm 2.
After the header follow the iterations of the loop in Algorithms 2 to 2.
Because the component is recursive, processing the component requires four
iterations, which are separated by solid lines in the table. The right-hand
side column of the table contains the iteration number and a number indicating
which row in the header is processed. The row for aggregate propagation lists
the aggregate atoms that have been propagated.

The grounding of rule $r_{2}$ in Row 1.1 does not produce any rule instances
in any iteration because the comparison $0>50$ is false. By first selecting
this literal when grounding the rule, the remaining rule body can be
completely ignored. Actual systems implement heuristics to prioritize such
literals. Next, in the grounding of rule $r_{3}$ in Row 1.2, direct shares
given by facts over $\mathit{owns}/3$ are accumulated. Because the rule does
not contain any recursive predicates, it only produces ground instances in the
first iteration. Unlike this, rule $r_{4}$ contains the recursive predicate
$\mathit{controls/2}$. It does not produce instances in the first iteration in
Row 1.3 because there are no corresponding atoms yet. Next, aggregate
propagation is triggered in Row 1.4, resulting in aggregate atoms
$\alpha_{a,r}(c_{1},c_{2})$ and $\alpha_{a,r}(c_{3},c_{4})$, for which enough
shares have been accumulated in Row 1.2. Note that this corresponds to the
propagation of the sets $G_{1}$ and $G_{2}$ in Example 24. With these atoms,
rule $r_{1}$ is instantiated in Row 1.5, leading to new atoms over
$\mathit{controls}/2$. Observe that, by selecting atom $\alpha_{a,r}(X,Y)$
first, GroundRule can instantiate the rule without backtracking.

In the second iteration, the newly obtained atoms over predicate
$\mathit{controls}/2$ yield atom $\eta_{e_{1},a,r}(35,c_{2},c_{1},c_{3})$ in
Row 2.3, which in turn leads to the aggregate atom $\alpha_{a,r}(c_{1},c_{3})$
resulting in further instances of $r_{4}$. Note that this corresponds to the
propagation of the set $G_{3}$ in Example 24.

The following iterations proceed in a similar fashion until no new atoms are
accumulated and the grounding loop terminates. Note that the utilized
selection strategy affects the amount of backtracking in rule instantiation.
One particular strategy used in gringo is to prefer atoms over recursive
predicates. If there is only one such atom, GroundRule can select this atom
first and only has to consider newly derived atoms for instantiation. The
table is made more compact by applying this strategy. Further techniques are
available in the database literature [Ullman (1988)] that also work in case of
multiple atoms over recursive predicates.

To conclude, we give the ground rules as output by a grounder like gringo in
Table 4. We omit the translation of aggregates because its main objective is
to show correctness of the algorithms. Solvers like clasp implement
translations or even native handling of aggregates geared toward efficient
solving [Gebser et al. (2009)]. Since our example program is positive, gringo
is even able to completely evaluate the rules to facts omitting true literals
from rule bodies marked in green.

$\displaystyle\mathit{controls}(c_{1},c_{2})\leftarrow{}$
$\displaystyle\color[rgb]{0.00,0.40,0.13}\mathrm{\\#sum}^{+}\\{60:\mathit{owns}(c_{1},c_{2},60)\\}>50$
$\displaystyle{}\wedge{}$
$\displaystyle{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{1})}\wedge{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{2})}\wedge{\color[rgb]{0.00,0.40,0.13}c_{1}\neq
c_{2}}$ $\displaystyle\mathit{controls}(c_{3},c_{4})\leftarrow{}$
$\displaystyle\color[rgb]{0.00,0.40,0.13}\mathrm{\\#sum}^{+}\\{51:\mathit{owns}(c_{3},c_{4},51)\\}>50$
$\displaystyle{}\wedge{}$
$\displaystyle{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{3})}\wedge{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{4})}\wedge{\color[rgb]{0.00,0.40,0.13}c_{3}\neq
c_{4}}$ $\displaystyle\mathit{controls}(c_{1},c_{3})\leftarrow{}$
$\displaystyle\\!\begin{aligned}
\color[rgb]{0.00,0.40,0.13}\mathrm{\\#sum}^{+}\\{&\color[rgb]{0.00,0.40,0.13}20:\mathit{owns}(c_{1},c_{3},20);\\\
&\color[rgb]{0.00,0.40,0.13}35,c_{2}:\mathit{controls}(c_{1},c_{2})\wedge\mathit{owns}(c_{2},c_{3},35)\\}>50\end{aligned}$
$\displaystyle{}\wedge{}$
$\displaystyle{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{1})}\wedge{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{3})}\wedge{\color[rgb]{0.00,0.40,0.13}c_{1}\neq
c_{3}}$ $\displaystyle\mathit{controls}(c_{1},c_{4})\leftarrow{}$
$\displaystyle\color[rgb]{0.00,0.40,0.13}\mathrm{\\#sum}^{+}\\{51,c_{3}:\mathit{controls}(c_{1},c_{3})\wedge\mathit{owns}(c_{3},c_{4},51)\\}>50$
$\displaystyle{}\wedge{}$
$\displaystyle{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{1})}\wedge{\color[rgb]{0.00,0.40,0.13}\mathit{company}(c_{4})}\wedge{\color[rgb]{0.00,0.40,0.13}c_{1}\neq
c_{4}}$ Table 4: Grounding of the company controls problem from Example 10 as
output by gringo.

##  7 Refinements

Up to now, we were primarily concerned by characterizing the theoretical and
algorithmic cornerstones of grounding. This section refines these concepts by
further detailing aggregate propagation, algorithm specifics, and the
treatment of language constructs from gringo’s input language.

###  7.1 Aggregate propagation

We used in Section 6 the relative translation of aggregates for propagation,
namely, formula ${\pi_{G}}(a\sigma)$ in Definition 20, to check whether an
aggregate is satisfiable. In this section, we identify several aggregate
specific properties that allow us to implement more efficient algorithms to
perform this check.

To begin with, we establish some properties that greatly simplify the
treatment of (arbitrary) monotone or antimonotone aggregates.

We have already seen in Proposition 24 that $\pi(a)_{I}$ is classically
equivalent to $\pi(a)$ for any closed aggregate $a$ and two-valued
interpretation $I$. Here is its counterpart for antimonotone aggregates.

######  Proposition 36.

Let $a$ be a closed aggregate.

If $a$ is antimonotone, then $\pi(a)_{I}$ is classically equivalent to $\top$
if $I\models\pi(a)$ and $\bot$ otherwise for any two-valued interpretation
$I$.

######  Example 28.

In Example 24, we check whether the interpretation $J$ satisfies the formulas
${\pi_{G_{1}}}(a\sigma_{1})_{I}$ to ${\pi_{G_{4}}}(a\sigma_{4})_{I}$.

Using Proposition 24, this boils down to checking $\sum_{e\in G_{i},J\models
B(e)}H(e)>50$ for each $1\leq i\leq 4$. We get $60>50$, $51>50$, $55>50$, and
$35\not>50$ for each $G_{i}$, which agrees with checking
$J\models{\pi_{G_{i}}}(a\sigma_{i})_{I}$.

An actual implementation can maintain a counter for the current value of the
sum for each closed aggregate instance, which can be updated incrementally and
compared with the bound as new instances of aggregate elements are grounded.

Next, we see that such counter based implementations are also possible
$\mathrm{\\#sum}$ aggregates using the $<$, $\leq$, $>$, or $\geq$ relations.
We restrict our attention to finite interpretations because Proposition 37 is
intended to give an idea on how to implement an actual propagation algorithm
for aggregates (infinite interpretations would add more special cases).
Furthermore, we just consider the case that the bound is an integer here; the
aggregate is constant for any other ground term.

######  Proposition 37.

Let $I$ be a finite two-valued interpretation, $E$ be a set of aggregate
elements, and $b$ be an integer.

For $T=H(\\{e\in\mathrm{Inst}(E)\mid I\models B(e)\\})$, we get

  1. (a)

$\pi(\mathrm{\\#sum}\\{E\\}\succ b)_{I}$ is classically equivalent to
$\pi(\mathrm{\\#sum}^{+}\\{E\\}\succ b^{\prime})$
with ${\succ}\in\\{{\geq},{>}\\}$ and $b^{\prime}=b-\mathrm{\\#sum}^{-}(T)$,
and

  2. (b)

$\pi(\mathrm{\\#sum}\\{E\\}\prec b)_{I}$ is classically equivalent to
$\pi(\mathrm{\\#sum}^{-}\\{E\\}\prec b^{\prime})$
with ${\prec}\in\\{{\leq},{<}\\}$ and $b^{\prime}=b-\mathrm{\\#sum}^{+}(T)$.

The remaining propositions identify properties that can be exploited when
propagating aggregates over the $=$ and $\neq$ relations.

######  Proposition 38.

Let $I$ be a two-valued interpretation, $E$ be a set of aggregate elements,
and $b$ be a ground term.

We get the following properties:

  1. (a)

$\pi(f\\{E\\}<b)_{I}\vee\pi(f\\{E\\}>b)_{I}\text{ implies }\pi(f\\{E\\}\neq
b)_{I}$, and

  2. (b)

$\pi(f\\{E\\}=b)_{I}\text{ implies }\pi(f\\{E\\}\leq
b)_{I}\wedge\pi(f\\{E\\}\geq b)_{I}$.

The following proposition identifies special cases when the implications in
Proposition 38 are equivalences. Another interesting aspect of this
proposition is that we can actually replace $\mathrm{\\#sum}$ aggregates over
$=$ and $\neq$ with a conjunction or disjunction, respectively, at the expense
of calculating a less precise approximate model. The conjunction is even
strongly equivalent to the original aggregate under Ferraris’ semantics but
not the disjunction.

######  Proposition 39.

Let $I$ and $J$ be two-valued interpretations, $f$ be an aggregate function
among $\mathrm{\\#count}$, $\mathrm{\\#sum}^{+}$, $\mathrm{\\#sum}^{-}$ or
$\mathrm{\\#sum}$, $E$ be a set of aggregate elements, and $b$ be an integer.

We get the following properties:

  1. (a)

for $I\subseteq J$, we have
$J\models\pi(f\\{E\\}<b)_{I}\vee\pi(f\\{E\\}>b)_{I}$ iff
$J\models\pi(f\\{E\\}\neq b)_{I}$, and

  2. (b)

for $J\subseteq I$, we have $J\models\pi(f\\{E\\}=b)_{I}$ iff
$J\models\pi(f\\{E\\}\leq b)_{I}\wedge\pi(f\\{E\\}\geq b)_{I}$.

The following proposition shows that full propagation of $\mathrm{\\#sum}$,
$\mathrm{\\#sum}^{+}$, or $\mathrm{\\#sum}^{-}$ aggregates over relations $=$
and $\neq$ involves solving the subset sum problem [Martello and Toth (1990)].
We assume that we propagate w.r.t. some polynomial number of aggregate
elements. Propagating possible atoms when using the $=$ relation, i.e., when
$I\subseteq J$, involves deciding an NP problem and propagating certain atoms
when using the $\neq$ relation, i.e., when $J\subseteq I$, involves deciding a
co-NP problem.999Note that clingo’s grounding algorithm does not attempt to
solve these problems in all cases. It simply over- or underapproximates the
satisfiability using Proposition 38. Note that the decision problem for
$\mathrm{\\#count}$ aggregates is polynomial, though.

######  Proposition 40.

Let $I$ and $J$ be finite two-valued interpretations, $f$ be an aggregate
function, $E$ be a set of aggregate elements, and $b$ be a ground term.

For $T_{I}=\\{H(e)\mid e\in\mathrm{Inst}(E),I\models B(e)\\}$ and
$T_{J}=\\{H(e)\mid e\in\mathrm{Inst}(E),J\models B(e)\\}$, we get the
following properties:

  1. (a)

for $J\subseteq I$, we have $J\models\pi(f\\{E\\}\neq b)_{I}$ iff there is no
set $X\subseteq T_{I}$ such that $f(X\cup T_{J})=b$, and

  2. (b)

for $I\subseteq J$, we have $J\models\pi(f\\{E\\}=b)_{I}$ and iff there is a
set $X\subseteq T_{J}$ such that $f(X\cup T_{I})=b$.

###  7.2 Algorithmic refinements

The calls in Algorithms 3 and 3 in Algorithm 3 can sometimes be combined to
calculate certain and possible atoms simultaneously. This can be done whenever
a component does not contain recursive predicates. In this case, it is
sufficient to just calculate possible atoms along with rule instances in
Algorithm 3 augmenting Algorithm 1 with an additional check to detect whether
a rule instance produces a certain atom. Observe that this condition applies
to all stratified components but can also apply to components depending on
unstratified components. In fact, typical programs following the generate,
define, and test methodology [Lifschitz (2002), Niemelä (2008)] of ASP, where
the generate part uses choice rules [Simons et al. (2002)] (see below), do not
contain unstratified negation at all. When a grounder is combined with a
solver built to store rules and perform inferences, one can optimize for the
case that there are no negative recursive predicates in a component. In this
case, it is sufficient to compute possible atoms along with their rule
instances and leave the computation of certain atoms to the solver. Finally,
note that gringo currently does not separate the calculation of certain and
possible atoms at the expense of computing a less precise approximate model
and possibly additional rule instances.

######  Example 29.

For the following example, gringo computes atom $p(4)$ as unknown but the
algorithms in Section 6 identify it as true.

$\displaystyle r(1,4)$ $\displaystyle p(1)$
$\displaystyle\leftarrow{\neg}q(1)$ $\displaystyle r(2,3)$ $\displaystyle
q(1)$ $\displaystyle\leftarrow{\neg}p(1)$ $\displaystyle r(3,1)$
$\displaystyle p(2)$ $\displaystyle p(Y)$ $\displaystyle\leftarrow\hbox
to0.0pt{$p(X)\wedge r(X,Y)$\hss}.$

When grounding the last rule, gringo determines $p(4)$ to be possible in the
first iteration because $p(1)$ is unknown at this point. In the second
iteration, it detects that $p(1)$ is a fact but does not use it for grounding
again. If there were further rules depending negatively on predicate $p/1$,
inapplicable rules might appear in gringo’s output.

Another observation is that the loop in Algorithm 2 does not produce further
rule instances in a second iteration for components without recursive
predicates. Gringo maintains an index [Garcia-Molina et al. (2009)] for each
positive body literal to speed up matching of literals; whenever none of these
indexes, used in rules of the component at hand, are updated, further
iterations can be skipped.

Just like dlv’s grounder, gringo adapts algorithms for semi-naive evaluation
from the field of databases. In particular, it works best on linear programs
[Abiteboul et al. (1995)], having at most one positive literal occurrence over
a recursive predicate in a rule body. The program in Example 10 for the
company controls problem is such a linear program because
$\mathit{controls}/2$ is the only recursive predicate. Algorithm 1 can easily
be adapted to efficiently ground linear programs by making sure that the
recursive positive literal is selected first. We then only have to consider
matches that induce atoms not already used for instantiations in previous
iterations of the loop in Algorithm 2 to reduce the amount of backtracking to
find rule instances. In fact, the order in which literals are selected in
Algorithm 1 is crucial for the performance of Algorithm 1. Gringo uses an
adaptation of the selection heuristics presented by lepesc01a that
additionally takes into account recursive predicates and terms with function
symbols.

To avoid unnecessary backtracking when grounding general logic programs,
gringo instantiates rules using an algorithm similar to the improved semi-
naive evaluation with optimizations for linear rules [Abiteboul et al.
(1995)].

###  7.3 Capturing gringo’s input language

We presented aggregate programs where rule heads are simple atoms. Beyond
that, gringo’s input language offers more elaborate language constructs to
ease modeling.

A prominent such construct are so-called choice rules [Simons et al. (2002)].
Syntactically, one-element choice rules have the form $\\{a\\}\leftarrow B$,
where $a$ is an atom and $B$ a body. Semantically, such a rule amounts to
$a\vee\neg a\leftarrow B$ or equivalently $a\leftarrow\neg\neg a\wedge B$. We
can easily add support for grounding choice rules, that is, rules where the
head is not a plain atom but an atom marked as a choice, by discarding choice
rules when calculating certain atoms and treating them like normal rules when
grounding possible atoms. A translation that allows for supporting head
aggregates using a translation to aggregate rules and choice rules is given by
gehakalisc15a. Note that gringo implements further refinements to omit
deriving head atoms if a head aggregate cannot be satisfied.

Another language feature that can be instantiated in a similar fashion as body
aggregates are conditional literals. Gringo adapts the rewriting and
propagation of body aggregates to also support grounding of conditional
literals.

Yet another important language feature are disjunctions in the head of rules
[Gelfond and Lifschitz (1991)]. As disjunctive logic programs, aggregate
programs allow us to solve problems from the second level of the polynomial
hierarchy. In fact, using Łukasiewicz’ theorem [Lukasiewicz (1941)], we can
write a disjunctive rule of form

$\displaystyle a\vee b$ $\displaystyle\leftarrow B$ as the shifted strongly
equivalent $\mathcal{R}$-program: $\displaystyle a$
$\displaystyle\leftarrow(b\rightarrow a)\wedge B$ $\displaystyle b$
$\displaystyle\leftarrow(a\rightarrow b)\wedge B.$

We can use this as a template to design grounding algorithms for disjunctive
programs. In fact, gringo calculates the same approximate model for the
disjunctive rule and the shifted program.

The usage of negation as failure is restricted in $\mathcal{R}$-programs. Note
that any occurrence of a negated literal $l$ in a rule body can be replaced by
an auxiliary atom $a$ adding rule $a\leftarrow l$ to the program. The
resulting program preserves the stable models modulo the auxiliary atoms. This
translation can serve as a template for double negation or negation in
aggregate elements as supported by gringo.

Integrity constraints are a straightforward extension of logic programs. They
can be grounded just like normal rules deriving an auxiliary atom that stands
for $\bot$. Grounding can be stopped whenever the auxiliary atom is derived as
certain. Integrity constraints also allow for supporting negated head atoms,
which can be shifted to rule bodies [Janhunen (2001)] resulting in integrity
constraints, and then treated like negation in rule bodies.

A frequently used convenience feature of gringo are term pools [Gebser et al.
(2015), Gebser et al. (2015)]. The grounder handles them by removing them in a
rewriting step. For example, a rule of form

$\displaystyle h(X;Y,Z)$ $\displaystyle\leftarrow p(X;Y),q(Z)$ is factored out
into the following rules: $\displaystyle h(X,Z)$ $\displaystyle\leftarrow
p(X),q(Z)$ $\displaystyle h(X,Z)$ $\displaystyle\leftarrow p(Y),q(Z)$
$\displaystyle h(Y,Z)$ $\displaystyle\leftarrow p(X),q(Z)$ $\displaystyle
h(Y,Z)$ $\displaystyle\leftarrow p(Y),q(Z)$

We can then apply the grounding algorithms developed in Section 6.

To deal with variables ranging over integers, gringo supports interval terms
[Gebser et al. (2015), Gebser et al. (2015)]. Such terms are handled by a
translation to inbuilt range predicates. For example the program

$\displaystyle h(l..u)$ for terms $l$ and $u$ is rewritten into $\displaystyle
h(A)$ $\displaystyle\leftarrow\mathit{rng}(A,l,u)$

by introducing auxiliary variable $A$ and range atom $\mathit{rng}(A,l,u)$.
The range atom provides matches including all substitutions that assign
integer values between $l$ and $u$ to $A$. Special care has to be taken
regarding rule safety, the range atom can only provide bindings for variable
$A$ but needs variables in the terms $l$ and $u$ to be provided elsewhere.

A common feature used when writing logic programs are terms involving
arithmetic expressions and assignments. Both influence which rules are
considered safe by the grounder. For example, the rule

$\displaystyle h(X,Y)$ $\displaystyle\leftarrow p(X+Y,Y)\wedge X=Y+Y$ is
rewritten into $\displaystyle h(X,Y)$ $\displaystyle\leftarrow p(A,Y)\wedge
X=Y+Y\wedge A=X+Y$

by introducing auxiliary variable $A$. The rule is safe because we can match
the literals in the order as given in the rewritten rule. The comparison
$X=Y+Y$ extends the substitution with an assignment for $X$ and the last
comparison serves as a test. Gringo does not try to solve complicated
equations but supports simple forms like the one given above.

Last but not least, gringo does not just support terms in assignments but it
also supports aggregates in assignments. To handle such kind of aggregates,
the rewriting and propagation of aggregates has to be extended. This is
achieved by adding an additional variable to aggregate replacement atoms (20),
which is assigned by propagation. For example, the rule

$\underbrace{h(X,Y)\leftarrow
q(X)\wedge\overbrace{Y=\mathrm{\\#sum}\\{Z:p(X,Z)\\}}^{a}}_{r}$ is rewritten
into $\displaystyle\epsilon_{a,r}(X)$ $\displaystyle\leftarrow q(X)$
$\displaystyle\eta_{e,a,r}(Z,X)$ $\displaystyle\leftarrow p(X,Z)\wedge q(X)$
$\displaystyle h(X,Y)$ $\displaystyle\leftarrow\alpha_{a,r}(X,Y)$

Aggregate elements are grounded as before but values for variable $Y$ are
computed during aggregate propagation. In case of multiple assignment
aggregates, additional care has to to be taken during the rewriting to ensure
that the rewritten rules are safe.

##  8 Related work

This section aims at inserting our contributions into the literature, starting
with theoretical aspects over algorithmic ones to implementations.

Splitting for infinitary formulas has been introduced by harlif16a
generalizing results of jaoitowo07a and felelipa09a. To this end, the concept
of an $A$-stable model is introduced [Harrison and Lifschitz (2016)]. We
obtain the following relationship between our definition of a stable model
relative to a set $\mathit{I\\!C}$ and $A$-stable models: For an
$\mathcal{N}$-program $P$, we have that if $X$ is a stable model of $P$
relative to $\mathit{I\\!C}$, then $X\cup\mathit{I\\!C}$ is an
$(\mathcal{A}\setminus\mathit{I\\!C})$-stable model of $P$. Similarly, we get
that if $X$ is an $A$-stable model of $P$, then $S_{P}^{X\setminus A}(X)$ is a
stable model of $P$ relative to $X\setminus A$. The difference between the two
concepts is that we fix atoms $\mathit{I\\!C}$ in our definition while
$A$-stable models allow for assigning arbitrary truth values to atoms in
$\mathcal{A}\setminus A$ [Harrison and Lifschitz (2016), Proposition 1]. With
this, let us compare our handling of program sequences to symmetric splitting
[Harrison and Lifschitz (2016)]. Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a
refined instantiation sequence of aggregate program $P$, and
$F=\bigcup_{i<j}\pi({P}_{i})$ and $G=\bigcup_{i\geq j}\pi({P}_{i})$ for some
$j\in\mathbb{I}$ such that $H(F)\neq H(G)$. We can use the infinitary
splitting theorem of harlif16a to calculate the stable model of
$F^{\wedge}\wedge G^{\wedge}$ through the $H(F)$\- and $\mathcal{A}\setminus
H(F)$-stable models of $F^{\wedge}\wedge G^{\wedge}$. Observe that
instantiation sequences do not permit positive recursion between their
components and infinite walks are impossible because an aggregate program
consists of finitely many rules inducing a finite dependency graph. Note that
we additionally require the condition $H(F)\neq H(G)$ because components can
be split even if their head atoms overlap. Such a split can only occur if
overlapping head atoms in preceding components are not involved in positive
recursion.

Next, let us relate our operators to the ones defined by truszczynski12a.
First of all, it is worthwhile to realize that the motivation of
truszczynski12a is to conceive operators mimicking model expansion in id-logic
by adding certain atoms. More precisely, let $\mathit{\Phi}$, $\mathit{St}$,
and $\mathit{Wf}$ stand for the versions of the Fitting, stable, and well-
founded operators defined by truszczynski12a. Then, we get the following
relations to the operators defined in the previous sections:

$\displaystyle\mathit{St}_{P,\mathit{I\\!C}}(J)$
$\displaystyle=\mathit{lfp}(\mathit{\Phi}_{P,\mathit{I\\!C}}(\cdot,J))$
$\displaystyle=\mathit{lfp}(T^{\mathit{I\\!C}}_{P_{J}})\cup\mathit{I\\!C}$
$\displaystyle=S_{P}^{\mathit{I\\!C}}(J)\cup\mathit{I\\!C}.$ For the well-
founded operator we obtain $\displaystyle\mathit{Wf}_{P,\mathit{I\\!C}}(I,J)$
$\displaystyle=W_{P}^{\mathit{I\\!C},\mathit{I\\!C}}(I,J)\sqcup\mathit{I\\!C}.$

Our operators allow us to directly calculate the atoms derived by a program.
The versions of truszczynski12a always include the input facts in their output
and the well-founded operator only takes certain but not possible atoms as
input.

In fact, we use operators as dematr00a to approximate the well-founded model
and to obtain a ground program. While we apply operators to infinitary
formulas (resulting from a translation of aggregates) as introduced by
truszczynski12a, there has also been work on applying operators directly to
aggregates. vabrde21a provide an overview. Interestingly, the high complexity
of approximating the aggregates pointed out in Proposition 40 has already been
identified by pedebr07a.

Simplification can be understood as a combination of unfolding (dropping rules
if a literal in the positive body is not among the head atoms of a program,
i.e., not among the possible atoms) and negative reduction (dropping rules if
an atom in the negative body is a fact, i.e., the literal is among the certain
atoms) [Brass and Dix (1999), Brass et al. (2001)]. Even the process of
grounding can be seen as a directed way of applying unfolding (when matching
positive body literals) and negative reduction (when matching negative body
literals). When computing facts, only rules whose negative body can be removed
using positive reduction are considered.

The algorithms of kestsr91a to calculate well-founded models perform a
computation inspired by the alternating sequence to define the well-founded
model as vangelder93a. Our work is different in so far as we are not primarily
interested in computing the well-founded model but the grounding of a program.
Hence, our algorithms stop after the second application of the stable operator
(the first to compute certain and the second to compute possible atoms). At
this point, a grounder can use algorithms specialized for propositional
programs to simplify the logic program at hand. Algorithmic refinements for
normal logic programs as proposed by kestsr91a also apply in our setting.

Last but not least, let us outline the evolution of grounding systems over the
last two decades.

The lparse [Syrjänen (2001a)] grounder introduced domain- or omega-restricted
programs [Syrjänen (2001b)]. Unlike safety, omega-restrictedness is not
modular. That is, the union of two omega-restricted programs is not
necessarily omega-restricted while the union of two safe programs is safe.
Apart from this, lparse supports recursive monotone and antimonotone
aggregates. However, our company controls encoding in Example 10 is not
accepted because it is not omega-restricted. For example, variable $X$ in the
second aggregate element needs a domain predicate. Even if we supplied such a
domain predicate, lparse would instantiate variable $X$ with all terms
provided by the domain predicate resulting in a large grounding. As noted by
ferlif02a, recursive nonmonotone aggregates (sum aggregates with negative
weights) are not supported correctly by lparse.

Gringo 1 and 2 add support for lambda-restricted programs [Gebser et al.
(2007)] extending omega-restricted programs. This augments the set of
predicates that can be used for instantiation but is still restricted as
compared to safe programs. That is, lambda-restrictedness is also not modular
and our company controls program is still not accepted. At the time, the
development goal was to be compatible to lparse but extend the class of
accepted programs. Notably, gringo 2 adds support for additional aggregates
[Gebser et al. (2009)]. Given its origin, gringo up to version $4$ handles
recursive nonmonotone aggregates in the same incorrect way as lparse.

The grounder of the dlv system has been the first one to implement grounding
algorithms based on semi-naive evaluation [Eiter et al. (1997)]. Furthermore,
it implements various techniques to efficiently ground logic programs [Leone
et al. (2001), Faber et al. (2001), Perri et al. (2007)]. The
$\textit{dlv}^{\mathcal{A}}$ system is the first dlv-based system to support
recursive aggregates [Dell’Armi et al. (2003)], which is nowadays also
available in recent versions of idlv [Calimeri et al. (2017)].

Gringo 3 closed up to dlv being the first gringo version to implement
grounding algorithms based on semi-naive evaluation [Gebser et al. (2011)].
The system accepts safe rules but still requires lambda-restrictedness for
predicates within aggregates. Hence, our company controls encoding is still
not accepted.

Gringo 4 implements grounding of aggregates with algorithms similar to the
ones presented in Section 6 [Gebser et al. (2015)]. Hence, it is the first
version that accepts our company controls encoding.

Finally, gringo 5 refines the translation of aggregates as proposed by
alfage15a to properly support nonmonotone recursive aggregates and refines the
semantics of pools and undefined arithmetics [Gebser et al. (2015)].

Another system with a grounding component is the idp system [De Cat et al.
(2014)]. Its grounder instantiates a theory by assigning sorts to variables.
Even though it supports inductive definitions, it relies solely on the sorts
of variables [Wittocx et al. (2010)] to instantiate a theory. In case of
inductive definitions, this can lead to instances of definitions that can
never be applied. We believe that the algorithms presented in Section 6 can
also be implemented in an idp system decreasing the instantiation size of some
problems (e.g., the company controls problem presented in Example 10).

Last but not least, we mention that not all ASP systems follow a two-phase
approach of grounding and solving but rather adapt a lazy approach by
grounding on-the-fly during solving [Palù et al. (2009), Lefèvre et al.
(2017), Weinzierl et al. (2020)].

##  9 Conclusion

We have provided a first comprehensive elaboration of the theoretical
foundations of grounding in ASP. This was enabled by the establishment of
semantic underpinnings of ASP’s modeling language in terms of infinitary
(ground) formulas [Harrison et al. (2014), Gebser et al. (2015)]. Accordingly,
we start by identifying a restricted class of infinitary programs, namely,
$\mathcal{R}$-programs, by limiting the usage of implications. Such programs
allow for tighter semantic characterizations than general
$\mathcal{F}$-programs, while being expressive enough to capture logic
programs with aggregates. Interestingly, we rely on well-founded models
[Bruynooghe et al. (2016), Truszczyński (2018)] to approximate the stable
models of $\mathcal{R}$-programs (and simplify them in a stable-models
preserving way). This is due do the fact that the (id-)well-founded-operator
enjoys monotonicity, which lends itself to the characterization of iterative
grounding procedures. The actual semantics of non-ground aggregate programs is
then defined via a translation to $\mathcal{R}$-programs. This setup allows us
to characterize the inner workings of our grounding algorithms for aggregate
programs in terms of the operators introduced for $\mathcal{R}$-programs. It
turns out that grounding amounts to calculating an approximation of the well-
founded model together with a ground program simplified with that model. This
does not only allow us to prove the correctness of our grounding algorithms
but moreover to characterize the output of a grounder like gringo in terms of
established formal means. To this end, we have shown how to split aggregate
programs into components and to compute their approximate models (and
corresponding simplified ground programs). The key instruments for obtaining
finite ground programs with finitary subformulas have been dedicated forms of
program simplification and aggregate translation. Even though, we limit
ourselves to $\mathcal{R}$-programs, we capture the core aspects of grounding:
a monotonically increasing set of possibly derivable atoms and on-the-fly
(ground) rule generation. Additional language features of gringo’s input
language are relatively straightforward to accommodate by extending the
algorithms presented in this paper.

For reference, we implemented the presented algorithms in a prototypical
grounder, $\mu$-gringo, supporting aggregate programs (see Footnote 1). While
it is written to be as concise as possible and not with efficiency in mind, it
may serve as a basis for experiments with custom grounder implementations. The
actual gringo system supports a much larger language fragment. There are some
differences compared to the algorithms presented here. First, certain atoms
are removed from rule bodies if not explicitly disabled via a command line
option. Second, translation $\pi$ is only used to characterize aggregate
propagation. In practice, gringo translates ground aggregates to monotone
aggregates [Alviano et al. (2015)]. Further translation [Bomanson et al.
(2014)] or even native handling [Gebser et al. (2009)] of them is left to the
solver. Finally, in some cases, gringo might produce more rules than the
algorithms presented above. This should not affect typical programs. A tighter
integration of grounder and solver to further reduce the number of ground
rules is an interesting topic of future research.

## References

  * Abiteboul et al. (1995) Abiteboul, S., Hull, R., and Vianu, V. 1995\.  Foundations of Databases.  Addison-Wesley.
  * Alviano et al. (2015) Alviano, M., Dodaro, C., Leone, N., and Ricca, F. 2015\.  Advances in WASP.  In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’15), F. Calimeri, G. Ianni, and M. Truszczyński, Eds. Lecture Notes in Artificial Intelligence, vol. 9345. Springer-Verlag, 40–54.
  * Alviano et al. (2015) Alviano, M., Faber, W., and Gebser, M. 2015\.  Rewriting recursive aggregates in answer set programming: Back to monotonicity.  Theory and Practice of Logic Programming 15, 4-5, 559–573.
  * Baral et al. (2007) Baral, C., Brewka, G., and Schlipf, J., Eds. 2007.  Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’07). Lecture Notes in Artificial Intelligence, vol. 4483. Springer-Verlag.
  * Belnap (1977) Belnap, N. 1977\.  A useful four-valued logic.  In Modern Uses of Multiple-Valued Logic, J. Dunn and G. Epstein, Eds. Reidel.
  * Bomanson et al. (2014) Bomanson, J., Gebser, M., and Janhunen, T. 2014\.  Improving the normalization of weight rules in answer set programs.  In Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA’14), E. Fermé and J. Leite, Eds. Lecture Notes in Artificial Intelligence, vol. 8761. Springer-Verlag, 166–180.
  * Brass and Dix (1999) Brass, S. and Dix, J. 1999\.  Semantics of (disjunctive) logic programs based on partial evaluation.  Journal of Logic Programming 40, 1, 1–46.
  * Brass et al. (2001) Brass, S., Dix, J., Freitag, B., and Zukowski, U. 2001\.  Transformation-based bottom-up computation of the well-founded model.  Theory and Practice of Logic Programming 1, 5, 497–538.
  * Bruynooghe et al. (2016) Bruynooghe, M., Denecker, M., and Truszczyński, M. 2016\.  ASP with first-order logic and definitions.  AI Magazine 37, 3, 69–80.
  * Calimeri et al. (2008) Calimeri, F., Cozza, S., Ianni, G., and Leone, N. 2008\.  Computable functions in ASP: Theory and implementation.  See Garcia de la Banda and Pontelli (2008), 407–424.
  * Calimeri et al. (2017) Calimeri, F., Fuscà, D., Perri, S., and Zangari, J. 2017\.  I-DLV: the new intelligent grounder of DLV.  Intelligenza Artificiale 11, 1, 5–20.
  * De Cat et al. (2014) De Cat, B., Bogaerts, B., Bruynooghe, M., and Denecker, M. 2014\.  Predicate logic as a modelling language: The IDP system.  CoRR abs/1401.6312.
  * Dell’Armi et al. (2003) Dell’Armi, T., Faber, W., Ielpa, G., Leone, N., and Pfeifer, G. 2003\.  Aggregate functions in disjunctive logic programming: Semantics, complexity, and implementation in DLV.  In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI’03), G. Gottlob and T. Walsh, Eds. Morgan Kaufmann Publishers, 847–852.
  * Denecker et al. (2000) Denecker, M., Marek, V., and Truszczyński, M. 2000\.  Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning.  In Logic-Based Artificial Intelligence, J. Minker, Ed. Kluwer Academic Publishers, Dordrecht, 127–144.
  * Eiter et al. (2001) Eiter, T., Faber, W., and Truszczyński, M., Eds. 2001\.  Proceedings of the Sixth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’01). Lecture Notes in Computer Science, vol. 2173. Springer-Verlag.
  * Eiter et al. (1997) Eiter, T., Leone, N., Mateis, C., Pfeifer, G., and Scarcello, F. 1997\.  A deductive system for nonmonotonic reasoning.  In Proceedings of the Fourth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’97), J. Dix, U. Furbach, and A. Nerode, Eds. Lecture Notes in Artificial Intelligence, vol. 1265. Springer-Verlag, 363–374.
  * Erdem et al. (2012) Erdem, E., Lee, J., Lierler, Y., and Pearce, D., Eds. 2012.  Correct Reasoning: Essays on Logic-Based AI in Honour of Vladimir Lifschitz. Lecture Notes in Computer Science, vol. 7265. Springer-Verlag.
  * Faber et al. (2012) Faber, W., Leone, N., and Perri, S. 2012\.  The intelligent grounder of DLV.  See Erdem et al. (2012), 247–264.
  * Faber et al. (2001) Faber, W., Leone, N., Perri, S., and Pfeifer, G. 2001\.  Efficient instantiation of disjunctive databases.  Technical Report DBAI-TR-2001-44, Technische Universität Wien.
  * Ferraris (2011) Ferraris, P. 2011\.  Logic programs with propositional connectives and aggregates.  ACM Transactions on Computational Logic 12, 4, 25.
  * Ferraris et al. (2009) Ferraris, P., Lee, J., Lifschitz, V., and Palla, R. 2009\.  Symmetric splitting in the general theory of stable models.  In Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09), C. Boutilier, Ed. AAAI/MIT Press, 797–803.
  * Ferraris and Lifschitz (2005) Ferraris, P. and Lifschitz, V. 2005\.  Weight constraints as nested expressions.  Theory and Practice of Logic Programming 5, 1-2, 45–74.
  * Fitting (2002) Fitting, M. 2002\.  Fixpoint semantics for logic programming: A survey.  Theoretical Computer Science 278, 1-2, 25–51.
  * Garcia de la Banda and Pontelli (2008) Garcia de la Banda, M. and Pontelli, E., Eds. 2008.  Proceedings of the Twenty-fourth International Conference on Logic Programming (ICLP’08). Lecture Notes in Computer Science, vol. 5366. Springer-Verlag.
  * Garcia-Molina et al. (2009) Garcia-Molina, H., Ullman, J., and Widom, J. 2009\.  Database Systems: The Complete Book, 2 ed.  Pearson Education.
  * Gebser et al. (2015) Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., and Schaub, T. 2015\.  Abstract Gringo.  Theory and Practice of Logic Programming 15, 4-5, 449–463.
  * Gebser et al. (2015) Gebser, M., Kaminski, R., Kaufmann, B., Lindauer, M., Ostrowski, M., Romero, J., Schaub, T., and Thiele, S. 2015\.  Potassco User Guide, 2 ed.  University of Potsdam.
  * Gebser et al. (2009) Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T. 2009\.  On the implementation of weight constraint rules in conflict-driven ASP solvers.  See Hill and Warren (2009), 250–264.
  * Gebser et al. (2011) Gebser, M., Kaminski, R., König, A., and Schaub, T. 2011\.  Advances in gringo series 3.  In Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’11), J. Delgrande and W. Faber, Eds. Lecture Notes in Artificial Intelligence, vol. 6645. Springer-Verlag, 345–351.
  * Gebser et al. (2009) Gebser, M., Kaminski, R., Ostrowski, M., Schaub, T., and Thiele, S. 2009\.  On the input language of ASP grounder gringo.  In Proceedings of the Tenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’09), E. Erdem, F. Lin, and T. Schaub, Eds. Lecture Notes in Artificial Intelligence, vol. 5753. Springer-Verlag, 502–508.
  * Gebser et al. (2015) Gebser, M., Kaminski, R., and Schaub, T. 2015\.  Grounding recursive aggregates: Preliminary report.  In Proceedings of the Third Workshop on Grounding, Transforming, and Modularizing Theories with Variables (GTTV’15), M. Denecker and T. Janhunen, Eds.
  * Gebser et al. (2012) Gebser, M., Kaufmann, B., and Schaub, T. 2012\.  Conflict-driven answer set solving: From theory to practice.  Artificial Intelligence 187-188, 52–89.
  * Gebser and Schaub (2016) Gebser, M. and Schaub, T. 2016\.  Modeling and language extensions.  AI Magazine 37, 3, 33–44.
  * Gebser et al. (2007) Gebser, M., Schaub, T., and Thiele, S. 2007\.  Gringo: A new grounder for answer set programming.  See Baral et al. (2007), 266–271.
  * Gelfond and Lifschitz (1988) Gelfond, M. and Lifschitz, V. 1988\.  The stable model semantics for logic programming.  In Proceedings of the Fifth International Conference and Symposium of Logic Programming (ICLP’88), R. Kowalski and K. Bowen, Eds. MIT Press, 1070–1080.
  * Gelfond and Lifschitz (1991) Gelfond, M. and Lifschitz, V. 1991\.  Classical negation in logic programs and disjunctive databases.  New Generation Computing 9, 365–385.
  * Giunchiglia et al. (2006) Giunchiglia, E., Lierler, Y., and Maratea, M. 2006\.  Answer set programming based on propositional satisfiability.  Journal of Automated Reasoning 36, 4, 345–377.
  * Harrison and Lifschitz (2016) Harrison, A. and Lifschitz, V. 2016\.  Stable models for infinitary formulas with extensional atoms.  Theory and Practice of Logic Programming 16, 5-6, 771–786.
  * Harrison et al. (2017) Harrison, A., Lifschitz, V., Pearce, D., and Valverde, A. 2017\.  Infinitary equilibrium logic and strongly equivalent logic programs.  Artificial Intelligence 246, 22–33.
  * Harrison et al. (2014) Harrison, A., Lifschitz, V., and Yang, F. 2014\.  The semantics of gringo and infinitary propositional formulas.  In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’14), C. Baral, G. De Giacomo, and T. Eiter, Eds. AAAI Press.
  * Hill and Warren (2009) Hill, P. and Warren, D., Eds. 2009.  Proceedings of the Twenty-fifth International Conference on Logic Programming (ICLP’09). Lecture Notes in Computer Science, vol. 5649. Springer-Verlag.
  * Janhunen (2001) Janhunen, T. 2001\.  On the effect of default negation on the expressiveness of disjunctive rules.  See Eiter et al. (2001), 93–106.
  * Janhunen et al. (2007) Janhunen, T., Oikarinen, E., Tompits, H., and Woltran, S. 2007\.  Modularity aspects of disjunctive stable models.  See Baral et al. (2007), 175–187.
  * Kaufmann et al. (2016) Kaufmann, B., Leone, N., Perri, S., and Schaub, T. 2016\.  Grounding and solving in answer set programming.  AI Magazine 37, 3, 25–32.
  * Kemp et al. (1991) Kemp, D., Stuckey, P., and Srivastava, D. 1991\.  Magic sets and bottom-up evaluation of well-founded models.  In Logic Programming, Proceedings of the 1991 International Symposium. MIT Press, 337–351.
  * Lefèvre et al. (2017) Lefèvre, C., Béatrix, C., Stéphan, I., and Garcia, L. 2017\.  ASPeRiX, a first-order forward chaining approach for answer set computing.  Theory and Practice of Logic Programming 17, 3, 266–310.
  * Leone et al. (2001) Leone, N., Perri, S., and Scarcello, F. 2001\.  Improving ASP instantiators by join-ordering methods.  See Eiter et al. (2001), 280–294.
  * Leone et al. (2006) Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., and Scarcello, F. 2006\.  The DLV system for knowledge representation and reasoning.  ACM Transactions on Computational Logic 7, 3, 499–562.
  * Lierler and Lifschitz (2009) Lierler, Y. and Lifschitz, V. 2009\.  One more decidable class of finitely ground programs.  See Hill and Warren (2009), 489–493.
  * Lifschitz (2002) Lifschitz, V. 2002\.  Answer set programming and plan generation.  Artificial Intelligence 138, 1-2, 39–54.
  * Lifschitz (2008) Lifschitz, V. 2008\.  Twelve definitions of a stable model.  See Garcia de la Banda and Pontelli (2008), 37–51.
  * Lifschitz and Turner (1994) Lifschitz, V. and Turner, H. 1994\.  Splitting a logic program.  In Proceedings of the Eleventh International Conference on Logic Programming. MIT Press, 23–37.
  * Lin and Zhao (2004) Lin, F. and Zhao, Y. 2004\.  ASSAT: computing answer sets of a logic program by SAT solvers.  Artificial Intelligence 157, 1-2, 115–137.
  * Lukasiewicz (1941) Lukasiewicz, J. 1941\.  Die logik und das grundlagenproblem.  Les Entreties de Zürich sur les Fondaments et la Méthode des Sciences Mathématiques 12, 6-9, 82–100.
  * Martello and Toth (1990) Martello, S. and Toth, P. 1990\.  Knapsack Problems: Algorithms and Computer Implementations.  John Wiley & sons.
  * Mumick et al. (1990) Mumick, I., Pirahesh, H., and Ramakrishnan, R. 1990\.  The magic of duplicates and aggregates.  In Proceedings of the Sixteenth International Conference on Very Large Data Bases (VLDB’90), D. McLeod, R. Sacks-Davis, and H. Schek, Eds. Morgan Kaufmann Publishers, 264–277.
  * Niemelä (2008) Niemelä, I. 2008\.  Answer set programming without unstratified negation.  See Garcia de la Banda and Pontelli (2008), 88–92.
  * Palù et al. (2009) Palù, A. D., Dovier, A., Pontelli, E., and Rossi, G. 2009\.  GASP: Answer set programming with lazy grounding.  Fundamenta Informaticae 96, 3, 297–322.
  * Pelov et al. (2007) Pelov, N., Denecker, M., and Bruynooghe, M. 2007\.  Well-founded and stable semantics of logic programs with aggregates.  Theory and Practice of Logic Programming 7, 3, 301–353.
  * Perri et al. (2007) Perri, S., Scarcello, F., Catalano, G., and Leone, N. 2007\.  Enhancing DLV instantiator by backjumping techniques.  Annals of Mathematics and Artificial Intelligence 51, 2-4, 195–228.
  * Simons et al. (2002) Simons, P., Niemelä, I., and Soininen, T. 2002\.  Extending and implementing the stable model semantics.  Artificial Intelligence 138, 1-2, 181–234.
  * Syrjänen (2001a) Syrjänen, T. 2001a.  Lparse 1.0 user’s manual.
  * Syrjänen (2001b) Syrjänen, T. 2001b.  Omega-restricted logic programs.  See Eiter et al. (2001), 267–279.
  * Tarski (1955) Tarski, A. 1955\.  A lattice-theoretic fixpoint theorem and its applications.  Pacific Journal of Mathematics 5, 285–309.
  * Truszczyński (2012) Truszczyński, M. 2012\.  Connecting first-order ASP and the logic FO(ID) through reducts.  See Erdem et al. (2012), 543–559.
  * Truszczyński (2018) Truszczyński, M. 2018\.  An introduction to the stable and well-founded semantics of logic programs.  In Declarative Logic Programming: Theory, Systems, and Applications, M. Kifer and Y. Liu, Eds. ACM / Morgan & Claypool, 121–177.
  * Turner (2003) Turner, H. 2003\.  Strong equivalence made easy: nested expressions and weight constraints.  Theory and Practice of Logic Programming 3, 4-5, 609–622.
  * Ullman (1988) Ullman, J. 1988\.  Principles of Database and Knowledge-Base Systems.  Computer Science Press.
  * van Emden and Kowalski (1976) van Emden, M. and Kowalski, R. 1976\.  The semantics of predicate logic as a programming language.  Journal of the ACM 23, 4, 733–742.
  * Van Gelder (1993) Van Gelder, A. 1993\.  The alternating fixpoint of logic programs with negation.  Journal of Computer and System Sciences 47, 185–221.
  * Vanbesien et al. (2021) Vanbesien, L., Bruynooghe, M., and Denecker, M. 2021\.  Analyzing semantics of aggregate answer set programming using approximation fixpoint theory.  CoRR abs/2104.14789.
  * Weinzierl et al. (2020) Weinzierl, A., Taupe, R., and Friedrich, G. 2020\.  Advancing lazy-grounding ASP solving techniques — restarts, phase saving, heuristics, and more.  Theory and Practice of Logic Programming 20, 5, 609–624.
  * Wittocx et al. (2010) Wittocx, J., Mariën, M., and Denecker, M. 2010\.  Grounding FO and FO(ID) with bounds.  Journal of Artificial Intelligence Research 38, 223–269.

##  Appendix A Proofs

We use the following reduct-based characterization of strong equivalence
[Turner (2003)].

######  Lemma 41.

Sets $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ of infinitary formulas are
strongly equivalent iff $\mathcal{H}_{1}^{I}$ and $\mathcal{H}_{2}^{I}$ are
classically equivalent for all two-valued interpretations $I$.

###### Proof.

Let $I$ and $J$ be two-valued interpretations, and $\mathcal{H}$ be an
infinitary formula. Clearly, $I\models\mathcal{H}^{J}$ iff $I\cap
J\models\mathcal{H}^{J}$. Thus, we only need to consider interpretations such
that $I\subseteq J$. By Lemma 1 due to halipeva17a, we have that
$I\models\mathcal{H}^{J}$ iff $(I,J)$ is an HT-model of $\mathcal{H}$. The
proposition holds because by Theorem 3 Item (iii) due to halipeva17a, we have
that $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ are strongly equivalent iff they
have the same HT models. ∎

###### Proof of Proposition 2.

Let $F={\\{B(r)\rightarrow H(r)\mid r\in P\\}}^{\wedge}$.

First, we consider the case $I\models F$. By Lemma 1 due to truszczynski12a,
this implies that $P^{I}$ and $F^{I}$ are classically equivalent and thus have
the same minimal models.101010To be precise, Lemma 1 by truszczynski12a is
stated for a set of formulas, which can be understood as an infinitary
conjunction. Thus, $I$ is a stable model of $P$ iff $I$ is a stable model of
$F$.

Second, we consider the case $I\not\models F$ and show that $I$ is neither a
stable model of $F$ nor $P$. Proposition 1 by truszczynski12a states that $I$
is a model of $F$ iff $I$ is a model of $F^{I}$. Thus, $I$ is not a stable
model of $F$. Furthermore, because $I\not\models F$, there is a rule $r\in P$
such that $I\not\models B(r)\rightarrow H(r)$. Consequently, we have $I\models
B(r)$ and $I\not\models H(r)$. Using the above proposition again, we get
$I\models B(r)^{I}$. Because $I\models B(r)^{I}$ and $I\not\models H(r)$, we
get $I\not\models r^{I}$ and in turn $I\not\models P^{I}$. Thus, $I$ is not a
stable model of $P$ either. ∎

######  Lemma 42.

Let $F$ be a formula, and $I$ and $J$ be interpretations.

If $F$ is positive and $I\subseteq J$, then $I\models F$ implies $J\models F$.

###### Proof.

This property can be shown by induction over the rank of the formula. ∎

The following two propositions shed some light on the two types of reducts.

######  Lemma 43.

Let $F$ be a formula, and $I$ and $J$ be interpretations.

Then,

  1. (a)

if $F$ is positive then $F^{I}$ is positive,

  2. (b)

$I\models F$ iff $I\models F^{I}$,

  3. (c)

if $F$ is strictly positive and $I\subseteq J$ then $I\models F$ iff $I\models
F^{J}$.

###### Proof.

###### Property (a).

Because the reduct only replaces subformulas by $\bot$, the resulting formula
is still positive.

###### Property (b).

Corresponds to Proposition 1 by truszczynski12a.

###### Property (c).

This property can be shown by induction over the rank of the formula.∎

######  Lemma 44.

Let $F$ be a formula, and $I$, $J$, and $X$ be interpretations.

Then,

  1. (a)

$F_{I}$ is positive,

  2. (b)

$I\models F$ iff $I\models F_{I}$,

  3. (c)

if $F$ is positive then $F=F_{I}$, and

  4. (d)

if $I\subseteq J$ then $X\models F_{J}$ implies $X\models F_{I}$.

###### Proof.

###### Property (a).

Because the id-reduct replaces all negative occurrences of atoms, the
resulting formula is positive.

###### Property (b).

This property holds because when the reduct replaces an atom $a$, it is
replaced by either $\top$ or $\bot$ depending on whether $I\models a$ or
$I\not\models a$. This does not change the satisfaction of the subformula
w.r.t. $I$.

###### Property (c).

Because a positive formula does not contain negative occurrences of atoms, it
is not changed by the id-reduct.

###### Property (d).

We prove by induction over the rank of formula $F$ that

$\displaystyle X\models F_{J}$ $\displaystyle\text{\ implies\ }X\models
F_{I}\text{\ and}$ (23) $\displaystyle X\models F_{\overline{I}}$
$\displaystyle\text{\ implies\ }X\models F_{\overline{J}}.$ (24)

###### Base.

We consider the case that $F$ is a formula of rank $0$.

$F$ is a formula of rank $0$ implies $F$ is an atom. First, we show (23). We
assume $X\models F_{J}$: $F$ is an atom $\displaystyle\text{\ implies\
}F_{I}=F_{J}=F.$ $\displaystyle F_{I}=F_{J}\text{\ and\ }X\models F_{J}$
$\displaystyle\text{\ implies\ }X\models F_{I}.$ Second, we show (24). We
assume $X\models F_{\overline{I}}$: $\displaystyle\text{$F$ is an atom}\text{\
and\ }X\models F_{\overline{I}}$ $\displaystyle\text{\ implies\
}F_{\overline{I}}=\top.$ $\displaystyle F_{\overline{I}}=\top$
$\displaystyle\text{\ implies\ }F\in I.$ $\displaystyle F\in I\text{\ and\
}I\subseteq J$ $\displaystyle\text{\ implies\ }F\in J.$
$\displaystyle\text{$F$ is an atom}\text{\ and\ }F\in J$ $\displaystyle\text{\
implies\ }F_{\overline{J}}=\top.$ $\displaystyle F_{\overline{J}}=\top$
$\displaystyle\text{\ implies\ }X\models F_{\overline{J}}.$

###### Hypothesis.

We assume that (23) and (24) hold for formulas $F$ of ranks smaller than $i$.

###### Step.

We only show (23) because (24) can be shown in a similar way. We consider
formulas $F$ of rank $i$.

First, we consider the case that $F$ is a conjunction of form
$\mathcal{H}^{\wedge}$.

$\displaystyle X\models\mathcal{H}^{\wedge}_{J}$ $\displaystyle\text{\
implies\ }X\models G_{J}\text{\ for all\ }G\in\mathcal{H}.$ $\displaystyle
X\models G_{J}$ $\displaystyle\text{\ implies\ }X\models G_{I}\text{\ by\
hypothesis}.$ $\displaystyle X\models G_{I}$ $\displaystyle\text{\ implies\
}X\models\mathcal{H}^{\wedge}_{I}.$

The case for disjunctions can be proven in a similar way.

Last, we consider the case that $F$ is an implication of form $G\rightarrow
H$. Observe that  $\displaystyle F_{I}$
$\displaystyle=G_{\overline{I}}\rightarrow H_{I}\text{\ and}$ $\displaystyle
F_{J}$ $\displaystyle=G_{\overline{J}}\rightarrow H_{J}.$ First, we consider
the case $X\not\models G_{\overline{J}}$: $\displaystyle X\not\models
G_{\overline{J}}$ $\displaystyle\text{\ implies\ }X\not\models
G_{\overline{I}}\text{\ by\ hypothesis}.$ $\displaystyle X\not\models
G_{\overline{I}}$ $\displaystyle\text{\ implies\ }X\models F_{I}.$ Second, we
consider the case $X\models H_{J}$: $\displaystyle X\models H_{J}$
$\displaystyle\text{\ implies\ }X\models H_{I}\text{\ by\ hypothesis}.$
$\displaystyle X\models H_{I}$ $\displaystyle\text{\ implies\ }X\models
F_{I}.\qed$

###### Proof of Lemma 6.

This lemma follows from Proposition 14 by dematr00a observing that the well-
founded operator is a monotone symmetric operator. The proposition is actually
a bit more general stating that the operator maps any consistent four-valued
interpretation to a consistent four-valued interpretation. ∎

######  Lemma 45.

Let $O$ and $O^{\prime}$ be monotone operators over complete lattice
$(L,\leq)$ with $O^{\prime}(x)\leq O(x)$ for each $x\in L$.

Then, we get $x^{\prime}\leq x$ where $x^{\prime}$ and $x$ are the least fixed
points of $O^{\prime}$ and $O$, respectively.

###### Proof.

Let $y$ be a prefixed point of $O$. We have $O(y)\leq y$. Because
$O^{\prime}(y)\leq O(y)$, we get $O^{\prime}(y)\leq y$. So each prefixed point
of $O$ is also a prefixed point of $O^{\prime}$.

Let $S^{\prime}$ and $S$ be the set of all prefixed points of $O^{\prime}$ and
$O$, respectively. We obtain $S\subseteq S^{\prime}$. By Theorem 1 (a), we get
that $x^{\prime}$ is the greatest lower bound of $S^{\prime}$. Observe that
$x^{\prime}$ is a lower bound for $S$. By construction of $S$, we have $x\in
S$. Hence, we get $x^{\prime}\leq x$. ∎

######  Lemma 46.

Let $P$ and $P^{\prime}$ be $\mathcal{F}$-programs and $I$ be an
interpretation.

Then, $P^{\prime}\subseteq P$ implies $S_{P^{\prime}}(I)\subseteq S_{P}(I)$.

###### Proof.

This lemma is a direct consequence of Lemma 45 observing that the one-step
provability operator derives fewer consequences for $P^{\prime}$. ∎

######  Lemma 47.

Let $P$ be an $\mathcal{R}$-program, $I$ be a two-valued interpretation, and
$J=S_{P}(I)$.

Then, $X$ is a stable model of $P$, $I\subseteq X$, and $I\subseteq J$ implies
$X\subseteq J$.

###### Proof.

Because $X$ is a stable model of $P$, it is the only minimal model of $P^{X}$.
Furthermore, we have that $J$ is a model of $P_{I}$. To show that $X\subseteq
J$, we show that $J$ is also a model of $P^{X}$. For this, it is enough to
show that for each rule $r\in P$ we have $J\not\models B(r)_{I}$ implies
$J\not\models B(r)^{X}$. We prove inductively over the rank of the formula
$F=B(r)$ that $J\not\models F_{I}$ implies $J\not\models F^{X}$.

###### Base.

We consider the case that $F$ is a formula of rank $0$.

If $X\not\models F$, we get $J\not\models F^{X}$ because $F^{X}=\bot$. Thus,
we only have to consider the case $X\models F$:

$F$ is a formula of rank $0$ implies $F$ is an atom. $F$ is an atom implies
$F_{I}=F$. $\displaystyle X\models F\text{\ and\ }\text{$F$ is an atom}$
$\displaystyle\text{\ implies\ }F^{X}=F.$ $\displaystyle F_{I}=F\text{\ and\
}F^{X}=F$ $\displaystyle\text{\ implies\ }F_{I}=F^{X}.$ $\displaystyle
J\not\models F_{I}\text{\ and\ }F_{I}=F^{X}$ $\displaystyle\text{\ implies\
}J\not\models F^{X}.$

###### Hypothesis.

We assume that $J\not\models F_{I}$ implies $J\not\models F^{X}$ holds for
formulas $F$ of ranks smaller than $i$.

###### Step.

We consider the case that $F$ is a formula of rank $i$.

As in the base case, we only have to consider the case $X\models F$.
Furthermore, we have to distinguish the cases that $F$ is a conjunction,
disjunction, or implication.

We first consider the case that $F$ is a conjunction of form
$\mathcal{F}^{\wedge}$:

$\displaystyle X\models F$ $\displaystyle\text{\ implies\ }F^{X}=\\{{G^{X}\mid
G\in\mathcal{F}\\}}^{\wedge}.$ $\displaystyle J\not\models F_{I}\text{\ and\
}F_{I}={\\{G_{I}\mid G\in\mathcal{F}\\}}^{\wedge}$ $\displaystyle\text{\
implies\ }J\not\models G_{I}\text{\ for some\ }G\in\mathcal{F}.$
$\displaystyle G\in\mathcal{F}\text{\ and\ }\text{$F$ has rank $i$}$ implies
$G$ has rank less than $i$. $\displaystyle J\not\models G_{I}\text{\ and\
}\text{$G$ has rank less than $i$}$ $\displaystyle\text{\ implies\
}J\not\models G^{X}\text{\ by\ hypothesis}.$ $\displaystyle J\not\models
G^{X}\text{\ and\ }F^{X}=\\{{G^{X}\mid G\in F\\}}^{\wedge}$
$\displaystyle\text{\ implies\ }J\not\models F^{X}.$

The case that $F$ is a disjunction can be shown in a similar way to the case
that $F$ is a conjunction.

Last, we consider the case that $F$ is an implication of form $G\rightarrow
H$. Observe that $G$ is positive because $F$ has no occurrences of
implications in its antecedent and, furthermore, given that $F$ is a formula
of rank $i$, $H$ is a formula of rank less than $i$.

We show $I\models G$:

$\displaystyle J\not\models F_{I}\text{\ and\
}F_{I}=G_{\overline{I}}\rightarrow H_{I}$ $\displaystyle\text{\ implies\
}J\models G_{\overline{I}}$ $\displaystyle J\models G_{\overline{I}}\text{\
and\ }\text{$G$ is positive}$ $\displaystyle\text{\ implies\ }I\models
G\text{\ because\ }G_{\overline{I}}\equiv\top.$ We show $J\models G^{X}$:
$\displaystyle\text{$G$ is positive}\text{,\ }I\subseteq X\text{, and\
}I\models G$ $\displaystyle\text{\ implies\ }X\models G\text{\ by\
\lx@cref{creftype~refnum}{lem:monotone-positive}.}$ $\displaystyle X\models
F\text{,\ }X\models G\text{, and\ }F=G\rightarrow H$ $\displaystyle\text{\
implies\ }X\models H\text{.}$ $\displaystyle\text{$G$ is positive}\text{,\
}I\subseteq X\text{, and\ }I\models G$ $\displaystyle\text{\ implies\
}I\models G^{X}\text{\ by\ \lx@cref{creftypecap~refnum}{lem:ferraris-
basic}~{}\ref{lem:ferraris-basic:d}.}$ $G$ is positive implies $G^{X}$ is
positive by Lemma 43 (a). $\displaystyle G^{X}\text{\ is positive}\text{,\
}I\subseteq J\text{, and\ }I\models G^{X}$ $\displaystyle\text{\ implies\
}J\models G^{X}\text{\ by\ \lx@cref{creftype~refnum}{lem:monotone-positive}.}$
We show $J\not\models H^{X}$: $\displaystyle I\models G\text{\ and\
}F_{I}=G_{\overline{I}}\rightarrow H_{I}$ $\displaystyle\text{\ implies\
}F_{I}\equiv H_{I}\text{\ because\ }G_{\overline{I}}\equiv\top.$
$\displaystyle F_{I}\equiv H_{I}\text{\ and\ }J\not\models F_{I}$
$\displaystyle\text{\ implies\ }J\not\models H_{I}.$ $\displaystyle
J\not\models H_{I}\text{\ and\ $H$ has rank less than $i$}$
$\displaystyle\text{\ implies\ }J\not\models H^{X}\text{\ by hypothesis.}$

Because $X\models F$, we have $F^{X}=G^{X}\rightarrow H^{X}$. Using $J\models
G^{X}$ and $J\not\models H^{X}$, we get $J\not\models F^{X}$.∎

###### Proof of Theorem 7.

Let $X$ be a stable model of $P$.

We prove by transfinite induction over the sequence of postfixed points
leading to the well-founded model:

$\displaystyle(I_{0},J_{0})$ $\displaystyle=(\emptyset,\Sigma),$
$\displaystyle(I_{\alpha+1},J_{\alpha+1})$
$\displaystyle=W_{P}(I_{\alpha},J_{\alpha})\text{\ for ordinals
$\alpha$},\text{\ and\ }$ $\displaystyle(I_{\beta},J_{\beta})$
$\displaystyle=(\bigcup_{\alpha<\beta}I_{\alpha},\bigcap_{\alpha<\beta}J_{\alpha})\text{\
for limit ordinals $\beta$.}$

We have that $\alpha<\beta$ implies
$(I_{\alpha},J_{\alpha})\leq_{p}(I_{\beta},J_{\beta})$ for ordinals $\alpha$
and $\beta$, $I_{\alpha}\subseteq J_{\alpha}$ for ordinals $\alpha$, and there
is a least ordinal $\alpha$ such that $(I,J)=(I_{\alpha},J_{\alpha})$.

###### Base.

We have $I_{0}\subseteq X\subseteq J_{0}$.

###### Hypothesis.

We assume $I_{\beta}\subseteq X\subseteq J_{\beta}$ for all ordinals
$\beta<\alpha$.

###### Step.

If $\alpha=\beta+1$ is a successor ordinal we have

$\displaystyle(I_{\alpha},J_{\alpha})$
$\displaystyle=W_{P}(I_{\beta},J_{\beta})$
$\displaystyle=(S_{P}(J_{\beta}),S_{P}(I_{\beta})).$

By the induction hypothesis we have $I_{\beta}\subseteq X\subseteq J_{\beta}$.

First, we show $I_{\alpha}\subseteq X$:

$X$ is a (stable) model $\displaystyle\text{\ implies\ }S_{P}(X)\subseteq X.$
$\displaystyle X\subseteq J_{\beta}$ $\displaystyle\text{\ implies\
}S_{P}(J_{\beta})\subseteq S_{P}(X).$ $\displaystyle S_{P}(X)\subseteq
X\text{\ and\ }S_{P}(J_{\beta})\subseteq S_{P}(X)$ $\displaystyle\text{\
implies\ }S_{P}(J_{\beta})\subseteq X.$ $\displaystyle
I_{\alpha}=S_{P}(J_{\beta})\text{\ and\ }S_{P}(J_{\beta})\subseteq X$
$\displaystyle\text{\ implies\ }I_{\alpha}\subseteq X.$

Second, we show $X\subseteq J_{\alpha}$:

$\displaystyle\beta<\alpha$ $\displaystyle\text{\ implies\
}(I_{\beta},J_{\beta})\leq_{p}(I_{\alpha},J_{\alpha})$
$\displaystyle(I_{\beta},J_{\beta})\leq_{p}(I_{\alpha},J_{\alpha})\text{\ and\
}I_{\alpha}\subseteq J_{\alpha}$ $\displaystyle\text{\ implies\
}I_{\beta}\subseteq J_{\alpha}$ $X$ is a stable model, $I_{\beta}\subseteq X$,
$J_{\alpha}=S_{P}(I_{\beta})$, and $I_{\beta}\subseteq J_{\alpha}$
$\displaystyle\text{\ implies\ }\text{$X\subseteq J_{\alpha}$ by
\lx@cref{creftype~refnum}{lem:stable:possible}}.$

We have shown $I_{\alpha}\subseteq X\subseteq J_{\alpha}$ for successor
ordinals.

If $\alpha$ is a limit ordinal we have

$\displaystyle(I_{\alpha},J_{\alpha})$
$\displaystyle=(\bigcup_{\beta<\alpha}I_{\beta},\bigcap_{\beta<\alpha}J_{\beta}).$

Let $x\in I_{\alpha}$. There must be an ordinal $\beta<\alpha$ such that $x\in
I_{\beta}$. Since $I_{\beta}\subseteq X$ by the hypothesis, we have $x\in X$.
Thus, $I_{\alpha}\subseteq X$.

Let $x\in X$. For each ordinal $\beta<\alpha$ we have $x\in J_{\beta}$ because
$X\subseteq J_{\beta}$ by the hypothesis. Thus, we get $x\in J_{\alpha}$. It
follows that $X\subseteq J_{\alpha}$.

We have shown $I_{\alpha}\subseteq X\subseteq J_{\alpha}$ for limit ordinals.∎

######  Lemma 48.

Let $P$ be an $\mathcal{F}$-program and $(I,J)$ be a four-valued
interpretation.

Then, we have $H(P^{I,J})=T_{P_{I}}(J)$.

###### Proof.

The program $P^{I,J}$ contains all rules $r\in P$ such that $J\models
B(r)_{I}$. This are exactly the rules whose heads are gathered by the $T$
operator. ∎

######  Lemma 49.

Let $P$ be an $\mathcal{F}$-program and $(I,J)$ be the well-founded model of
$P$.

Then, we have

  1. (a)

$S_{P^{I,J}}(I^{\prime})=J$ for all $I^{\prime}\subseteq I$, and

  2. (b)

$S_{P^{I,J}}(J^{\prime})=S_{P}(J^{\prime})$ for all $J\subseteq J^{\prime}$.

###### Proof.

Throughout the proof we use

$\displaystyle S_{P}(J)$ $\displaystyle=I,$ $\displaystyle S_{P}(I)$
$\displaystyle=J,$ $\displaystyle P^{I,J}$ $\displaystyle\subseteq P\text{,
and}$ $\displaystyle I$ $\displaystyle\subseteq J\text{\ because the well-
founded model is consistent.}$

###### Property (a).

We show $J=S_{P^{I,J}}(I)$. Let $\hat{J}=S_{P^{I,J}}(I)$ and $r\in P\setminus
P^{I,J}$:

$\displaystyle P^{I,J}\subseteq P$ and $\displaystyle\hat{J}=S_{P^{I,J}}(I)$
and $\displaystyle J=S_{P}(I)$ $\displaystyle\text{\ implies\
}\hat{J}\subseteq J\text{\ by
\lx@cref{creftype~refnum}{lem:program:positive:subset}.}$ $\displaystyle
r\notin P^{I,J}$ $\displaystyle\text{\ implies\ }J\not\models B(r)_{I}.$
$\displaystyle\hat{J}\subseteq J\text{\ and\ }J\not\models B(r)_{I}$
$\displaystyle\text{\ implies\ }\hat{J}\not\models B(r)_{I}\text{\ by
\lx@cref{creftype~refnum}{lem:monotone-positive}.}$
$\displaystyle\hat{J}=S_{P^{I,J}}(I)\text{\ and\ }\hat{J}\not\models B(r)_{I}$
$\displaystyle\text{\ implies\ }\hat{J}\models P_{I}.$
$\displaystyle\hat{J}\models P_{I}\text{\ and\ }J=S_{P}(I)$
$\displaystyle\text{\ implies\ }J\subseteq\hat{J}.$ $\displaystyle
J\subseteq\hat{J}\text{\ and\ }\hat{J}\subseteq J$ $\displaystyle\text{\
implies\ }J=\hat{J}.$

Thus, we get that $S_{P^{I,J}}(I)=J$.

With this we can continue to prove $S_{P^{I,J}}(I^{\prime})=J$. Let $r\in
P^{I,J}$:

$\displaystyle r\in P^{I,J}$ $\displaystyle\text{\ implies\ }J\models
B(r)_{I}.$ $\displaystyle r\in P^{I,J}\text{\ and\ }P^{I,J}\subseteq P$
$\displaystyle\text{\ implies\ }r\in P.$ $\displaystyle J\models
B(r)_{I}\text{,\ }r\in P,\text{\ and\ }S_{P}(I)=J$ $\displaystyle\text{\
implies\ }H(r)\in J.$ $\displaystyle J\models B(r)_{I}\text{\ and\
}I^{\prime}\subseteq I$ $\displaystyle\text{\ implies\ }J\models
B(r)_{I^{\prime}}\text{\ by \lx@cref{creftypecap~refnum}{lem:foid-
basic}~{}\ref{lem:foid-basic:d}.}$ $\displaystyle H(r)\in J\text{\ and\
}J\models B(r)_{I^{\prime}}$ $\displaystyle\text{\ implies\
}S_{P^{I,J}}(I^{\prime})\subseteq J.$ $\displaystyle I^{\prime}\subseteq
I\text{\ and\ }J=S_{P^{I,J}}(I)$ $\displaystyle\text{\ implies\ }J\subseteq
S_{P^{I,J}}(I^{\prime}).$

Thus, we get $S_{P^{I,J}}(I^{\prime})=J$.

###### Property (b).

Let $I^{\prime}=S_{P^{I,J}}(J^{\prime})$ and $r\in P\setminus P^{I,J}$:

$\displaystyle r\notin P^{I,J}$ $\displaystyle\text{\ implies\ }J\not\models
B(r)_{I}.$ $\displaystyle I\subseteq J\text{,\ }J\subseteq J^{\prime}\text{,
and\ }J\not\models B(r)_{I}$ $\displaystyle\text{\ implies\ }J\not\models
B(r)_{J^{\prime}}.\text{\ by \lx@cref{creftypecap~refnum}{lem:foid-
basic}~{}\ref{lem:foid-basic:d}.}.$ $\displaystyle I^{\prime}\subseteq
I\text{,\ }I\subseteq J\text{, and\ }J\not\models B(r)_{J^{\prime}}$
$\displaystyle\text{\ implies\ }I^{\prime}\not\models
B(r)_{J^{\prime}}.\text{\ by \lx@cref{creftype~refnum}{lem:monotone-
positive}.}$ $\displaystyle I^{\prime}=S_{P^{I,J}}(J^{\prime})\text{\ and\
}I^{\prime}\not\models B(r)_{J^{\prime}}$ $\displaystyle\text{\ implies\
}S_{P}(J^{\prime})\subseteq S_{P^{I,J}}(J^{\prime}).$ $\displaystyle
P^{I,J}\subseteq P$ $\displaystyle\text{\ implies\
}S_{P^{I,J}}(J^{\prime})\subseteq S_{P}(J^{\prime})\text{\ by
\lx@cref{creftype~refnum}{lem:program:positive:subset}.}$

Thus, we get $S_{P^{I,J}}(J^{\prime})=S_{P}(J^{\prime})$.∎

###### Proof of Theorem 8.

By Lemma 49, we have $(I,J)=W_{P^{I,J}}(I,J)$. Furthermore, we let
$(\widehat{I},\widehat{J})=\mathit{WM}(P^{I,J})$:

$\displaystyle(\widehat{I},\widehat{J})=\mathit{WM}(P^{I,J})\text{\ and\
}(I,J)=W_{P^{I,J}}(I,J)$ $\displaystyle\text{\ implies\
}(\widehat{I},\widehat{J})\leq_{p}(I,J).$ by Theorem 1 (c).
$\displaystyle\widehat{I}\subseteq I$ $\displaystyle\text{\ implies\
}S_{P^{I,J}}(\widehat{I})=S_{P^{I,J}}(I)$ by Lemma 49 (a).
$\displaystyle\hat{J}=S_{P^{I,J}}(\widehat{I})=S_{P^{I,J}}(I)=J$
$\displaystyle\text{\ implies\ }\widehat{J}=J.$
$\displaystyle\widehat{I}=S_{P^{I,J}}(\widehat{J})\text{,\
}S_{P^{I,J}}(J)=I\text{, and\ }\widehat{J}=J$ $\displaystyle\text{\ implies\
}\widehat{I}=I.$

We obtain $(I,J)=(\widehat{I},\widehat{J})$. ∎

###### Proof of Theorem 9.

We first show that all rule bodies removed by the simplification are falsified
by $X$. Let $r\in P\setminus P^{I,J}$ and assume $X\models{B(r)}$:

$\displaystyle X\models B(r)$ $\displaystyle\text{\ implies\ }X\models
B(r)_{X}\text{\ by\ \lx@cref{creftypecap~refnum}{lem:foid-
basic}~{}\ref{lem:foid-basic:b}}.$ $\displaystyle X\models B(r)_{X}\text{\
and\ }I\subseteq X$ $\displaystyle\text{\ implies\ }X\models B(r)_{I}\text{\
by\ \lx@cref{creftypecap~refnum}{lem:foid-basic}~{}\ref{lem:foid-basic:d}}.$
$\displaystyle X\models B(r)_{I}\text{\ and\ }X\subseteq J$
$\displaystyle\text{\ implies\ }J\models B(r)_{I}\text{\ by\
\lx@cref{creftype~refnum}{lem:monotone-positive}}.$ This is a contradiction
and, thus, $X\not\models B(r)$. We use the following consequence in the proof
below: $\displaystyle X\not\models B(r)$ $\displaystyle\text{\ implies\
}{(P\setminus P^{I,J})}^{X}\equiv\emptyset.$

To show the theorem, we show that $P^{X}$ and ${(P^{I,J})}^{X}$ have the same
minimal models. Clearly, we have $P^{X}={(P^{I,J})}^{X}\cup{(P\setminus
P^{I,J})}^{X}$. Using this and ${(P\setminus P^{I,J})}^{X}\equiv\emptyset$, we
obtain that $P^{X}$ and ${(P^{I,J})}^{X}$ have the same minimal models. ∎

###### Proof of Corollary 10.

The result follows from Theorems 9, 8 and 7. ∎

###### Proof of Theorem 11.

By Lemma 46, we have $S_{P^{I,J}}(X)\subseteq S_{Q}(X)\subseteq S_{P}(X)$ for
any two-valued interpretation $X$. Thus, by Theorem 8, we get
$(I,J)=W_{Q}(I,J)$.

Let $(\widehat{I},\widehat{J})$ be a prefixed point of $W_{Q}$ with
$(\widehat{I},\widehat{J})\leq_{p}(I,J)$. We have
$(S_{Q}(\widehat{J}),S_{Q}(\widehat{I}))\leq_{p}(\widehat{I},\widehat{J})\leq_{p}(I,J)$.

$\displaystyle J\subseteq\widehat{J}$ $\displaystyle\text{\ implies\
}S_{P^{I,J}}(\widehat{J})=S_{Q}(\widehat{J})=S_{P}(\widehat{J})$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{prp:simplification:well-
founded}~{}\ref{prp:simplification:well-founded:b}}.$ $\displaystyle
S_{Q}(\widehat{J})=S_{P}(\widehat{J})\text{\ and\
}S_{Q}(\widehat{J})\subseteq\widehat{I}$ $\displaystyle\text{\ implies\
}S_{P}(\widehat{J})\subseteq\widehat{I}.$ $\displaystyle\widehat{J}\subseteq
S_{Q}(\widehat{I})\text{\ and\ }S_{Q}(\widehat{I})\subseteq
S_{P}(\widehat{I})$ $\displaystyle\text{\ implies\ }\widehat{J}\subseteq
S_{P}(\widehat{I}).$ $\displaystyle
S_{P}(\widehat{J})\subseteq\widehat{I}\text{\ and\ }\widehat{J}\subseteq
S_{P}(\widehat{I})$ $\displaystyle\text{\ implies\
}W_{P}(\widehat{I},\widehat{J})\leq_{p}(\widehat{I},\widehat{J}).$
$\displaystyle
W_{P}(\widehat{I},\widehat{J})\leq_{p}(\widehat{I},\widehat{J})$
$\displaystyle\text{\ implies\ }(I,J)\leq_{p}(\widehat{I},\widehat{J})$
$\displaystyle\text{\ by\ \lx@cref{creftypecap~refnum}{thm:knaster-
tarski}~{}\ref{thm:knaster-tarski:a}}.$
$\displaystyle(I,J)\leq_{p}(\widehat{I},\widehat{J})\text{\ and\
}(\widehat{I},\widehat{J})\leq_{p}(I,J)$ $\displaystyle\text{\ implies\
}(I,J)=(\widehat{I},\widehat{J}).$

By Theorem 1 (a), we obtain that $\mathit{WM}(Q)=(I,J)$. ∎

###### Proof of Corollary 12.

Observe that $P^{I,J}=Q^{I,J}$. With this, the corollary follows from
Corollaries 10 and 11. ∎

Alternatively, the incorporation of context atoms can also be seen as a form
of partial evaluation applied to the underlying program.

######  Definition 22.

Let $\mathit{I\\!C}$ be a two-valued interpretation.

We define the _partial evaluation_ of an $\mathcal{F}$-formula w.r.t.
$\mathit{I\\!C}$ as follows:

$\displaystyle\mathit{pe}_{\mathit{I\\!C}}({a})$ $\displaystyle=\top\text{\ if
}a\in\mathit{I\\!C}$
$\displaystyle\mathit{pe}_{\overline{\mathit{I\\!C}}}({a})$ $\displaystyle=a$
$\displaystyle\mathit{pe}_{\mathit{I\\!C}}({a})$ $\displaystyle=a\text{\ if
}a\notin\mathit{I\\!C}$
$\displaystyle\mathit{pe}_{\mathit{I\\!C}}({\mathcal{H}^{\wedge}})$
$\displaystyle={\\{\mathit{pe}_{\mathit{I\\!C}}({F})\mid
F\in\mathcal{H}\\}}^{\wedge}$
$\displaystyle\mathit{pe}_{\overline{\mathit{I\\!C}}}({\mathcal{H}^{\wedge}})$
$\displaystyle={\\{\mathit{pe}_{\overline{\mathit{I\\!C}}}({F})\mid
F\in\mathcal{H}\\}}^{\wedge}$
$\displaystyle\mathit{pe}_{\mathit{I\\!C}}({\mathcal{H}^{\vee}})$
$\displaystyle={\\{\mathit{pe}_{\mathit{I\\!C}}({F})\mid
F\in\mathcal{H}\\}}^{\vee}$
$\displaystyle\mathit{pe}_{\overline{\mathit{I\\!C}}}({\mathcal{H}^{\vee}})$
$\displaystyle={\\{\mathit{pe}_{\overline{\mathit{I\\!C}}}({F})\mid
F\in\mathcal{H}\\}}^{\vee}$
$\displaystyle\mathit{pe}_{\mathit{I\\!C}}({F\rightarrow G})$
$\displaystyle=\mathit{pe}_{\overline{\mathit{I\\!C}}}({F})\rightarrow\mathit{pe}_{\mathit{I\\!C}}({G})$
$\displaystyle\mathit{pe}_{\overline{\mathit{I\\!C}}}({F\rightarrow G})$
$\displaystyle=\mathit{pe}_{\mathit{I\\!C}}({F})\rightarrow\mathit{pe}_{\overline{\mathit{I\\!C}}}({G})$

where $a$ is an atom, $\mathcal{H}$ a set of formulas, and $F$ and $G$ are
formulas.

The partial evaluation of an $\mathcal{F}$-program $P$ w.r.t. a two-valued
interpretation $\mathit{I\\!C}$ is
$\mathit{pe}_{\mathit{I\\!C}}({P})=\\{\mathit{pe}_{\mathit{I\\!C}}({r})\mid
r\in P\\}$ where
$\mathit{pe}_{\mathit{I\\!C}}({r})=H(h)\leftarrow\mathit{pe}_{\mathit{I\\!C}}({B(r)})$.
Accordingly, the partial evaluation of rules boils down to replacing satisfied
positive occurrences of atoms in rule bodies by $\top$.

We observe the following relationship between the relative one-step operators
and partial evaluations.

######  Observation 50.

Let $P$ be a positive $\mathcal{F}$-program and $\mathit{I\\!C}$ be a two-
valued interpretation.

Then, we have for any two-valued interpretation $I$ that

$\displaystyle T_{P}^{\mathit{I\\!C}}(I)$
$\displaystyle=T_{\mathit{pe}_{\mathit{I\\!C}}({P})}(I).$

Note that
${\mathit{pe}_{\mathit{I\\!C}}({P})_{J}}={\mathit{pe}_{\mathit{I\\!C}}({P_{J}})}$.

###### Proof of Proposition 13.

Clearly, $\mathit{pe}_{\mathit{I\\!C}}({P})$ is positive whenever $P$ is
positive. Using 50, we obtain that $T_{P}^{\mathit{I\\!C}}$ is monotone.

The second property directly follows from the monotonicity of the one-step
provability operator. ∎

######  Lemma 51.

Let $P$ be an $\mathcal{F}$-program and $\mathit{I\\!C}$ be a two-valued
interpretation.

For any two-valued interpretation $J$, we get

$\displaystyle S_{P}^{\mathit{I\\!C}}(J)$
$\displaystyle=\mathit{LM}(\mathit{pe}_{\mathit{I\\!C}}({P})_{J}).$

###### Proof.

This lemma immediately follows from 50. ∎

###### Proof of Proposition 14.

Both properties can be shown by inspecting the reduced programs.

###### Property $J^{\prime}\subseteq J$ implies
$S_{P}^{\mathit{I\\!C}}(J)\subseteq S_{P}^{\mathit{I\\!C}}(J^{\prime})$.

Observe that we can use Lemma 51 to equivalently write
$S_{P}^{\mathit{I\\!C}}(J)=S_{\mathit{pe}_{\mathit{I\\!C}}({P})}(J)$ and
$S_{P}^{\mathit{I\\!C}}(J^{\prime})=S_{\mathit{pe}_{\mathit{I\\!C}}({P})}(J^{\prime})$.
With this and Proposition 4, we see that the relative stable operator is
antimonotone just as the stable operator.

###### Property $\mathit{I\\!C}^{\prime}\subseteq\mathit{I\\!C}$ implies
$S_{P}^{\mathit{I\\!C}^{\prime}}(J)\subseteq S_{P}^{\mathit{I\\!C}}(J)$.

Observe that $S_{P}^{\mathit{I\\!C}}(J)$ is equal to the least fixed point of
$T_{P_{J}}^{\mathit{I\\!C}}$ and $S_{P}^{\mathit{I\\!C}^{\prime}}(J)$ is equal
to the least fixed point of $T_{P_{J}}^{\mathit{I\\!C}^{\prime}}$.
Furthermore, observe that $T_{P_{J}}^{\mathit{I\\!C}^{\prime}}(X)\subseteq
T_{P_{J}}^{\mathit{I\\!C}}(X)$ for any two-valued interpretation $X$ because
$\mathit{I\\!C}^{\prime}\subseteq\mathit{I\\!C}$ and the underlying $T$
operator is monotone. With this and Lemma 45, we have shown the property.∎

######  Observation 52.

Let $P$ be an $\mathcal{F}$-program, and $\mathit{I\\!C}$ and $J$ be two-
valued interpretations.

We get the following properties:

  1. (a)

$S_{P}^{\emptyset}(J)=S_{P}(J)$,

  2. (b)

$S_{P}^{\mathit{I\\!C}}(J)\subseteq H(P)$, and

  3. (c)

$S_{P}^{\mathit{I\\!C}}(J)=S_{P}^{\mathit{I\\!C}\cap{B(P)}^{+}}(J\cap{B(P)}^{-})$.

###### Proof of Proposition 15.

Both properties can be shown by using the monotonicity of the underlying
relative stable operator:

###### Property $(I^{\prime},J^{\prime})\leq_{p}(I,J)$ implies
$W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(I^{\prime},J^{\prime})\leq_{p}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(I,J)$.

Given that $S_{P}^{\mathit{I\\!C}}$ is antimonotone and
$J^{\prime}\cup\mathit{J\\!C}\subseteq J\cup\mathit{J\\!C}$, we have
$S_{P}^{\mathit{I\\!C}}(J\cup\mathit{J\\!C})\subseteq
S_{P}^{\mathit{I\\!C}}(J^{\prime}\cup\mathit{J\\!C})$. Analogously, we can
show $S_{P}^{\mathit{J\\!C}}(I^{\prime}\cup\mathit{I\\!C})\subseteq
S_{P}^{\mathit{J\\!C}}(I\cup\mathit{I\\!C})$. We get
$(S_{P}^{\mathit{I\\!C}}(J\cup\mathit{J\\!C}),S_{P}^{\mathit{J\\!C}}(I\cup\mathit{I\\!C}))\leq_{p}(S_{P}^{\mathit{I\\!C}}(J^{\prime}\cup\mathit{J\\!C}),S_{P}^{\mathit{J\\!C}}(I^{\prime}\cup\mathit{I\\!C}))$.

Hence, $W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}$ is monotone.

###### Property
$(\mathit{I\\!C}^{\prime},\mathit{J\\!C}^{\prime})\leq_{p}(\mathit{I\\!C},\mathit{J\\!C})$
implies
$W_{P}^{\mathit{I\\!C}^{\prime},\mathit{J\\!C}^{\prime}}(I,J)\leq_{p}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(I,J)$.

We have to show
$(S_{P}^{\mathit{I\\!C}^{\prime}}(J\cup\mathit{J\\!C}^{\prime}),S_{P}^{\mathit{J\\!C}^{\prime}}(I\cup\mathit{I\\!C}^{\prime}))\leq_{p}(S_{P}^{\mathit{I\\!C}}(J\cup\mathit{J\\!C}),\allowbreak
S_{P}^{\mathit{J\\!C}}(I\cup\mathit{I\\!C}))$.

Given that $\mathit{I\\!C}^{\prime}\subseteq\mathit{I\\!C}$ and
$J\cup\mathit{J\\!C}\subseteq J\cup\mathit{J\\!C}^{\prime}$, we obtain
$S_{P}^{\mathit{I\\!C}^{\prime}}(J\cup\mathit{J\\!C}^{\prime})\subseteq
S_{P}^{\mathit{I\\!C}}(J\cup\mathit{J\\!C})$ using Proposition 14. The same
argument can be used for the possible atoms of the four-valued
interpretations. Given that $\mathit{J\\!C}\subseteq\mathit{J\\!C}^{\prime}$
and $I\cup\mathit{I\\!C}^{\prime}\subseteq I\cup\mathit{I\\!C}$, we obtain
$S_{P}^{\mathit{J\\!C}}(I\cup\mathit{I\\!C})\subseteq
S_{P}^{\mathit{J\\!C}^{\prime}}(I\cup\mathit{I\\!C}^{\prime})$ using
Proposition 14.

Hence, we have shown
$W_{P}^{\mathit{I\\!C}^{\prime},\mathit{J\\!C}^{\prime}}(I,J)\leq_{p}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(I,J)$.∎

######  Observation 53.

Let $P$ be an $\mathcal{F}$-program, and $I$, $I^{\prime}$ and
$\mathit{I\\!C}$ be two-valued interpretations.

We get the following properties:

  1. (a)

$I\models P$ and $\mathit{I\\!C}\subseteq I$ implies
$I\models\mathit{pe}_{\mathit{I\\!C}}({P})$,

  2. (b)

$I\models\mathit{pe}_{\mathit{I\\!C}}({P})$ and $I^{\prime}\cap
B(P)^{+}\subseteq\mathit{I\\!C}$ implies $I\cup
I^{\prime}\models\mathit{pe}_{\mathit{I\\!C}}({P})$, and

  3. (c)

$I\models\mathit{pe}_{\mathit{I\\!C}}({P})$ implies $I\models P$.

######  Lemma 54.

Let $\mathit{P\\!B}$ and $\mathit{P\\!T}$ be $\mathcal{F}$-programs,
$\mathit{I\\!C}$ and $J$ be two-valued interpretations,
$I=S_{\mathit{P\\!B}\cup\mathit{P\\!T}}^{\mathit{I\\!C}}(J)$,
$\mathit{I\\!E}=I\cap({B(\mathit{P\\!B})}^{+}\cap H(\mathit{P\\!T}))$,
$\mathit{I\\!B}=S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(J)$, and
${\mathit{I\\!T}}=S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\mathit{I\\!B}}(J)$.

Then, we have $I=\mathit{I\\!B}\cup{\mathit{I\\!T}}$.

###### Proof.

Let $\widetilde{I}=\mathit{I\\!B}\cup{\mathit{I\\!T}}$. Furthermore, we use
the following programs:

$\displaystyle\widehat{\mathit{P\\!B}}$
$\displaystyle=\mathit{pe}_{\mathit{I\\!C}}({\mathit{P\\!B}_{J}})$
$\displaystyle\widetilde{\mathit{P\\!B}}$
$\displaystyle=\mathit{pe}_{\mathit{I\\!C}\cup\mathit{I\\!E}}({\mathit{P\\!B}_{J}})=\mathit{pe}_{\mathit{I\\!E}}({\widehat{\mathit{P\\!B}}})$
$\displaystyle\widehat{\mathit{P\\!T}}$
$\displaystyle=\mathit{pe}_{\mathit{I\\!C}}({\mathit{P\\!T}_{J}})$
$\displaystyle\widetilde{\mathit{P\\!T}}$
$\displaystyle=\mathit{pe}_{\mathit{I\\!C}\cup\mathit{I\\!B}}({\mathit{P\\!T}_{J}})=\mathit{pe}_{\mathit{I\\!B}}({\widehat{\mathit{P\\!T}}})$

Observe that

$\displaystyle I$
$\displaystyle=S_{\mathit{P\\!B}\cup\mathit{P\\!T}}^{\mathit{I\\!C}}(J)=\mathit{LM}(\widehat{\mathit{P\\!B}}\cup\widehat{\mathit{P\\!T}}),$
$\displaystyle\mathit{I\\!B}$
$\displaystyle=S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(J)=\mathit{LM}(\widetilde{\mathit{P\\!B}})\text{,
and}$ $\displaystyle\mathit{I\\!T}$
$\displaystyle=S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\mathit{I\\!B}}(J)=\mathit{LM}(\widetilde{\mathit{P\\!T}}).$

To show that $\widetilde{I}\subseteq I$, we show that $I$ is a model of both
$\widetilde{\mathit{P\\!B}}$ and $\widetilde{\mathit{P\\!T}}$. To show that
$I\subseteq\widetilde{I}$, we show that $\widetilde{I}$ is a model of both
$\widehat{\mathit{P\\!B}}$ and $\widehat{\mathit{P\\!T}}$.

###### Property $I\models\widetilde{\mathit{P\\!B}}$.

$\displaystyle
I=\mathit{LM}(\widehat{\mathit{P\\!B}}\cup\widehat{\mathit{P\\!T}})$
$\displaystyle\text{\ implies\ }I\models\widehat{\mathit{P\\!B}}.$
$\displaystyle I\models\widehat{\mathit{P\\!B}}\text{\ and\
}\mathit{I\\!E}\subseteq I$ $\displaystyle\text{\ implies\
}I\models\widetilde{\mathit{P\\!B}}$ $\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:a}}.$

###### Property $I\models\widetilde{\mathit{P\\!T}}$.

$\displaystyle
I=\mathit{LM}(\widehat{\mathit{P\\!B}}\cup\widehat{\mathit{P\\!T}})$
$\displaystyle\text{\ implies\ }I\models\widehat{\mathit{P\\!T}}.$
$\displaystyle I\models\widetilde{\mathit{P\\!B}}\text{\ and\
}\mathit{I\\!B}=\mathit{LM}(\widetilde{\mathit{P\\!B}})$ $\displaystyle\text{\
implies\ }\mathit{I\\!B}\subseteq I.$ $\displaystyle
I\models\widehat{\mathit{P\\!T}}\text{\ and\ }\mathit{I\\!B}\subseteq I$
$\displaystyle\text{\ implies\ }I\models\widetilde{\mathit{P\\!T}}.$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:a}}.$

###### Property $\widetilde{I}\models\widehat{\mathit{P\\!B}}$.

Let $E={B(\mathit{P\\!B})}^{+}\cap H(\mathit{P\\!T})$:

$\displaystyle\widetilde{I}\subseteq I\text{\ and\ }\mathit{I\\!E}=I\cap E$
$\displaystyle\text{\ implies\ }\mathit{I\\!T}\cap E\subseteq\mathit{I\\!E}.$
$\displaystyle\mathit{I\\!T}=\mathit{LM}(\widetilde{\mathit{P\\!T}})$
$\displaystyle\text{\ implies\ }\mathit{I\\!T}\subseteq
H(\widetilde{\mathit{P\\!T}}).$ $\displaystyle\mathit{I\\!T}\cap
E\subseteq\mathit{I\\!E}\text{\ and\ }\mathit{I\\!T}\subseteq
H(\widetilde{\mathit{P\\!T}})$ $\displaystyle\text{\ implies\
}\mathit{I\\!T}\cap{B(\mathit{P\\!B})}^{+}\subseteq\mathit{I\\!E}.$
$\displaystyle\mathit{I\\!T}\cap{B(\mathit{P\\!B})}^{+}\subseteq\mathit{I\\!E}$
$\displaystyle\text{\ implies\
}\mathit{I\\!T}\cap{B(\widehat{\mathit{P\\!B}})}^{+}\subseteq\mathit{I\\!E}.$
$\displaystyle\mathit{I\\!T}\cap{B(\widehat{\mathit{P\\!B}})}^{+}\subseteq\mathit{I\\!E}\text{\
and\ }\mathit{I\\!B}=\mathit{LM}(\widetilde{\mathit{P\\!B}})$
$\displaystyle\text{\ implies\
}\widetilde{I}\models\widetilde{\mathit{P\\!B}}$ $\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:b}}.$
$\displaystyle\widetilde{I}\models\widetilde{\mathit{P\\!B}}$
$\displaystyle\text{\ implies\ }\widetilde{I}\models\widehat{\mathit{P\\!B}}$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:c}}.$

###### Property $\widetilde{I}\models\widehat{\mathit{P\\!T}}$.

$\displaystyle\mathit{I\\!T}=\mathit{LM}(\widetilde{\mathit{P\\!T}})$
$\displaystyle\text{\ implies\
}\widetilde{I}\models\widetilde{\mathit{P\\!T}}$ $\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:b}}.$
$\displaystyle\widetilde{I}\models\widetilde{\mathit{P\\!T}}$
$\displaystyle\text{\ implies\ }\widetilde{I}\models\widehat{\mathit{P\\!T}}$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:evaluation:properties}~{}\ref{obs:evaluation:properties:c}}.\qed$

###### Proof of Theorem 16.

Let $P=\mathit{P\\!B}\cup\mathit{P\\!T}$ and $E={B(\mathit{P\\!B})}^{\pm}\cap
H(\mathit{P\\!T})$. We begin by evaluating $P$, $\mathit{P\\!B}$ and
$\mathit{P\\!T}$ w.r.t. $(I,J)$ and obtain

$\displaystyle(I,J)$
$\displaystyle=W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(I,J)$
$\displaystyle=(S_{P}^{\mathit{I\\!C}}(\mathit{J\\!C}\cup
J),S_{P}^{\mathit{J\\!C}}(\mathit{I\\!C}\cup I)),$
$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(I,J)$
$\displaystyle=(S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(\mathit{J\\!C}\cup\mathit{J\\!E}\cup
J),S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\mathit{J\\!E}}(\mathit{I\\!C}\cup\mathit{I\\!E}\cup
I))\text{, and}$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle=W_{\mathit{P\\!T}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})}(I,J)$
$\displaystyle=(S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\widehat{\mathit{I\\!B}}}(\mathit{J\\!C}\cup\widehat{\mathit{J\\!B}}\cup
J),S_{\mathit{P\\!T}}^{\mathit{J\\!C}\cup\widehat{\mathit{J\\!B}}}(\mathit{I\\!C}\cup\widehat{\mathit{I\\!B}}\cup
I)).$ Using $(\mathit{I\\!E},\mathit{J\\!E})\sqsubseteq(I,J)$, we get
$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle=(S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(\mathit{J\\!C}\cup
J),S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\mathit{J\\!E}}(\mathit{I\\!C}\cup
I)).$ By Lemma 54 and 52 (c), we get
$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle\sqsubseteq(I,J),$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle=(S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(\mathit{J\\!C}\cup
J),S_{\mathit{P\\!T}}^{\mathit{J\\!C}\cup\mathit{J\\!E}}(\mathit{I\\!C}\cup
I))\text{, and}$ $\displaystyle(I,J)$
$\displaystyle=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}}).$

We first show
$(\mathit{I\\!B},\mathit{J\\!B})=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
and then
$({\mathit{I\\!T}},{\mathit{J\\!T}})=(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$.

###### Property
$(\mathit{I\\!B},\mathit{J\\!B})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$.

$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqsubseteq(I,J)$
and $\displaystyle(\mathit{I\\!E},\mathit{J\\!E})=(I,J)\sqcap E$
$\displaystyle\text{\ implies\
}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqsubseteq(I,J).$
$\displaystyle(I,J)=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ implies\
}(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqsubseteq(I,J).$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqsubseteq
H(\mathit{P\\!T})$ $\displaystyle\text{\ implies\
}(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap
E.$
$(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap
E\text{\ and\ }$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqsubseteq(I,J)$
$\displaystyle\text{\ implies\
}(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!E},\mathit{J\\!E}).$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!E},\mathit{J\\!E})$
and
$\displaystyle(I,J)=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ implies\
}(I,J)\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\mathit{I\\!E},\mathit{J\\!E}).$

With the above, we use 52 (c) to show that
$(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$ is a fixed point of
$W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{J\\!C},\mathit{J\\!E})}$:

$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(I,J)$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}((I,J)\sqcap{B(\mathit{P\\!B})}^{\pm})$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}((\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\mathit{I\\!E},\mathit{J\\!E}))$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$

Thus, by Theorem 1 (c),
$(\mathit{I\\!B},\mathit{J\\!B})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$.

###### Property
$(\mathit{I\\!B},\mathit{J\\!B})=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$.

To show the property, let

$\displaystyle(\widetilde{I},\widetilde{J})$
$\displaystyle=(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}}),$
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
$\displaystyle=W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\sqcap
E,$ $\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})$
$\displaystyle=(S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\widetilde{\mathit{I\\!E}}}(\mathit{J\\!C}\cup\widetilde{J}),S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\widetilde{\mathit{J\\!E}}}(\mathit{I\\!C}\cup\widetilde{I})),$
$\displaystyle(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})$
$\displaystyle=(S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\widetilde{\mathit{I\\!B}}}(\mathit{J\\!C}\cup\widetilde{J}),S_{\mathit{P\\!T}}^{\mathit{J\\!C}\cup\widetilde{\mathit{J\\!B}}}(\mathit{I\\!C}\cup\widetilde{I})),\text{\
and}$ $\displaystyle
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})$
$\displaystyle=(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\sqcup(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\text{\
by \lx@cref{creftype~refnum}{prp:splitting:stable}.}$

We get:

$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle\text{\ implies\ }(\widetilde{I},\widetilde{J})\leq_{p}(I,J).$
$\displaystyle(\widetilde{I},\widetilde{J})\leq_{p}(I,J)$
$\displaystyle\text{\ implies\
}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(I,J).$
$\displaystyle
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(I,J)$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})\leq_{p}(\mathit{I\\!E},\mathit{J\\!E}).$
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!E},\mathit{J\\!E})$
$\displaystyle\text{\ implies\
}(\widetilde{I},\widetilde{J})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\mathit{I\\!E},\mathit{J\\!E}).$
$\displaystyle(\widetilde{I},\widetilde{J})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\mathit{I\\!E},\mathit{J\\!E})$
$\displaystyle\text{\ implies\
}\widetilde{\mathit{I\\!B}}=S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\widetilde{\mathit{I\\!E}}}(\mathit{J\\!C}\cup\mathit{J\\!E}\cup\mathit{J\\!B})$
$\displaystyle\hbox to0.0pt{\text{\ and\ }\hss}\phantom{\text{\ implies\
}}\widetilde{\mathit{J\\!B}}=S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\widetilde{\mathit{J\\!E}}}(\mathit{I\\!C}\cup\mathit{I\\!E}\cup\mathit{I\\!B}).$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:stable:relative:properties}~{}\ref{obs:stable:relative:properties:c}}.$
$\displaystyle\widetilde{\mathit{I\\!B}}=S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\widetilde{\mathit{I\\!E}}}(\mathit{J\\!C}\cup\mathit{J\\!E}\cup\mathit{J\\!B})$
and
$\displaystyle\widetilde{\mathit{J\\!B}}=S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\widetilde{\mathit{J\\!E}}}(\mathit{I\\!C}\cup\mathit{I\\!E}\cup\mathit{I\\!B})$
and
$\displaystyle\mathit{I\\!B}=S_{\mathit{P\\!B}}^{\mathit{I\\!C}\cup\mathit{I\\!E}}(\mathit{J\\!C}\cup\mathit{J\\!E}\cup\mathit{J\\!B})$
and
$\displaystyle\mathit{J\\!B}=S_{\mathit{P\\!B}}^{\mathit{J\\!C}\cup\mathit{J\\!E}}(\mathit{I\\!C}\cup\mathit{I\\!E}\cup\mathit{I\\!B})$
and
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})\leq_{p}(\mathit{I\\!E},\mathit{J\\!E})$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\leq_{p}(\mathit{I\\!B},\mathit{J\\!B})$
$\displaystyle\text{\ by\ \lx@cref{creftype~refnum}{prp:well-
founded:relative:monotonicity}}.$
$\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\leq_{p}(\mathit{I\\!B},\mathit{J\\!B})$
and
$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}}).$
$\displaystyle\widehat{\mathit{I\\!T}}=S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\widehat{\mathit{I\\!B}}}(\mathit{J\\!C}\cup
J)$ and
$\displaystyle\widehat{\mathit{J\\!T}}=S_{\mathit{P\\!T}}^{\mathit{J\\!C}\cup\widehat{\mathit{J\\!B}}}(\mathit{I\\!C}\cup
I)$ and
$\displaystyle\widetilde{\mathit{I\\!T}}=S_{\mathit{P\\!T}}^{\mathit{I\\!C}\cup\widetilde{\mathit{I\\!B}}}(\mathit{J\\!C}\cup\widetilde{J})$
and
$\displaystyle\widetilde{\mathit{J\\!T}}=S_{\mathit{P\\!T}}^{\mathit{J\\!C}\cup\widetilde{\mathit{J\\!B}}}(\mathit{I\\!C}\cup\widetilde{I})$
and
$\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\leq_{p}(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
and $\displaystyle(\widetilde{I},\widetilde{J})\leq_{p}(I,J)$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\leq_{p}(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ by\
\lx@cref{creftype~refnum}{prp:stable:relative:monotonicity}}.$ $\displaystyle
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})=(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\sqcup(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})$
and
$\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\leq_{p}(\mathit{I\\!B},\mathit{J\\!B})$
and
$\displaystyle(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\leq_{p}(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ implies\
}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}}).$
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})\leq_{p}(\mathit{I\\!E},\mathit{J\\!E})$
and
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})\sqsubseteq
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})$ and
$\displaystyle
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
and
$\displaystyle(\widetilde{I},\widetilde{J})=(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ implies\
}W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(\widetilde{I},\widetilde{J}).$
$\displaystyle\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}}(P)=(I,J)$ and
$\displaystyle
W_{P}^{\mathit{I\\!C},\mathit{J\\!C}}(\widetilde{I},\widetilde{J})\leq_{p}(\widetilde{I},\widetilde{J})$
$\displaystyle\text{\ implies\ }(I,J)\leq_{p}(\widetilde{I},\widetilde{J})$
$\displaystyle\text{\ by\ \lx@cref{creftypecap~refnum}{thm:knaster-
tarski}~{}\ref{thm:knaster-tarski:a}}.$
$\displaystyle(\widetilde{I},\widetilde{J})\leq_{p}(I,J)\text{\ and\
}(I,J)\leq_{p}(\widetilde{I},\widetilde{J})$ $\displaystyle\text{\ implies\
}(I,J)=(\widetilde{I},\widetilde{J}).$
$\displaystyle(\widetilde{I},\widetilde{J})=(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ implies\
}(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqsubseteq(\widetilde{I},\widetilde{J}).$
$\displaystyle(\widetilde{I},\widetilde{J})=(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
and
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!E},\mathit{J\\!E})$
$\displaystyle\text{\ implies\
}(\widetilde{I},\widetilde{J})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E}).$
$\displaystyle(I,J)=(\widetilde{I},\widetilde{J})$ and
$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})\sqsubseteq(\widetilde{I},\widetilde{J})$
and
$\displaystyle(\widetilde{I},\widetilde{J})\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\mathit{I\\!B},\mathit{J\\!B})\sqcup(\mathit{I\\!E},\mathit{J\\!E})$
and
$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(\mathit{I\\!B},\mathit{J\\!B})$
and
$\displaystyle(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!E},\mathit{J\\!E})}(I,J)$
$\displaystyle\text{\ implies\
}(\mathit{I\\!B},\mathit{J\\!B})=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:stable:relative:properties}~{}\ref{obs:stable:relative:properties:c}}.$

###### Property
$(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})=({\mathit{I\\!T}},{\mathit{J\\!T}})$.

Observe that the lemma can be applied with $\mathit{P\\!B}$ and
$\mathit{P\\!T}$ exchanged. Let

$\displaystyle\widetilde{E}$ $\displaystyle={B(\mathit{P\\!T})}^{\pm}\cap
H(\mathit{P\\!B})\text{,}$
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
$\displaystyle=(I,J)\cap\widetilde{E}\text{,}$
$\displaystyle(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})$
$\displaystyle=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})}(\mathit{P\\!T})\text{,
and}$ $\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})$
$\displaystyle=W_{\mathit{P\\!B}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})}(I,J).$
Using the properties shown so far, we obtain $\displaystyle(I,J)$
$\displaystyle=(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\sqcup(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}}).$

With this we get:

$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})$
and
$\displaystyle(I,J)=(\widehat{\mathit{I\\!B}},\widehat{\mathit{J\\!B}})\sqcup(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
and $\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\sqsubseteq
H(\mathit{P\\!B})$ and
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})=(I,J)\sqcap\widetilde{E}$
$\displaystyle\text{\ implies\
}(\mathit{I\\!B},\mathit{J\\!B})\sqcap{B(\mathit{P\\!T})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}}).$
$\displaystyle(I,J)=(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\sqcup(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})$
and
$\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\sqsubseteq
H(\mathit{P\\!B})$ and
$\displaystyle(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})=(I,J)\sqcap\widetilde{E}$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\sqcap{B(\mathit{P\\!T})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}}).$
$\displaystyle(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})\sqcap{B(\mathit{P\\!T})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
and
$\displaystyle(I,J)=(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\sqcup(\widetilde{\mathit{I\\!B}},\widetilde{\mathit{J\\!B}})$
$\displaystyle\text{\ implies\
}(I,J)\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\sqcup(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}}).$
$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\sqcap{B(\mathit{P\\!T})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
and
$\displaystyle(I,J)\sqcap{B(\mathit{P\\!B})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})\sqcup(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
and
$\displaystyle(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})=W_{\mathit{P\\!T}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})}(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})$
and
$\displaystyle(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})=W_{\mathit{P\\!T}}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})}(I,J)$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})=(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:stable:relative:properties}~{}\ref{obs:stable:relative:properties:c}}.$
$\displaystyle(\mathit{I\\!B},\mathit{J\\!B})\sqcap{B(\mathit{P\\!T})}^{\pm}\sqsubseteq(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})$
and
$\displaystyle(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\widetilde{\mathit{I\\!E}},\widetilde{\mathit{J\\!E}})}(\mathit{P\\!T})$
and
$\displaystyle(\mathit{I\\!T},\mathit{J\\!T})=\mathit{WM}^{(\mathit{I\\!C},\mathit{J\\!C})\sqcup(\mathit{I\\!B},\mathit{J\\!B})}(\mathit{P\\!T})$
$\displaystyle\text{\ implies\
}(\widetilde{\mathit{I\\!T}},\widetilde{\mathit{J\\!T}})=(\mathit{I\\!T},\mathit{J\\!T})$
$\displaystyle\text{\ by\
\lx@cref{creftypecap~refnum}{obs:stable:relative:properties}~{}\ref{obs:stable:relative:properties:c}}.$

Thus, we get
$(\widehat{\mathit{I\\!T}},\widehat{\mathit{J\\!T}})=({\mathit{I\\!T}},{\mathit{J\\!T}})$.∎

###### Proof of Theorem 17.

The theorem can be shown by transfinite induction over the sequence indices.
We do not give the full induction proof here but focus on the key idea. Let
$({I}_{i}^{\prime},{J}_{i}^{\prime})$ be the intermediate interpretations as
in 5 when computing the well-founded model of the sequence. Furthermore, let

$\displaystyle(I_{i},J_{i})$
$\displaystyle=\mathit{WM}^{(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})\sqcup(\mathit{I\\!E}_{i},\mathit{J\\!E}_{i})}({P}_{i})$
be the intermediate interpretations where
$(\mathit{I\\!C}_{i},\mathit{J\\!C}_{i})$ is the union of the intermediate
interpretations as in 4 and
$\displaystyle(\mathit{I\\!E}_{i},\mathit{J\\!E}_{i})$
$\displaystyle=(I,J)\cap E_{i}$

with $E_{i}$ as in 3.

Observe that with Theorem 16, we have
$\mathit{WM}(\bigcup_{i\in\mathbb{I}}{P}_{i})=\bigcup_{i\in\mathbb{I}}(I_{i},J_{i})$.
By Proposition 15, we have
$({I}_{i}^{\prime},{J}_{i}^{\prime})\leq_{p}(I_{i},J_{i})$ and, thus, we
obtain that
$\mathit{WM}({({P}_{i})}_{i\in\mathbb{I}})\leq_{p}\mathit{WM}(\bigcup_{i\in\mathbb{I}}{P}_{i})$.
∎

###### Proof of Theorem 18.

By Theorem 17, we have

$\displaystyle\bigsqcup_{i\in\mathbb{I}}(I_{i},J_{i})$
$\displaystyle\leq_{p}(I,J).$ We get $\bigcup_{i\in\mathbb{I}}I_{i}\subseteq
I$ and, thus, $\displaystyle\bigcup_{i\leq k}I_{i}$
$\displaystyle=\mathit{I\\!C}_{k}\cup I_{k}\subseteq I.$ Using
$J\subseteq\bigcup_{i\in\mathbb{I}}J_{i}$ and $J_{i}\subseteq H({P}_{i})$, we
get $\displaystyle J\cap{B({P}_{k})}^{\pm}$
$\displaystyle\subseteq(\bigcup_{i\leq
k}J_{i}\cup\bigcup_{k<i}H({P}_{i}))\cap{B({P}_{k})}^{\pm}$
$\displaystyle\subseteq(\bigcup_{i\leq k}J_{i}\cup
E_{k})\cap{B({P}_{k})}^{\pm}$ $\displaystyle\subseteq(\mathit{J\\!C}_{k}\cup
J_{k}\cup E_{k})\cap{B({P}_{k})}^{\pm}.$

Using both results, we obtain

$\displaystyle((\mathit{I\\!C}_{k},\mathit{J\\!C}_{k})\sqcup(\emptyset,E_{k})\sqcup(I_{k},J_{k}))\sqcap{B({P}_{k})}^{\pm}$
$\displaystyle\leq_{p}(I,J)\sqcap{B({P}_{k})}^{\pm}.$

Because the body literals determine the simplification, we get

$\displaystyle{P}_{k}^{I,J}$
$\displaystyle\subseteq{P}_{k}^{(\mathit{I\\!C}_{k},\mathit{J\\!C}_{k})\sqcup(\emptyset,E_{k})\sqcup(I_{k},J_{k})}.\qed$

######  Lemma 55.

Let ${({P}_{i})}_{i\in\mathbb{I}}$ be a sequence of $\mathcal{R}$-programs,
and $(I,J)$ be the well-founded model of $\bigcup_{i\in\mathbb{I}}{{P}_{i}}$.

Then, $\bigcup_{i\in\mathbb{I}}{{P}_{i}}$ and
$\bigcup_{i\in\mathbb{I}}{{Q}_{i}}$ with
${P}_{i}^{I,J}\subseteq{Q}_{i}\subseteq{P}_{i}$ have the same well-founded and
stable models.

###### Proof.

This lemma is a direct consequence of Theorems 11, 12 and 18. ∎

###### Proof of Corollary 19.

This corollary is a direct consequence of Theorems 18 and 55. ∎

###### Proof of Corollary 20.

This can be proven in the same way as Theorem 17 but note that because $E_{i}$
is empty, we get $({I}_{i}^{\prime},{J}_{i}^{\prime})=(I_{i},J_{i})$. ∎

###### Proof of Corollary 21.

This can be proven in the same way as Theorem 18 but note that because $E_{i}$
is empty, all $\leq_{p}$ and most $\subseteq$ relations can be replaced with
equivalences. ∎

Whenever head atoms do not interfere with negative body literals, the relative
well founded-model of a program can be calculated with just two applications
of the relative stable operator.

######  Lemma 56.

Let $P$ be an $\mathcal{F}$-program such that ${B(P)}^{-}\cap H(P)=\emptyset$
and $(\mathit{I\\!C},\mathit{J\\!C})$ be a four-valued interpretation.

Then,
$\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}}(P)=(S_{P}^{\mathit{I\\!C}}(\mathit{J\\!C}),S_{P}^{\mathit{J\\!C}}(\mathit{I\\!C}))$.

###### Proof.

Let $(I,J)=\mathit{WM}^{\mathit{I\\!C},\mathit{J\\!C}}(P)$.

We have $J=S_{P}^{\mathit{J\\!C}}(\mathit{I\\!C}\cup I)$. By 52 (b), we get
$J\subseteq H(P)$. With this and ${B(P)}^{-}\cap H(P)=\emptyset$, we get
${B(P)}^{-}\cap J=\emptyset$. Thus, $S_{P}^{\mathit{I\\!C}}(\mathit{J\\!C}\cup
J)=S_{P}^{\mathit{I\\!C}}(\mathit{J\\!C})$ by 52 (c).

The same arguments apply to show $S_{P}^{\mathit{J\\!C}}(\mathit{I\\!C}\cup
I)=S_{P}^{\mathit{J\\!C}}(\mathit{I\\!C})$. ∎

Any sequence as in Corollary 20 in which each $P_{i}$ additionally satisfies
the precondition of Lemma 56 has a total well-founded model. Furthermore, the
well-founded model of such a sequence can be calculated with just two
(independent) applications of the relative stable operator per program $P_{i}$
in the sequence.

###### Proof of Proposition 23.

We use Lemma 41 to show that both formulas are strongly equivalent.

###### Property $I\models\pi(a)^{J}$ implies $I\models\tau(a)^{J}$ for
arbitrary interpretations $I$.

The formulas $\pi(a)$ and $\tau(a)$ only differ in the consequents of their
implications. Observe that the consequents in $\pi(a)$ are stronger than the
ones in $\tau(a)$. Thus, it follows that $\pi(a)$ is stronger than $\tau(a)$.
Furthermore, observe that the same holds for their reducts.

###### Property $I\not\models\pi(a)^{J}$ implies $I\not\models\tau(a)^{J}$ for
arbitrary interpretations $I$.

Let $G$ be the set of all instance of the aggregate elements of $a$. Because
$I\not\models\pi(a)^{J}$, there must be a set $D\subseteq G$ such that
$D\mathrel{\not\kern-1.0pt\triangleright}a$,
$I\models{(\tau(D)^{\wedge})}^{J}$, and
$I\not\models{({\pi_{a}}(D)^{\vee})}^{J}$. With this, we construct the set

$\displaystyle\widehat{D}=D\cup\\{e\in G\setminus D\mid
I\models\tau(e)^{J}\\}.$ The construction of $\widehat{D}$ and $\displaystyle
D\mathrel{\not\kern-1.0pt\triangleright}a$ and $\displaystyle
I\not\models{({\pi_{a}}(D)^{\vee})}^{J}$ $\displaystyle\text{\ implies\
}\widehat{D}\mathrel{\not\kern-1.0pt\triangleright}a\text{\ and\
}I\not\models{(\tau_{a}(\widehat{D})^{\vee})}^{J}.$ The construction of
$\widehat{D}$ and $\displaystyle I\models{(\tau(D)^{\wedge})}^{J}$
$\displaystyle\text{\ implies\ }I\models{(\tau(\widehat{D})^{\wedge})}^{J}.$
$\displaystyle\widehat{D}\mathrel{\not\kern-1.0pt\triangleright}a$ and
$\displaystyle I\not\models{(\tau_{a}(\widehat{D})^{\vee})}^{J}$ and
$\displaystyle I\models{(\tau(\widehat{D})^{\wedge})}^{J}$
$\displaystyle\text{\ implies\ }I\not\models\tau(a)^{J}.\qed$

###### Proof of Proposition 24.

Let $G$ be the set of ground instances of the aggregate elements of $a$.
Furthermore, observe that a monotone aggregate $a$ is either constantly true
or not justified by the empty set.

In case that $\pi(a)\equiv\top$, we get $\pi(a)_{I}\equiv\top$ and the lemma
holds.

Next, we consider the case that the empty set does not justify the aggregate.
Observe that ${\pi_{a}}(\emptyset)$ is stronger than ${\pi_{a}}(D)$ for any
$D\subseteq G$. And, we have that $\pi(a)$ contains the implication
$\top\rightarrow{\pi_{a}}(\emptyset)$. Because of this, we have
$\pi(a)\equiv{\pi_{a}}(\emptyset)$. Furthermore, all consequents in $\pi(a)$
are positive formulas and, thus, not modified by the reduct. Thus, the reduct
${(\top\rightarrow{\pi_{a}}(\emptyset))}_{I}$ is equal to
$\top\rightarrow{\pi_{a}}(\emptyset)$. And as before, it is stronger than all
other implications in $\pi(a)_{I}$. Hence, we get
$\pi(a)_{I}\equiv{\pi_{a}}(\emptyset)$. ∎

###### Proof of Theorem 25.

Remember that the translation $\pi(a)$ is a conjunction of implications. The
antecedents of the implications are conjunctions of aggregate elements and the
consequents are disjunctions of conjunctions of aggregate elements.

###### Property (a).