$\beta\not\rightsquigarrow\alpha$. We first show that $\succ$ is acyclic. If
it was not the case, there would be a cycle
$\alpha_{1}\succ\alpha_{2}\succ\dots\succ\alpha_{n}\succ\alpha_{1}$. By
construction of $\succ$, it would then be the case that
$\alpha_{1}\rightsquigarrow\alpha_{2}\rightsquigarrow\dots\rightsquigarrow\alpha_{n}\rightsquigarrow\alpha_{1}$
and for every $(j,i)\in\\{(1,2),\dots,(n-1,n),(n,1)\\}$,
$\alpha_{i}\not\rightsquigarrow\alpha_{j}$, a contradiction. It is then easy
to verify that $F$ is the corresponding AF of $P$:

  * •

if $\alpha\rightsquigarrow\beta$ then $\alpha\rightsquigarrow^{P}\beta$ by
construction of $\rightsquigarrow^{P}$ and $\beta\not\succ\alpha$ otherwise
$\alpha\not\rightsquigarrow\beta$ by construction of $\succ$;

  * •

if (i) $\alpha\rightsquigarrow^{P}\beta$ and (ii) $\beta\not\succ\alpha$, then
it follows from (i) that $\alpha\rightsquigarrow\beta$ or
$\beta\rightsquigarrow\alpha$, and from (ii) that
$\beta\not\rightsquigarrow\alpha$ or $\alpha\rightsquigarrow\beta$, so
$\alpha\rightsquigarrow\beta$.∎

See 28

###### Proof.

Let $F=(\mathit{Args},\rightsquigarrow)$ be a strongly symmetric SETAF.
Suppose for a contradiction that there is a preferred extension $E$ that is
not a stable extension. Then $(\mathit{Args}\setminus E)\setminus
E^{+}\neq\emptyset$. Let $B=\\{\beta_{1},\ldots,\beta_{n}\\}$ be a
$\subseteq$-maximal subset of $(\mathit{Args}\setminus E)\setminus E^{+}$ that
is conflict-free. We show with the following two claims that $E\cup B$ is
admissible, which contradicts the fact that $E$ is a preferred extension, and
therefore allows us to conclude that $E$ is stable.
Claim: $E\cup B$ is conflict-free.
_Proof of claim_. Suppose that $E\cup B$ is not conflict-free. As $E$ is
conflict-free and $B$ is conflict-free, any attack contained in $E\cup B$ must
contain elements from both $E$ and $B$. Moreover, since $F$ is strongly
symmetric, we may assume that the attack targets an element of $E$. Thus,
there exists $S\subseteq E\cup B$ with $S\cap B\neq\emptyset$ and
$\varepsilon\in E$ such that $S\rightsquigarrow\varepsilon$. Since $E$ is a
preferred extension, we must have $(S\setminus E)\cap E^{+}\neq\emptyset$,
which implies $B\cap E^{+}\neq\emptyset$. This is a contradiction, since
$B\subseteq\mathit{Args}\setminus E^{+}$.
Claim: $E\cup B\subseteq\Gamma_{F}(E\cup B)$.
_Proof of claim_. Suppose for a contradiction that $E\cup
B\not\subseteq\Gamma_{F}(E\cup B)$. Then there exists an attack
$S\rightsquigarrow\alpha$ such that $\alpha\in E\cup B$ and $S\cap(E\cup
B)^{+}=\emptyset$. Since $E$ is a preferred extension, we know that
$E\subseteq\Gamma_{F}(E)\subseteq\Gamma_{F}(E\cup B)$, so $\alpha\in B$. Since
$E\cup B$ is conflict-free (by the preceding claim), there must exist
$\sigma\in S\setminus(E\cup B)$. As $S\cap(E\cup B)^{+}=\emptyset$, we must
have $\sigma\in(\mathit{Args}\setminus E)\setminus E^{+}$. From the maximality
of $B$, we know that $B\cup\\{\sigma\\}$ is not conflict-free, and since $B$
is conflict-free, there must be an attack that involves $\sigma$. Moreover, as
$F$ is strongly symmetric, we can assume that $\sigma$ is the target of the
attack, which yields $\sigma\in B^{+}$, again contradicting $S\cap(E\cup
B)^{+}=\emptyset$. ∎

See 32

###### Proof.

Let $P=(\mathit{Args},\rightsquigarrow,\succ)$ be a strongly symmetric PSETAF
such that $\succ$ is transitive, and let
$F=(\mathit{Args},\rightsquigarrow_{\succ})$ be the corresponding SETAF.
Suppose for a contradiction that $S_{0}$ is a preferred extension of $P$ but
not a stable extension of $P$. It follows that $S_{0}$ is a preferred
extension of $F$ but not a stable extension of $F$. To obtain a contradiction,
we will construct an admissible set which is a proper superset of $S_{0}$. To
initiate the construction, we will require the following claim.
Claim 1. There exists $\alpha\in(\mathit{Args}\setminus S_{0})$ such that
$S_{0}\cup\\{\alpha\\}$ is conflict-free in $F$.
_Proof of claim_. Since $S_{0}$ is preferred but not stable, there is
$\alpha\in(\mathit{Args}\setminus S_{0})$ such that $\alpha\not\in S_{0}^{+}$.
Suppose for a contradiction that $S_{0}\cup\\{\alpha\\}$ is not conflict-free.
As $\alpha\not\in S_{0}^{+}$, it follows that there is some
$S^{\prime}\subseteq S_{0}$ and $\sigma\in S_{0}$ such that
$S^{\prime}\cup\\{\alpha\\}\rightsquigarrow_{\succ}\sigma$. However, since
$S_{0}$ is preferred, it must defend itself against this attack, and since
$S_{0}$ is conflict-free, the only possibility is that $\alpha\in S_{0}^{+}$,
which yields a contradiction. (end proof of claim)
We now proceed to construct a finite sequence $S_{0},S_{1},S_{2},\ldots,S_{n}$
of subsets of $\mathit{Args}$ as follows:

  * •

While there exists $\alpha$ such that (i) $\alpha\in(\mathit{Args}\setminus
S_{i})$ and (ii) $S_{i}\cup\\{\alpha\\}$ is conflict-free

    * –

Pick some $\alpha_{i}$ that satisfies (i) and (ii) and such that there is no
$\alpha_{i}^{\prime}$ satisfying (i) and (ii) with
$\alpha_{i}^{\prime}\succ\alpha_{i}$ (such an $\alpha_{i}$ must exist due to
the acyclicity of $\succ$).

    * –

Set $S_{i+1}=S_{i}\cup\\{\alpha_{i}\\}$

Since for every $i\geq 0$, we have $S_{i}\subseteq\mathit{Args}$ and
$S_{i}\subsetneq S_{i+1}$, the construction will terminate after a finite
number of iterations. We observe that each $S_{i}$ is conflict-free. We will
show that the final set $S_{n}$ is conflict-free and defends itself against
all attacks, which contradicts the fact that $S_{0}$ is a preferred extension.
The main ingredient in showing this is the following claim:
Claim 2. For each $0\leq i\leq n$, the following property holds:

> For each attack $T\rightsquigarrow_{\succ}\sigma$ on $S_{i}$ such that
> $T\cap S_{i}^{+}=\emptyset$ (i.e. $S_{i}$ does not defend against this
> attack):
>
> (a)
>
>
> if $i\geq 1$ and $\tau\in T\setminus S_{i}$, then the set
> $S_{i-1}\cup\\{\tau\\}$ is conflict-free;
>
> (b)
>
>
> for every $\tau\in T\setminus S_{i}$, $\tau\not\succ\sigma^{\prime}$ for all
> $\sigma^{\prime}\in S_{i}\setminus S_{0}$;
>
> (c)
>
>
> there exists $\tau\in T\setminus S_{i}$ such that
> $\tau\not\succ\tau^{\prime}$ for every $\tau^{\prime}\in
> T\cup\\{\sigma\\}\setminus\\{\tau\\}$.

_Proof of claim_. The base case ($i=0$) is trivial, as $S_{0}$ is a preferred
extension, and so there is no undefended attack. We will suppose that we have
already shown the property to hold for $i=0,\ldots,k$ and prove it still holds
for $i=k+1$. Let us consider some attack $T\rightsquigarrow_{\succ}\sigma$
with $\sigma\in S_{k+1}$ such that $T\cap S_{k+1}^{+}=\emptyset$. We need to
show that conditions (a), (b), and (c) are satisfied. We prove each condition
in turn.
Claim 2.1: Condition (a) holds: for every $\tau\in T\setminus S_{k+1}$, the
set $S_{k}\cup\\{\tau\\}$ is conflict-free.
_Proof of claim._ Suppose for a contradiction that $S_{k}\cup\\{\tau\\}$ is
not conflict-free. The attack contained in $S_{k}\cup\\{\tau\\}$ cannot target
$\tau$, since otherwise we would have $\tau\in T\cap S_{k}^{+}$, contradicting
the fact that $T\cap S_{k+1}^{+}=\emptyset$. The conflict must however involve
$\tau$ since $S_{k}$ is conflict-free. Thus, there must exist $S^{*}\subseteq
S_{k}$ and $\sigma^{*}\in S_{k}$ such that
$S^{*}\cup\\{\tau\\}\rightsquigarrow_{\succ}\sigma^{*}$. If
$(S^{*}\cup\\{\tau\\})\cap S_{k+1}^{+}\neq\emptyset$, then we must have
$\tau\in S_{k+1}^{+}$, which again gives a contradiction. Thus,
$(S^{*}\cup\\{\tau\\})\cap S_{k+1}^{+}=\emptyset$, which implies
$(S^{*}\cup\\{\tau\\})\cap S_{k}^{+}=\emptyset$. We can therefore apply the
induction hypothesis for $i=k$. As $(S^{*}\cup\\{\tau\\})\setminus
S_{k}=\\{\tau\\}$, it follows from condition (c) applied to the undefended
attack $S^{*}\cup\\{\tau\\}\rightsquigarrow_{\succ}\sigma^{*}$ that
$\tau\not\succ\beta$ for all $\beta\in S^{*}\cup\\{\sigma^{*}\\}$. Since $P$
is strongly symmetric, it follows that we also have the attack
$S^{*}\cup\\{\sigma^{*}\\}\rightsquigarrow_{\succ}\tau$. But this means that
$T\cap S_{k}^{+}\neq\emptyset$, so $T\cap S_{k+1}^{+}\neq\emptyset$, a
contradiction. (end proof of claim)
Claim 2.2: Condition (b) holds: for every $\tau\in T\setminus S_{k+1}$,
$\tau\not\succ\sigma^{\prime}$ for all $\sigma^{\prime}\in S_{k+1}\setminus
S_{0}$.
_Proof of claim._ Suppose for a contradiction that the condition does not
hold. Since $S_{k+1}\setminus
S_{0}=\\{\alpha_{0},\ldots,\alpha_{k-1},\alpha_{k}\\}$, this means that there
exists $\tau\in T\setminus S_{k+1}$ and $0\leq j\leq k$ such that
$\tau\succ\alpha_{j}$. Since $\alpha_{j}$ was selected for addition to $S_{j}$
despite $\tau\succ\alpha_{j}$, it must be the case that $S_{j}\cup\\{\tau\\}$
is not conflict-free. As $S_{j}\subseteq S_{k}$, the set $S_{k}\cup\\{\tau\\}$
must also contain some attack, which contradicts Claim 2.1, which states that
$S_{k}\cup\\{\tau\\}$ is conflict-free. (end proof of claim)
Claim 2.3: Condition (c) holds: there exists $\tau\in T\setminus S_{k+1}$ such
that $\tau\not\succ\tau^{\prime}$ for every $\tau^{\prime}\in
T\cup\\{\sigma\\}\setminus\\{\tau\\}$.
_Proof of claim._ Suppose for a contradiction that condition (c) does not
hold. Then for every $\tau\in T\setminus S_{k+1}$, there exists
$\tau^{\prime}\in(T\cup\\{\sigma\\}\setminus\\{\tau\\})$ such that
$\tau\succ\tau^{\prime}$. However, due to Claim 2.2, we know that
$\tau^{\prime}\not\in S_{k+1}\setminus S_{0}$. Moreover, we also know that
$\sigma\in S_{k+1}\setminus S_{0}$, since $T\cap S_{k+1}^{+}=\emptyset$, while
every attack on $S_{0}$ is defended ($S_{0}$ being a preferred extension).
Thus, we have:

For every $\tau\in T\setminus S_{k+1}$, there exists
$\tau^{\prime}\in(T\setminus(S_{k+1}\setminus S_{0}))\setminus\\{\tau\\}$ such
that $\tau\succ\tau^{\prime}$. (1)

Define $S_{0}^{*}$ as the restriction of $S_{0}$ to those elements $s_{0}\in
S_{0}$ such that $s_{0}\not\succ\tau^{\prime}$ for every $\tau^{\prime}\in
S_{k+1}\setminus S_{0}$. We aim to show that if $\tau\in T\setminus S_{k+1}$
and $s_{0}\in S_{0}\setminus S_{0}^{*}$, then $\tau\not\succ s_{0}$. Suppose
for a contradiction that we have $\tau\succ s_{0}$ for such a $\tau$ and
$s_{0}$. From $s_{0}\in S_{0}\setminus S_{0}^{*}$, we know that there exists
$\tau^{\prime}\in S_{k+1}\setminus S_{0}$ such that $s_{0}\succ\tau^{\prime}$.
But then by transitivity of $\succ$, we must also have
$\tau\succ\tau^{\prime}$, which contradicts Claim 2.2. We can thus refine the
preceding statement as follows:

For every $\tau\in T\setminus S_{k+1}$, there exists
$\tau^{\prime}\in(T\setminus(S_{k+1}\cup\\{\tau\\}))\cup(T\cap S_{0}^{*})$
such that $\tau\succ\tau^{\prime}$. (2)

Next consider $\sigma_{0}\in T\cap S_{0}^{*}$, and suppose for a contradiction
that there is no $\tau^{\prime}\in T\cup\\{\sigma\\}$ such that
$\sigma_{0}\succ\tau^{\prime}$. Since $P$ is strongly symmetric and
$T\rightsquigarrow_{\succ}\sigma$, we must have
$T\setminus\\{\sigma_{0}\\}\cup\\{\sigma\\}\rightsquigarrow_{\succ}\sigma_{0}$.
We know that $(T\setminus\\{\sigma_{0}\\}\cup\\{\sigma\\})\cap
S_{0}^{+}\neq\emptyset$ since $S_{0}$ is a preferred extension of $F$. As
$\sigma\in S_{k+1}$ and $S_{k+1}$ is conflict-free, it must be the case that
$(T\setminus S_{k+1})\cap S_{0}^{+}\neq\emptyset$. But this means that $T\cap
S_{k+1}^{+}\neq\emptyset$, a contradiction. When combined with the definition
of $S_{0}^{*}$ and the transitivity of $\succ$, we get:

For every $\sigma_{0}\in T\cap S_{0}^{*}$, there exists $\tau^{\prime}\in
T\setminus(S_{k+1}\setminus S_{0}^{*})$ such that
$\sigma_{0}\succ\tau^{\prime}$. (3)

Since $S_{k+1}$ is conflict-free, we know that $T\setminus
S_{k+1}\neq\emptyset$. This means that the set $(T\setminus S_{k+1})\cup(T\cap
S_{0}^{*})$ is non-empty. Moreover, statements (2) and (3) show that for every
$\tau\in(T\setminus S_{k+1})\cup(T\cap S_{0}^{*})$ there exists
$\tau^{\prime}\in(T\setminus S_{k+1})\cup(T\cap S_{0}^{*})$ such that
$\tau\succ\tau^{\prime}$. This implies the existence of a cycle in the
preference relation $\succ$, contradicting the fact that $\succ$ is acyclic.
(end proof of claim)
We have thus established Claim 2. Now consider the final set $S_{n}$, which
is, by construction, conflict-free. Suppose for a contradiction that
$S_{n}\not\subseteq\Gamma_{F}(S_{n})$. Then there is an attack
$U\rightsquigarrow_{\succ}\sigma_{n}$ on some $\sigma_{n}\in S_{n}$ such that
$U\cap S_{n}^{+}=\emptyset$. Since $S_{n}$ is conflict-free, $U\setminus
S_{n}\neq\emptyset$. Consider some $\upsilon\in U\setminus S_{n}$. Since
$\upsilon\not\in S_{n}$, the set $S_{n}\cup\\{\upsilon\\}$ is not conflict-
free, and so there must be some attack that involves but does not target
$\upsilon$. Let
$S_{n}^{\prime}\cup\\{\upsilon\\}\rightsquigarrow_{\succ}\sigma_{n}^{\prime}$
be such an attack, where $S_{n}^{\prime}\subseteq S_{n}$ and
$\sigma_{n}^{\prime}\in S_{n}$. Since $S_{n}$ is conflict-free and
$\upsilon\not\in S_{n}^{+}$, this attack is not defended by $S_{n}$, i.e.
$(S_{n}^{\prime}\cup\\{\upsilon\\})\cap S_{n}^{+}=\emptyset$. We can thus
apply Claim 2, condition (c), to obtain $\upsilon\not\succ\beta$ for all
$\beta\in S_{n}^{\prime}\cup\\{\sigma_{n}^{\prime}\\}$. It follows that we
also have the attack
$S_{n}^{\prime}\cup\\{\sigma_{n}^{\prime}\\}\rightsquigarrow_{\succ}\upsilon$,
which contradicts $U\cap S_{n}^{+}=\emptyset$.

We have thus exhibited a set $S_{n}\supsetneq S_{0}$ that is conflict-free and
such that $S_{n}\subseteq\Gamma_{F}(S_{n})$, which contradicts that fact that
$S_{0}$ is a preferred extension. Having obtained the desired contradiction,
we can conclude that every preferred extension of a strongly symmetric PSETAF
with a transitive preference relation is also a stable extension. ∎

##  Appendix C Proofs for Section 6

######  Lemma 51.

Let $\mathcal{K}_{\succ}$ be a prioritized KB with
$\mathcal{K}=\langle\mathcal{T},\mathcal{A}\rangle$ and
$\mathcal{A}^{\prime}\subseteq\mathcal{A}$. The set $\mathcal{A}^{\prime}$ is
$\mathcal{T}$-consistent iff $\mathcal{A}^{\prime}$ is conflict-free in the
associated PSETAF $F_{\mathcal{K},\succ}$.

###### Proof.

Assume for a contradiction that $\mathcal{A}^{\prime}$ is
$\mathcal{T}$-consistent and not conflict-free. There exists
$\alpha\in\mathcal{A}^{\prime}\cap\mathcal{A}^{\prime+}$, so there exists
$A\subseteq\mathcal{A}^{\prime}$ such that
$A\rightsquigarrow_{\mathcal{K}}\alpha$. However, it follows that
$(A\cup\\{\alpha\\})\in\mathit{Conf}(\mathcal{K})$, contradicting the
$\mathcal{T}$-consistency of $\mathcal{A}^{\prime}$.

If $\mathcal{A}^{\prime}$ is $\mathcal{T}$-inconsistent, there exists
$C\in\mathit{Conf}(\mathcal{K})$ such that $C\subseteq\mathcal{A}^{\prime}$.
Since $\succ$ is acyclic and $C$ is finite, there exists $\gamma\in C$ such
that for every $\delta\in C$, $\gamma\not\succ\delta$. It follows that
$C\setminus\\{\gamma\\}\rightsquigarrow_{\mathcal{K}}\gamma$. Thus $\gamma\in
C\cap C^{+}$, i.e., $C$ is not conflict-free, hence neither is
$\mathcal{A}^{\prime}$. ∎

See 35

###### Proof.

Assume for a contradiction that
$\mathcal{A}^{\prime}\in\mathit{PRep}(\mathcal{K}_{\succ})$ and is not a
stable extension of $F_{\mathcal{K},\succ}$. By Lemma 51,
$\mathcal{A}^{\prime}$ is conflict-free so
${\mathcal{A}^{\prime}}^{+}\subseteq\mathcal{A}\setminus\mathcal{A}^{\prime}$.
Since $\mathcal{A}^{\prime}$ is not stable, there must then exist
$\alpha\in\mathcal{A}\setminus\mathcal{A}^{\prime}$ such that
$\alpha\notin{\mathcal{A}^{\prime}}^{+}$. Since $\mathcal{A}^{\prime}$ is a
repair, $\mathcal{A}^{\prime}\cup\\{\alpha\\}$ is $\mathcal{T}$-inconsistent,
and since $\alpha\notin{\mathcal{A}^{\prime}}^{+}$, then for every
$B\subseteq\mathcal{A}^{\prime}$ such that $B\cup\\{\alpha\\}$ is
$\mathcal{T}$-inconsistent, there exists $\beta\in B$ such that
$\alpha\succ\beta$. Then
$\mathcal{A}^{\prime}\setminus\\{\beta\mid\alpha\succ\beta\\}\cup\\{\alpha\\}$
is a Pareto improvement of $\mathcal{A}^{\prime}$. It follows that
$\mathcal{A}^{\prime}\notin\mathit{PRep}(\mathcal{K})$.

In the other direction, assume for a contradiction that $\mathcal{A}^{\prime}$
is a stable extension of $F_{\mathcal{K},\succ}$ and
$\mathcal{A}^{\prime}\notin\mathit{PRep}(\mathcal{K}_{\succ})$. By Lemma 51,
since $\mathcal{A}^{\prime}$ is stable, $\mathcal{A}^{\prime}$ is
$\mathcal{T}$-consistent. Since
$\mathcal{A}^{\prime}\notin\mathit{PRep}(\mathcal{K}_{\succ})$, it follows
that there exists $\alpha\in\mathcal{A}\setminus\mathcal{A}^{\prime}$ such
that $\alpha$ is $\mathcal{T}$-consistent and for every
$B\subseteq\mathcal{A}^{\prime}$ such that $B\cup\\{\alpha\\}$ is
$\mathcal{T}$-inconsistent, there exists $\beta\in B$ such that
$\alpha\succ\beta$. Since $\mathcal{A}^{\prime}$ is stable, there exists
$A\subseteq\mathcal{A}^{\prime}$ such that
$A\rightsquigarrow_{\mathcal{K}}\alpha$ (otherwise
$\alpha\notin{\mathcal{A}^{\prime}}^{+}$). But then $A\cup\\{\alpha\\}$ is
$\mathcal{T}$-inconsistent, so there exists $\beta\in A$ such that
$\alpha\succ\beta$, which contradicts $A\rightsquigarrow_{\mathcal{K}}\alpha$.
∎

See 36

###### Proof.

Let $\mathcal{K}_{\succ}$ be a prioritized KB with
$\mathcal{K}=\langle\mathcal{T},\mathcal{A}\rangle$, and a transitive priority
relation $\succ$. The associated PSETAF is
$F_{\mathcal{K},\succ}=(\mathcal{A},\rightsquigarrow_{\mathcal{K}},\succ)$,
where $\rightsquigarrow_{\mathcal{K}}=\\{(C\setminus\\{\alpha\\},\alpha)\mid
C\in\mathit{Conf}(\mathcal{K}),\alpha\in C\\}$.

Let
$F_{\mathsf{cl}}=(\mathcal{A},\rightsquigarrow_{\mathcal{K}},\succ^{\prime})$
where $\succ^{\prime}$ is the transitive closure of $\succ$. The transitive
closure of an acyclic binary relation is acyclic, so $\succ^{\prime}$ is an
acyclic binary relation over $\mathcal{A}$, so $F_{\mathsf{cl}}$ is a PSETAF.
Moreover, observe that $F_{\mathsf{cl}}$ is strongly symmetric and
$\succ^{\prime}$ is transitive, so by Theorem 32, $F_{\mathsf{cl}}$ is
coherent.

We show that $F_{\mathcal{K},\succ}$ and $F_{\mathsf{cl}}$ have the same
corresponding SETAF, so that $F_{\mathcal{K},\succ}$ is coherent. The
corresponding SETAF of $F_{\mathcal{K},\succ}$ is
$(\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ})$, where
$S\rightsquigarrow_{\mathcal{K},\succ}\alpha$ iff
$S\rightsquigarrow_{\mathcal{K}}\alpha$ and $\alpha\not\succ\beta$ for every
$\beta\in S$, and the corresponding SETAF of $F_{\mathsf{cl}}$ is
$(\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ^{\prime}})$, where
$S\rightsquigarrow_{\mathcal{K},\succ^{\prime}}\alpha$ iff
$S\rightsquigarrow_{\mathcal{K}}\alpha$ and $\alpha\not\succ^{\prime}\beta$
for every $\beta\in S$. Since $\succ\subseteq\succ^{\prime}$, we thus have
$\rightsquigarrow_{\mathcal{K},\succ^{\prime}}\subseteq\rightsquigarrow_{\mathcal{K},\succ}$.
Assume for a contradiction that there exists
$S\rightsquigarrow_{\mathcal{K},\succ}\alpha$ such that
$S\not\rightsquigarrow_{\mathcal{K},\succ^{\prime}}\alpha$. There must be
$\beta\in S$ such that $\alpha\succ^{\prime}\beta$. Since $\succ^{\prime}$ is
the transitive closure of $\succ$, it follows that there exists
$\gamma_{1},\dots,\gamma_{n}$ such that
$\alpha\succ\gamma_{1}\succ\dots\succ\gamma_{n}\succ\beta$. But then, since
$\\{\alpha,\beta\\}\subseteq S\cup\\{\alpha\\}\in\mathit{Conf}(\mathcal{K})$
and $\succ$ is a transitive priority relation, it follows that
$\alpha\succ\beta$. Hence $S\not\rightsquigarrow_{\mathcal{K},\succ}\alpha$.
We conclude that
$\rightsquigarrow_{\mathcal{K},\succ^{\prime}}=\rightsquigarrow_{\mathcal{K},\succ}$
and that$F_{\mathcal{K},\succ}$ and $F_{\mathsf{cl}}$ have the same
corresponding SETAF. ∎

See 39

###### Proof.

Since $\mathcal{B}\in\mathit{PRep}(\mathcal{K}_{\succ})$, by Theorem 35,
$\mathcal{B}$ is a stable extension of $F_{\mathcal{K},\succ}$. Since every
stable extension is also a complete extension, and $\mathcal{G}$ is the
$\subseteq$-minimal complete extension of $F_{\mathcal{K},\succ}$, it follows
that $\mathcal{G}\subseteq\mathcal{B}$. ∎

See 38

###### Proof.

Let $\mathcal{G}$ be the grounded extension of $F_{\mathcal{K}}$ and
$\mathcal{A}^{\cap}$ be the intersection of the repairs of $\mathcal{K}$. Let
$\alpha\in\mathcal{A}^{\cap}$. There is no $C\in\mathit{Conf}(\mathcal{K})$
such that $\alpha\in C$ (otherwise $C\setminus\\{\alpha\\}$ would be
$\mathcal{T}$-consistent and could be extended to a repair of $\mathcal{K}$
that would not contain $\alpha$). Thus there is no
$A\rightsquigarrow_{\mathcal{K}}\alpha$. It follows that
$\alpha\in\Gamma_{F_{\mathcal{K}}}(\emptyset)\subseteq\mathcal{G}$. Hence
$\mathcal{A}^{\cap}\subseteq\mathcal{G}$. In the other direction, let
$\mathcal{A}^{\prime}\in\mathit{SRep}(\mathcal{K})$. Since $\succ_{\emptyset}$
is the empty relation, then
$\mathit{SRep}(\mathcal{K})=\mathit{PRep}(\mathcal{K}_{\succ_{\emptyset}})$,
so $\mathcal{A}^{\prime}\in\mathit{PRep}(\mathcal{K}_{\succ_{\emptyset}})$ and
by Theorem 39, $\mathcal{G}\subseteq\mathcal{A}^{\prime}$. It follows that
$\mathcal{G}\subseteq\mathcal{A}^{\cap}$. ∎

See 46

###### Proof.

Let $\alpha\in\mathit{Elect}(\mathcal{K}_{\succ})$ and
$F=(\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ})$ be the SETAF
corresponding to $F_{\mathcal{K},\succ}$. Since for every
$C\in\mathit{Conf}(\mathcal{K})$ such that $\alpha\in C$, there exists
$\beta\in C$ such that $\alpha\succ\beta$, there is no
$C\in\mathit{Conf}(\mathcal{K})$ such that
$C\setminus\\{\alpha\\}\rightsquigarrow_{\mathcal{K},\succ}\alpha$, so no
$S\subseteq\mathcal{A}$ such that
$S\rightsquigarrow_{\mathcal{K},\succ}\alpha$. It follows that
$\alpha\in\Gamma_{F}(\emptyset)\subseteq\mathcal{G}$. ∎

See 48

###### Proof.

We adapt the proof of P-hardness for the problem of deciding whether an
argument belongs to the grounded extension of an argumentation framework given
in (?) (Reduction 3.8). We modify the original log-space reduction from
deciding whether a variable is in the minimal model of a definite Horn formula
so that the argument framework does not contain cycles, which are not allowed
in our setting. Let $\varphi=\\{r_{l}:b_{l,1}\wedge\dots\wedge
b_{l,i_{l}}\rightarrow h_{l}\mid 1\leq l\leq n\\}$ be a definite Horn formula
over the set of variables $X$, and let $z\in X$ be the variable we want to
decide whether it belongs to the minimal model of $\varphi$. We assume
w.l.o.g. that for every $r_{l}$, $h_{l}\neq b_{l,j}$ for all $j$.

We construct a DL-Litecore KB
$\mathcal{K}=\langle\mathcal{T},\mathcal{A}\rangle$ and priority relation as
follows.

$\displaystyle\mathcal{T}=$
$\displaystyle\\{\exists\mathit{FalseInBod}^{-}\sqsubseteq\neg\exists\mathit{SatBodHead},\exists\mathit{SatBodHead}^{-}\sqsubseteq\exists\mathit{FalseInBod},\exists\mathit{FalseInBod}\sqsubseteq\neg
T\\}$ $\displaystyle\mathcal{A}=$
$\displaystyle\\{\mathit{FalseInBod}(b_{l,j},r_{l})\mid r_{l}\in\varphi,1\leq
j\leq i_{l}\\}\cup\\{\mathit{SatBodHead}(r_{l},h_{l})\mid
r_{l}\in\varphi\\}\cup\\{T(z)\\}$
$\mathit{SatBodHead}(r_{l},x)\succ\mathit{FalseInBod}(x,r_{l^{\prime}})$

Clearly, $\succ$ is acyclic. We show that $T(z)$ belongs to the grounded
extension $\mathcal{G}$ of $F_{\mathcal{K},\succ}$ iff $z$ belongs to the
minimal model of $\varphi$. The corresponding AF
$F=(\mathcal{A},\rightsquigarrow_{\mathcal{K},\succ})$ of
$F_{\mathcal{K},\succ}$ is such that

$\displaystyle\rightsquigarrow_{\mathcal{K},\succ}=$
$\displaystyle\\{(\mathit{SatBodHead}(\\_,x),\mathit{FalseInBod}(x,\\_))\mid
x\in X\\}\cup$
$\displaystyle\\{(\mathit{SatBodHead}(r_{l},\\_),\mathit{FalseInBod}(\\_,r_{l})),(\mathit{FalseInBod}(\\_,r_{l}),\mathit{SatBodHead}(r_{l},\\_))\mid
r_{l}\in\varphi\\}\cup$
$\displaystyle\\{(T(z),\mathit{FalseInBod}(z,\\_)),(\mathit{FalseInBod}(z,\\_),T(z))\\}$

The intuition behind the reduction is that an argument
$\mathit{SatBodHead}(r_{l},x)$ is in $\mathcal{G}$ iff all variables in the
body of $r_{l}$ are in the minimal model of $\varphi$, so that $x$ is also in
this model, and that an argument $\mathit{FalseInBod}(x,\\_)$, stating that
$x$ is not in the model, is attacked by $\mathcal{G}$ only if $x$ is in the
model. That is, when computing $\mathcal{G}$ via iteratively applying the
characteristic function $\Gamma_{F}$ we simulate the following algorithm for
deciding whether $z$ is in the minimal model of $\varphi$. The algorithm
starts with the rules with empty body and adds their rule heads to the minimal
model: $\Gamma_{F}(\emptyset)=\\{\mathit{SatBodHead}(r_{l},x)\mid\text{there
is no }\mathit{FalseInBod}(\\_,r_{l})\in\mathcal{A}\\}\cup\\{T(z)\text{ if
there is no }\mathit{FalseInBod}(z,\\_)\in\mathcal{A}\\}$. Then it iteratively
considers all rules with the body already being part of the minimal model and
adds their heads to the minimal model until a fixed-point is reached: if
$G_{i}$ is the result at step $i$, let
$S_{i}=\\{\mathit{FalseInBod}(y,\\_)\mid\mathit{SatBodHead}(\\_,y)\in
G_{i}\\}$ be the set of arguments that are attacked by $G_{i}$,
$\Gamma_{F}(G_{i})=\\{\mathit{SatBodHead}(r_{l},x)\mid\text{there is no
}\mathit{FalseInBod}(\\_,r_{l})\in\mathcal{A}\setminus
S_{i}\\}\cup\\{T(z)\text{ if there is no
}\mathit{FalseInBod}(z,\\_)\in\mathcal{A}\setminus S_{i}\\}$. We then have
that $z$ is in the minimal model of the Horn-formula $\varphi$ iff
$T(z)\in\mathcal{G}$. This shows the P-hardness of assertion entailment as
well as of verifying $\mathcal{G}$. ∎

We recall the definition of well-founded semantics and introduce some notation
and terminology. Our presentation is loosely based upon Chapter 15 from (?),
but tailored (and simplified) to suit our purposes. We refer readers to the
latter chapter for a more detailed introduction to the semantics of rule
languages with negation.

A _normal logic program_ (aka Datalog¬ program, henceforth abbreviated to
program) is a finite set of _rules_ of the form
$\rho=\mathtt{h}\leftarrow\mathtt{b}_{1},\ldots,\mathtt{b}_{n},\neg\
\mathtt{b}_{n+1},\ldots,\neg\ \mathtt{b}_{n+m}$, where each $\mathtt{b}_{i}$
is an atom $\mathtt{p}(t_{1},\ldots,t_{n})$ whose every term $t_{i}$ is either
a constant or a variable. The atom $\mathtt{h}$ is called the head of the rule
$\rho$, and the body of $\rho$ is $\mathtt{b}_{1},\ldots,\mathtt{b}_{n},\neg\
\mathtt{b}_{n+1},\ldots,\neg\ \mathtt{b}_{n+m}$. The atoms
$\mathtt{b}_{1},\ldots,\mathtt{b}_{n}$ are called _positive body atoms_ ,
while the atoms $\mathtt{b}_{n+1},\ldots,\mathtt{b}_{n+m}$ (which are preceded
by $\neg$) are called _negative body atoms_. As is common, we require rules to
satisfy the following safety condition: every variable that appears in the
head atom of a rule must occur in some positive body atom of that rule. Note
that it is allowed for the body of a rule to be empty (empty ruleheads can
also be considered, but will not be used in what follows).

A _definite rule_ is a rule that does not contain any negative body atoms, and
a _definite program_ is a finite set of definite rules. A _ground atom (resp.
rule, program)_ is an atom (resp. rule, program) that does not contain any
variables. We will sometimes use the term _fact_ in place of _ground atom_.
Given any program $\Pi$, the _grounding of $\Pi$_, denoted $grnd(\Pi)$,
consists of all ground rules that can be obtained from a rule in $\Pi$ by
instantiating its variables with constants occurring in $\Pi$.

Given a ground program $\Pi$, we let $B_{\Pi}$ consist of all facts that
appear (positively or negatively) in $\Pi$. A _2-valued instance_ $\mathbf{I}$
for $\Pi$ assigns to each fact in $B_{\Pi}$ a value that is either true or
false. We denote by $\bot$ the 2-valued instance that assigns false to all
facts in $B_{\Pi}$. A _3-valued instance_ for $\Pi$ is defined similarly,
except now there are three possible values: true, unknown, or false. It will
be convenient to view 2-valued instances as sets of (positive) facts, where a
fact is assigned true if it belongs to the set, and otherwise, is assigned
false. Similarly, a 3-valued instance can be given as a consistent set of
literals (possibly negated facts), where facts appearing positively in the set
are assigned true, those whose negation is in the set are assigned false, and
all other facts are treated as unknown. We use the notation
$\mathbf{I}(\mathtt{a})$ to refer to the truth value that $\mathbf{I}$ assigns
to the fact $\mathtt{a}$.

Given two 3-valued instances $\mathbf{I}$ and $\mathbf{J}$, we write
$\mathbf{I}<\mathbf{J}$ to mean that
$\mathbf{I}(\mathtt{a})<\mathbf{J}(\mathtt{a})$ for ever ground atom
$\mathtt{a}$, where the truth values are ordered as follows: false $<$ unknown
$<$ true. A _(2-valued) model_ of a ground definite program $\Pi$ is a
2-valued instance for $\Pi$ such that for every rule $\rho\in\Pi$, if all body
atoms in $\rho$ are assigned true, then the head atom is also assigned true.
It is known that every ground definite program has a unique _minimal model_ ,
i.e., a model $\mathbf{I}$ such that $\mathbf{I}<\mathbf{J}$ for every model
$\mathbf{J}$. We denote by $mm(\Pi)$ the minimal model of a ground definite
program $\Pi$.

We next extend minimal models to stratified programs. A _stratification_ of a
program $\Pi$ is a sequence $\Pi^{1},\ldots,\Pi^{n}$ and a function $\sigma$
mapping predicates to $[1,n]$ such that the following conditions hold:

  * •

$\Pi$ is the disjoint union of $\Pi^{1},\ldots,\Pi^{n}$

  * •

for every predicate $P$ that occurs in $\Pi$, all rules that have $P$ in the
head belong to $\Pi^{\sigma(P)}$

  * •

for every $1\leq i\leq n$:

    * –

if predicate $P$ occurs positively in the body of some rule of $\Pi^{i}$, then
$\sigma(P)\leq i$

    * –

if predicate $P$ occurs negatively in the body of a rule of $\Pi^{i}$, then
$\sigma(P)<i$

A program $\Pi$ is stratified if there exists a stratification for $\Pi$.
Given a program $\Pi$ with stratification $\Pi^{1},\ldots,\Pi^{n}$, we proceed
as follows. We start by computing the grounding $grnd(\Pi)$, and let
$gr(\Pi^{1}),\ldots,gr(\Pi^{n})$ be the ground programs corresponding to
$\Pi^{1},\ldots,\Pi^{n}$ (note that they are grounded w.r.t. all constants
occurring in $\Pi$, not just the constants from the stratum). We set $M_{1}$
equal to the minimal model of the ground definite program $gr(\Pi^{1})$. Then
for $1\leq i<n$, we let $M_{i+1}=M_{i}\cup M^{\prime}_{i+1}$, where
$M^{\prime}_{i+1}$ is the minimal model of the ground definite program
obtained from $gr(\Pi^{i+1}$) by (i) deleting every rule whose body contains
$\neg\mathtt{a}$ where $\mathtt{a}\in M_{i}$, and (ii) removing all negative
facts from the remaining rule bodies. We call $M_{n}$ the minimal model of
$\Pi$.

We now proceed to the definition of the well-founded semantics, which can be
applied to arbitary programs. For every ground program $\Pi$ and 2-valued
instance111This construction in (?) was originally defined for 3-valued
instances, but as is noted there, only 2-valued instances are needed for the
fixpoint construction of the well-founded semantics. Focusing on 2-valued
instances simplifies some definitions. $\mathbf{I}$ for $\Pi$, we denote by
$\Pi|_{\mathbf{I}}$ the ground definite program that is obtained from $\Pi$ as
follows: (i) delete every rule whose body contains $\neg\mathtt{a}$ where
$\mathtt{a}\in\mathbf{I}$, (ii) remove all negative body atoms from the
remaining rules. We then consider the following infinite sequence of 2-valued
instances:

$\mathbf{I}_{0}=\bot\qquad\mathbf{I}_{i+1}=mm(\Pi|_{\mathbf{I}_{i}})$

It is known (and can be readily verified) that for every $i>0$, we have:

$\mathbf{I}_{0}<\mathbf{I}_{2}<\ldots<\mathbf{I}_{2i}<\mathbf{I}_{2i+2}<\mathbf{I}_{2i+1}<\mathbf{I}_{2i-1}<\ldots<\mathbf{I}_{1}$

As there are a finite number of possible instances, the sequences
$(\mathbf{I}_{2i})_{i\geq 0}$ and $(\mathbf{I}_{2i+1})_{i\geq 0}$ both reach a
fixpoint. We let $\mathbf{I}_{*}$ denote the limit of the increasing sequence
$(\mathbf{I}_{2i})_{i\geq 0}$, and let $\mathbf{I}^{*}$ denote the limit of
the decreasing sequence $(\mathbf{I}_{2i+1})_{i\geq 0}$. Then the (unique)
_well-founded model_ of $\Pi$ is the 3-valued instance that assigns true to
all facts $\mathtt{a}$ such that $\mathtt{a}\in\mathbf{I}_{*}$, assigns false
to all facts $\mathtt{a}$ such that $\mathtt{a}\not\in\mathbf{I}^{*}$, and
unknown to all other facts. If $\Pi$ is an arbitrary (not necessarily ground)
program, then the well-founded model of $\Pi$ is defined as the well-founded
model of $grnd(\Pi)$.

It is known that if $\Pi$ is stratified, then the well-founded model of $\Pi$
is equal to the minimal model of $\Pi$. More precisely, if $\Pi$ has a
stratification with $p$ levels, then $\mathbf{I}_{2p}$ is the minimal model,
and we have $\mathbf{I}_{2p}=\mathbf{I}_{2p+i}$ for all $i\geq 0$.

We recall the following result from (?) (very slightly modified to suit our
later extensions) that shows how to compute the grounded extension of an AF
via well-founded semantics. It makes reference to the following two rules:

$r_{\mathtt{acc}}:\mathtt{acc}(x)\leftarrow\mathtt{arg}(x),\neg\mathtt{def}(x)\qquad
r_{\mathtt{def}}:\mathtt{def}(x)\leftarrow\mathtt{attack}(y,x),\mathtt{acc}(y)$

######  Theorem 52.

Let $F=(\mathit{Args},\rightsquigarrow)$ be an AF. Then
$E\subseteq\mathit{Args}$ is the grounded extension of $F$ iff

$\\{\mathtt{acc}(\alpha),\neg\mathtt{def}(\alpha)\mid\alpha\in
E\\}\cup\\{\mathtt{def}(\beta),\neg\mathtt{acc}(\beta)\mid\beta\in
E^{+}\\}\cup\\{\mathtt{attack}(\alpha,\beta)\mid\alpha\rightsquigarrow\beta\\}\cup\\{\mathtt{arg}(\alpha)\mid\alpha\in\mathit{Args}\\}$

is the well-founded model of the program
$\\{r_{\mathtt{acc}},r_{\mathtt{def}}\\}\cup\\{\mathtt{attack}(\alpha,\beta)\leftarrow\,\mid\alpha\rightsquigarrow\beta\\}\cup\\{\mathtt{arg}(\alpha)\leftarrow\,\mid\alpha\in\mathit{Args}\\}$.

The following theorem generalizes the preceding result to $k$-SETAFs, i.e.,
SETAFs for which $S\rightsquigarrow\beta$ implies $|S|\leq k$. We will use
relations $\mathtt{attack}_{1},\ldots,\mathtt{attack}_{k}$ to store attacks,
where $\mathtt{attack}_{i}(\alpha_{1},\ldots,\alpha_{i},\beta)$ specifies that
there is an attack $\\{\alpha_{1},\ldots,\alpha_{i}\\}\rightsquigarrow\beta$.
We will use the following variants of rule $r_{\mathtt{def}}$, where $i$
ranges from $1$ to $k$:

$r_{\mathtt{def}}^{i}:\mathtt{def}(x)\leftarrow\mathtt{attack}_{i}(y_{1},\ldots,y_{i},x),\mathtt{acc}(y_{1}),\ldots,\mathtt{acc}(y_{i})$

Theorem 49. _Let $F=(\mathit{Args},\rightsquigarrow)$ be a $k$-SETAF. Then
$\alpha$ is in the grounded extension of $F$ iff $\mathtt{acc}(\alpha)$
belongs to the well-founded model of the following normal logic program:_

$\displaystyle\\{\mathtt{def}(x)\leftarrow\mathtt{att}_{i}(y_{1},..,y_{i},x),\mathtt{acc}(y_{1}),...,\mathtt{acc}(y_{i})\mid
1\leq i\leq
k\\}\cup\\{\mathtt{acc}(x)\leftarrow\mathtt{arg}(x),\neg\mathtt{def}(x)\\}$
$\displaystyle\cup\\{\mathtt{arg}(\alpha)\mid\alpha\in\mathit{Args}\\}\cup\\{\mathtt{att}_{i}(\alpha_{1},\ldots,\alpha_{i},\beta)\leftarrow\,\mid\\{\alpha_{1},\ldots,\alpha_{i}\\}\rightsquigarrow\beta\\}$

###### Proof.

Let
$\Pi_{F}=\\{r_{\mathtt{acc}},r_{\mathtt{def}}^{1},\ldots,r_{\mathtt{def}}^{k}\\}\cup\\{\mathtt{arg}(\alpha)\mid\alpha\in\mathit{Args}\\}\cup\\{\mathtt{attack}_{i}(\alpha_{1},\ldots,\alpha_{i},\beta)\leftarrow\,\mid\\{\alpha_{1},\ldots,\alpha_{i}\\}\rightsquigarrow\beta\\}$,
and let us consider the sequence of sets produced during the computation of
the well-founded model of $\Pi_{F}$. A straightforward inductive argument
shows that the following statements holds for every $j\geq 0$:

$\displaystyle\mathbf{I}_{2j+2}$ $\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in\Gamma_{F}^{j+1}(\emptyset)\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in(\Gamma_{F}^{j+1}(\emptyset))^{+}\\}$
$\displaystyle\mathbf{I}_{2j+1}$ $\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in\mathit{Args}\setminus(\Gamma_{F}^{j}(\emptyset))^{+}\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in(\mathit{Args}\setminus(\Gamma_{F}^{j}(\emptyset))^{+})^{+}\\}$

where $S_{\mathtt{arg}}=\\{\mathtt{arg}(\alpha)\mid\alpha\in\mathit{Args}\\}$,
$S_{\mathtt{attack}}=\\{\mathtt{attack}_{i}(\alpha_{1},\ldots,\alpha_{i},\beta)\mid\\{\alpha_{1},\ldots,\alpha_{i}\\}\rightsquigarrow\beta\\}$
and $(\Gamma_{F}^{0}(\emptyset))^{+}=\emptyset$. Recall that these are
2-valued instances, so we list the positive facts, with all other facts being
assigned false.

Now let $E$ be the grounded extension of $F$. Then there is $\ell$ such that
$E=\Gamma_{F}^{\ell}(\emptyset)$, and
$\Gamma_{F}^{\ell+j}(\emptyset)=\Gamma_{F}^{\ell}(\emptyset)$ for all $j\geq
1$. Then we have:

$\displaystyle\mathbf{I}_{*}$ $\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in\Gamma_{F}^{\ell}(\emptyset)\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in(\Gamma_{F}^{\ell}(\emptyset))^{+}\\}$
$\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in
E\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in E^{+}\\}$
$\displaystyle\mathbf{I}^{*}$ $\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in\mathit{Args}\setminus(\Gamma_{F}^{\ell}(\emptyset))^{+}\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in(\mathit{Args}\setminus(\Gamma_{F}^{\ell}(\emptyset))^{+})^{+}\\}$
$\displaystyle=S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha)\mid\alpha\in\mathit{Args}\setminus
E^{+}\\}\cup\\{\mathtt{def}(\beta)\mid\beta\in(\mathit{Args}\setminus
E^{+})^{+}\\}$

Note that if $\beta\not\in(\mathit{Args}\setminus E^{+})^{+}$, then for every
$S\rightsquigarrow\beta$, there exists $\gamma\in S$ such that $\gamma\in
E^{+}$. It follows that $\beta\in\Gamma_{F}(E)=E$. We therefore have that the
well-founded model of $\Pi_{F}$ is equal to

$S_{\mathtt{arg}}\cup
S_{\mathtt{attack}}\cup\\{\mathtt{acc}(\alpha),\neg\mathtt{def}(\alpha)\mid\alpha\in
E\\}\cup\\{\mathtt{def}(\beta),\neg\mathtt{acc}(\beta)\mid\beta\in E^{+}\\}$

which completes the proof. ∎

Next we need to define rules to compute conflicts, in order to derive which
attack facts should be included. We assume that we have a finite set
$Q_{\mathsf{unsat}}$ of BCQs such that $\mathcal{A}$ is
$\mathcal{T}$-consistent iff no $q\in Q_{\mathsf{unsat}}$ evaluates to true on
$\mathcal{A}$ (or more formally, on the interpretation
$\mathcal{I}_{\mathcal{A}}$ based upon $\mathcal{A}$). Note that when
$\mathcal{T}$ is formulated in DL-Lite${}^{\mathcal{H}}_{\mathsf{horn}}$, such
a set $Q_{\mathsf{unsat}}$ can be computed using standard query rewriting
procedures. In what follows, we let $N$ be the maximal number of conjuncts in
any BCQ in $Q_{\mathsf{unsat}}$.

To be able to identify conflicts, and later repairs, we assume that each
assertion has an additional final argument that contains a unique id for that
assertion, e.g. $A(a,u_{5}),R(a,b,u_{17})$. Given a (standard) ABox
$\mathcal{A}$, we will use $\mathcal{A}_{id}$ to denote a corresponding set of
annotated assertions, and for every $\alpha\in\mathcal{A}$, we let
$id(\alpha)$ be the id of the corresponding atom in $\mathcal{A}_{id}$. We
will store the priority relation in a binary relation $\mathtt{pref}$ over
assertion ids, with $\mathtt{pref}(id(\alpha),id(\beta))$ meaning that
$\alpha\succ\beta$. We let $Q_{\mathsf{unsat}}^{*}$ consist of all BCQs
$q^{*}$ that can be obtained from some $q\in Q_{\mathsf{unsat}}$ as follows:
(i) order the atoms in $q$, and (ii) add a final argument $z_{j}$ to the $j$th
atom (where $z_{j}$ is a fresh variable not occurring in $Q_{\mathsf{unsat}}$
and distinct from $z_{k}$ with $k\neq j$).

We introduce predicates $\mathtt{confl}_{i}$ for $i=1,\ldots,N$, which will
store conflicts that involve exactly $i$ assertions. Concretely, for each BCQ
$q^{*}\in Q_{\mathsf{unsat}}^{*}$ with a single atom we have the following
rule (which can be omitted if we assume no self-contradicting assertions):

$\mathtt{confl}_{0}(z_{1})\leftarrow q^{*}(z_{1})$

and for every BCQ $q^{*}\in Q_{\mathsf{unsat}}^{*}$ with $k+1$ atoms, we have:

$\mathtt{confl}_{k}(z_{1},\ldots,z_{k},z_{k+1})\leftarrow
q^{*}(z_{1},\ldots,z_{k},z_{k+1}),\bigwedge_{\begin{subarray}{c}0\leq j<k\\\
(z_{\ell_{1}},\ldots,z_{\ell_{j}},z_{\ell_{j+1}})\in\\{z_{1},\ldots,z_{k},z_{k+1}\\}^{j+1}\end{subarray}}\neg\mathtt{confl}_{j}(z_{\ell_{1}},\ldots,z_{\ell_{j}},z_{\ell_{j+1}})$

Here we write $q^{*}(z_{1},\ldots,z_{k})$ to highlight the shared variables
$z_{j}$, but $q^{*}$ will contain also the original variables in the BCQ $q$.
Observe that negated body atoms are used to ensure subset minimality. We can
then compute the attack relations by using the following rule for every $1\leq
i<N$:

$r_{\mathtt{att}}^{i}:\mathtt{attack}_{i}(z_{1},\ldots,z_{i},z_{i+1})\leftarrow\mathtt{confl}_{i}(z_{1},\ldots,z_{i},z_{i+1}),\neg\mathtt{pref}(z_{i+1},z_{1}),\ldots,\neg\mathtt{pref}(z_{i+1},z_{i})$

where We generate the set of arguments (corresponding to ids of assertions
that are not self-contradictory) by means of the following rules, for every
concept name $A$ and role name $R$:

$\mathtt{arg}(z_{1})\leftarrow
A(x,z_{1}),\neg\mathtt{confl}_{0}(z_{1})\qquad\mathtt{arg}(z_{1})\leftarrow
R(x,y,z_{1}),\neg\mathtt{confl}_{0}(z_{1})$

Let $\Pi_{\mathtt{confl}}$ be the preceding set of rules. We observe that
$\Pi_{\mathtt{confl}}$ is stratified. It is not hard to see that these rules
allow us to compute the conflicts, and hence the attacks in the SETAF
corresponding to the PSETAF $F_{\mathcal{K},\succ}$. Specifically, we have:

######  Lemma 53.

Let $F=(\mathit{Args},\rightsquigarrow_{\succ})$ be the corresponding SETAF
for the PSETAF $F_{\mathcal{K},\succ}$ based upon the prioritized KB
$\mathcal{K}_{\succ}$. The following statements are equivalent:

  1. 1.

$\\{\alpha_{1},\ldots,\alpha_{n}\\}\rightsquigarrow_{\succ}\beta$

  2. 2.

the atom $\mathtt{attack}_{n}(id(\alpha_{1}),\ldots,id(\alpha_{n}),id(\beta))$
belongs to the minimal model of
$\Pi_{\mathtt{confl}}\cup\\{\gamma\leftarrow\,\mid\gamma\in\mathcal{A}_{id}\\}\cup\\{\mathtt{pref}(id(\alpha),id(\beta))\mid\alpha\succ\beta\\}$.

Intuitively, we want to construct a program that first computes the minimal
model of the stratified program $\Pi_{\mathtt{confl}}$, then uses the attack
and conflict facts from this model as input for the ‘argumentation’ program

$\Pi_{\mathtt{arg}}=\\{r_{\mathtt{acc}},r_{\mathtt{def}}^{1},\ldots,r_{\mathtt{def}}^{N}\\}$

However, if we simply apply well-founded semantics to the combined program, we
might not get the desired result: while we are ‘waiting’ for the computation
of the stratified rules to finish, there could be some incorrectly derived
$\mathtt{confl}_{i}$ facts, which could lead to wrongly derived
$\mathtt{attack}$ and $\mathtt{def}$ facts, in turn wrongly eliminating some
$\mathtt{acc}$ facts.

The following lemma provides a means of safely combining the two programs to
achieve the desired result. The basic idea is to delay the application of
rules in the second program until the initial stratified program has
stabilized. We note that the lemma is tailored to our purposes, and some of
the hypotheses could be relaxed at the cost of a more involved proof.

######  Lemma 54.

Let $\Pi_{1}$ and $\Pi_{2}$ be programs verifying the following conditions:
(i) $\Pi_{1}$ is stratified and does not use any predicate / fact that occurs
in the head of a rule from $\Pi_{2}$, and (ii) $\Pi_{2}$ may only use
predicates / facts from $\Pi_{1}$ in the body of rules and in positive form.
Then we can construct a program $\Pi_{1\rightarrow 2}$ such that the following
models contain precisely the same (positive) facts over the relations in
$\Pi_{2}$:

  * •

the well-founded model of $\Pi_{1\rightarrow 2}$

  * •

the well-founded model of $\Pi_{2}\cup\\{\alpha\leftarrow\,\mid\alpha\in
mm(\Pi_{1})\\}$

###### Proof.

Suppose that $\Pi_{1}$ has a stratification with $p$ levels. Consider the
following auxiliary program:

$\Pi_{p}=\\{\mathtt{odd}(x)\leftarrow\mathtt{next}(y,x),\neg\mathtt{odd}(y)\\}\cup\\{\mathtt{next}(i,i+1)\leftarrow\,\mid
0\leq i<2p\\}$

We assume that the predicate names $\mathtt{odd},\mathtt{next}$ and constants
$0,1,\ldots,2p$ do not occur in either $\Pi_{1}$ or $\Pi_{2}$ (otherwise, we
can choose other fresh names / constants). A straightforward induction shows
that the following instances will be produced during the construction of the
well-founded model of $\Pi_{p}$:

$\displaystyle\mathbf{I}_{2j+2}$ $\displaystyle=\\{\mathtt{odd}(i)\mid 1\leq
i\leq 2p,i<2j+2,\text{ and }i\text{ is odd }\\}\cup\\{\mathtt{next}(i,i+1)\mid
0\leq i<2p\\}$ $\displaystyle\mathbf{I}_{2j+1}$
$\displaystyle=\\{\mathtt{odd}(i)\mid 1\leq i\leq 2p\text{ and either }i\text{
is odd or }i>2j+1\\}\cup\\{\mathtt{next}(i,i+1)\mid 0\leq i<p\\}$

In particular, this means that the instance $\mathbf{I}_{2p}$, and every later
instance in the sequence, contains

$\neg\mathtt{odd}(0),\mathtt{odd}(1),\neg\mathtt{odd}(2),\ldots,\mathtt{odd}(2p-1),\neg\mathtt{odd}(2p)$

but none of the earlier instances contains precisely this combination of
positive and negative facts.

Let us now modify the rules in $\Pi_{2}$ as follows: add
$\neg\mathtt{odd}(0),\mathtt{odd}(1),\neg\mathtt{odd}(2),\ldots,\mathtt{odd}(2p-1),\neg\mathtt{odd}(2p)$
to the body of each rule $r$ (denoting the result $r^{\prime}$). Let
$\Pi_{2}^{\prime}$ be the resulting set of rules.

Now consider the program $\Pi_{1\rightarrow
2}=\Pi_{1}\cup\Pi_{2}^{\prime}\cup\Pi_{p}$ and let
$\mathbf{J_{0}},\mathbf{J}_{1},\mathbf{J}_{2},\ldots$ be the sequence of
instances obtained during the construction of the well-founded model of
$grnd(\Pi_{1}\cup\Pi_{2}^{\prime}\cup\Pi_{p})$. We consider the three parts of
the program:

  * •

Sub-program $\Pi_{1}$: Due to the assumptions on $\Pi_{1}$, and the safety
condition on rules that ensures all head variables occur in a positive body
atom, it is not hard to show that for every $i\geq 2p$, $\mathbf{J}_{i}$
contains the same positive facts as the minimal model of $\Pi_{1}$, when
restricted to predicates and facts from $\Pi_{1}$. Specifically, we have:

    * –

every $\alpha\in mm(\Pi_{1})$ belongs to $\mathbf{J}_{i}$

    * –

if $\alpha\in\mathbf{J}_{i}$ and $\alpha$ uses a predicate from $\Pi_{1}$,
then $\alpha\in mm(\Pi_{1})$

  * •

Sub-program $\Pi_{p}$: The rule
$\mathtt{odd}(x)\leftarrow\mathtt{next}(y,x),\neg\mathtt{odd}(y)$ is guarded
by the predicate $\mathtt{next}$ which only occurs in $\Pi_{p}$ and which can
only match the concrete facts given in $\Pi_{p}$. It follows that
$\mathbf{J}_{i}$ and $\mathbf{I}_{i}$ contain precisely the same positive
$\mathtt{odd}$ and $\mathtt{next}$ facts for every $i\geq 0$. In particular,
the set of literals
$\\{\neg\mathtt{odd}(0),\mathtt{odd}(1),\neg\mathtt{odd}(2),\ldots,\mathtt{odd}(2p-1),\neg\mathtt{odd}(2p)\\}$
belongs to $\mathbf{J}_{i}$ for every $i\geq 2p$, and it is not contained in
$\mathbf{J}_{i}$ for $i<2p$.

  * •

Sub-program $\Pi_{2}^{\prime}$: Every rule in $\Pi_{2}^{\prime}$ contains
$\neg\mathtt{odd}(0),\mathtt{odd}(1),\neg\mathtt{odd}(2),\ldots,\mathtt{odd}(2p-1),\neg\mathtt{odd}(2p)$
in its body. It follows from the preceding point that this set of literals is
not contained in $\mathbf{J}_{i}$ for $i<2p$. Thus, for $i<2p$, the rules of
$\Pi_{2}^{\prime}$ cannot fire. For every $i\geq 2p$, the set of literals
$\\{\neg\mathtt{odd}(0),\mathtt{odd}(1),\neg\mathtt{odd}(2),\ldots,\mathtt{odd}(2p-1),\neg\mathtt{odd}(2p)\\}$
belongs to $\mathbf{J}_{i}$, so the rules in $\Pi_{2}^{\prime}$ behave
henceforth like the original rules in $\Pi_{2}$. Moreover, as noted above,
when $i\geq 2p$, the instance $\mathbf{J}_{i}$ contains the same facts as
$mm(\Pi_{1})$ w.r.t. predicates / facts from $\Pi_{1}$, so the same rule
applications that were possible using $\\{\alpha\leftarrow\,\mid\alpha\in
mm(\Pi_{1})\\}$ can be reproduced in $\Pi_{1\rightarrow 2}$ starting from
timepoint $2p$. Conversely, due to the safety condition on $\Pi_{2}$, all
applications of rules from $\Pi_{2}^{\prime}$ used to generate the instances
$\mathbf{J}_{2p},\mathbf{J}_{2p+1},\ldots$ can be reproduced by the program
$\Pi_{2}\cup\\{\alpha\leftarrow\,\mid\alpha\in mm(\Pi_{1})\\}$. It follows
that the well-founded model of $\Pi_{1\rightarrow 2}$ and the well-founded
model of $\Pi_{2}\cup\\{\alpha\leftarrow\,\mid\alpha\in mm(\Pi_{1})\\}$
contain precisely the same positive facts when restricted to the relations /
facts in $\Pi_{2}$. ∎

It is easily verified that $\Pi_{\mathtt{confl}}$ and $\Pi_{\mathtt{arg}}$
satisfy the conditions of programs $\Pi_{1}$ and $\Pi_{2}$ of the preceding
lemma. We can therefore combine Theorem 49 and Lemmas 53 and 54 to obtain the
following result. While stated for DL-Lite${}^{\mathcal{H}}_{\mathsf{horn}}$,
the result holds for any constraint / ontology language for which conflicts
can be identified by a finite set of CQs that depends solely on the ontology /
constraints.

See 50

A natural under-approximation of the grounded extension is obtained by
considering $\Gamma_{F}^{d}(\emptyset)$ for some fixed number $d$. We describe
how to adapt the preceding program to compute such an approximation.
Essentially, we need to replace the rules
$r_{\mathtt{acc}},r_{\mathtt{def}}^{i}$ by the following stratified set of
rules (recall that $N$ is the maximal cardinality of conflicts):

$\displaystyle\mathtt{acc}_{1}(x)$ $\displaystyle\leftarrow\mathtt{arg}(x)$
$\displaystyle\mathtt{def}_{1}(x)$
$\displaystyle\leftarrow\mathtt{attack}_{i}(y_{1},\ldots,y_{i},x),\mathtt{acc}_{1}(y_{1}),\ldots,\mathtt{acc}_{1}(y_{i})$
$\displaystyle 1\leq i<N$ $\displaystyle\mathtt{acc}_{j+1}(x)$
$\displaystyle\leftarrow\mathtt{arg}(x),\neg\mathtt{def}_{j}(x)$
$\displaystyle 1\leq j<2d$ $\displaystyle\mathtt{def}_{j+1}(x)$
$\displaystyle\leftarrow\mathtt{attack}_{i}(y_{1},\ldots,y_{i},x),\mathtt{acc}_{j+1}(y_{1}),\ldots,\mathtt{acc}_{j+1}(y_{i})$
$\displaystyle 1\leq j<2d,1\leq i<N$

It is easily verified that the preceding rules behave exactly like
$r_{\mathtt{acc}},r_{\mathtt{def}}^{i}$ for the first $2d$ iterations. To make
this more formal, let $\Pi_{\mathtt{arg}}^{d}$ be the preceding rules.
Consider some ABox $\mathcal{A}$, a priority relation $\succ$ between facts in
$\mathcal{A}$, and define $S_{\mathcal{A},\succ}$ as follows:

$S_{\mathcal{A},\succ}=\\{\gamma\leftarrow\,\mid\gamma\in\mathcal{A}_{id}\\}\cup\\{\mathtt{pref}(id(\alpha),id(\beta))\leftarrow\,\mid\alpha\succ\beta\\}$

Now let $\mathbf{K}_{0},\mathbf{K}_{1},\ldots$ and
$\mathbf{L}_{0},\mathbf{L}_{1},\ldots$ be respectively the sequence of
instances generated during the computation of the well-founded models of
$\\{r_{\mathtt{acc}}\\}\cup\\{r_{\mathtt{def}}^{i},1\leq i\leq N\\}\cup
S_{\mathcal{A},\succ}$ and $\Pi_{\mathtt{arg}}^{d}\cup S_{\mathcal{A},\succ}$
respectively. Then for every $1\leq j\leq 2d$, we have the following:

  * •

$\mathtt{acc}_{j}(\alpha)\in\mathbf{L}_{j}$ iff
$\mathtt{acc}(\alpha)\in\mathbf{K}_{j}$

  * •

$\mathtt{def}_{j}(\alpha)\in\mathbf{L}_{j}$ iff
$\mathtt{def}(\alpha)\in\mathbf{K}_{j}$

Thus, by combining the $\Pi_{\mathtt{arg}}^{d}$ with the program
$\Pi_{\mathtt{confl}}$, we obtain a stratified program whose minimal model
contains $\mathtt{acc}_{2d}(id(\alpha))$ iff
$\alpha\in\Gamma_{F_{\mathcal{K},\succ}}^{d}(\emptyset)$. Moreover, by
examining the program, we remark that there is no recursion inside the strata
of the program. It is known that every non-recursive stratified datalog query
can be equivalently expressed as a first-order query, essentially by
‘unfolding’ the rules starting from a chosen goal predicate. We thus obtain:

######  Theorem 55.

For every DL-Lite${}^{\mathcal{H}}_{\mathsf{horn}}$ TBox $\mathcal{T}$ and
$d>0$, there exists a first-order query $\Psi_{\mathcal{T},d}$ with one free
variable such that for every ABox $\mathcal{A}$, priority relation $\succ$ for
$\mathcal{K}=\langle\mathcal{T},\mathcal{A}\rangle$, and assertion $\alpha$,
the following are equivalent:

  * •

$\alpha$ belongs to $\Gamma_{F_{\mathcal{K},\succ}}^{d}(\emptyset)$

  * •

$\Psi_{\mathcal{T},d}(id(\alpha))$ evaluates to true over the finite first-
order interpretation corresponding to
$\mathcal{A}_{id}\cup\\{\mathtt{pref}(id(\alpha),id(\beta))\mid\alpha\succ\beta\\}$.

##  Appendix D Comparison with Related Work

Let $\trianglerighteq$ be a partial preorder (i.e. a reflexive and transitive
binary relation) over the ABox $\mathcal{A}$ of a KB $\mathcal{K}$. We show
that the preferred repair
$\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)$ defined in (?) is
precisely the intersection of the completion-optimal repairs of
$\mathcal{K}_{\succ_{\trianglerighteq}}$ where
$\alpha\succ_{\trianglerighteq}\beta$ iff $\\{\alpha,\beta\\}\subseteq
C\in\mathit{Conf}(\mathcal{K})$ and $\alpha\triangleright\beta$ (i.e.
$\alpha\trianglerighteq\beta$ and $\beta\ntrianglerighteq\alpha$).

We first recall the definition of
$\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)$. Observe that given a
total preorder $\geq$ over $\mathcal{A}$, $\succ_{\geq}$ is score-structured,
so the three families of optimal repairs collapse. We denote by
$\mathit{OptRep}(\mathcal{K},\geq)$ the set
$\mathit{CRep}(\mathcal{K}_{\succ_{\geq}})=\mathit{GRep}(\mathcal{K}_{\succ_{\geq}})=\mathit{PRep}(\mathcal{K}_{\succ_{\geq}})$.
The repairs in $\mathit{OptRep}(\mathcal{K},\geq)$ correspond to the preferred
repairs used in (?), which are the $\subseteq_{P}$-repairs of (?) defined with
the priority levels naturally associated with $\geq$.

######  Definition 56.

Let $\geq$ be a total preorder that extends $\trianglerighteq$, i.e. such that
for every $\alpha,\beta\in\mathcal{A}$, if $\alpha\trianglerighteq\beta$, then
$\alpha\geq\beta$, and if $\alpha\triangleright\beta$, then $\alpha>\beta$.
The intersection of preferred repairs associated with $(\mathcal{K},\geq)$ is
$\mathit{IPR}(\mathcal{K},\geq)=\bigcap_{\mathcal{A}^{\prime}\in\mathit{OptRep}(\mathcal{K},\geq)}\mathcal{A}^{\prime}$.

The preferred repair associated with $(\mathcal{K},\trianglerighteq)$ is:
$\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)=\bigcap_{\geq\text{total
extension of }\trianglerighteq}\mathit{IPR}(\mathcal{K},\geq)$.

######  Theorem 57.

For every KB $\mathcal{K}=\langle\mathcal{T},\mathcal{A}\rangle$ and partial
preorder $\trianglerighteq$ over $\mathcal{A}$,
$\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)=\bigcap_{\mathcal{A}^{\prime}\in\mathit{CRep}(\mathcal{K},\succ_{\trianglerighteq})}\mathcal{A}^{\prime}$,
where $\alpha\succ_{\trianglerighteq}\beta$ iff $\\{\alpha,\beta\\}\subseteq
C\in\mathit{Conf}(\mathcal{K})$ and $\alpha\triangleright\beta$.

###### Proof.

Let
$\mathcal{A}^{\cap,C,\succ_{\trianglerighteq}}=\bigcap_{\mathcal{A}^{\prime}\in\mathit{CRep}(\mathcal{K},\succ_{\trianglerighteq})}\mathcal{A}^{\prime}$
be the intersection of the completion-optimal repairs of
$\mathcal{K}_{\succ_{\trianglerighteq}}$.

Let $\alpha_{0}\in\mathcal{A}^{\cap,C,\succ_{\trianglerighteq}}$, let $\geq$
be a total preorder that extends $\trianglerighteq$ and
$\mathcal{A}^{\prime}\in\mathit{OptRep}(\mathcal{K},\geq)$. For every
$\alpha,\beta$, if $\alpha{\succ_{\trianglerighteq}}\beta$, then
$\\{\alpha,\beta\\}\subseteq C\in\mathit{Conf}(\mathcal{K})$ and
$\alpha\triangleright\beta$, so since $\geq$ extends $\trianglerighteq$,
$\alpha>\beta$, i.e. $\alpha\succ_{\geq}\beta$. It follows that $\succ_{\geq}$
extends $\succ_{\trianglerighteq}$. Hence, the completion-optimal repairs of
$\mathcal{K}_{\succ_{\geq}}$ form a subset of the completion-optimal repairs
of $\mathcal{K}_{\succ_{\trianglerighteq}}$, so their intersections are
related as follows:
$\bigcap_{\mathcal{A}^{\prime}\in\mathit{CRep}(\mathcal{K},\succ_{\trianglerighteq})}\mathcal{A}^{\prime}\subseteq\bigcap_{\mathcal{A}^{\prime}\in\mathit{CRep}(\mathcal{K},\succ_{\geq})}\mathcal{A}^{\prime}$.
It follows that
$\alpha_{0}\in\bigcap_{\mathcal{A}^{\prime}\in\mathit{CRep}(\mathcal{K},\succ_{\geq})}\mathcal{A}^{\prime}=\bigcap_{\mathcal{A}^{\prime}\in\mathit{OptRep}(\mathcal{K},\geq)}\mathcal{A}^{\prime}=\mathit{IPR}(\mathcal{K},\geq)$.
Hence, for every total preorder $\geq$ that extends $\trianglerighteq$,
$\alpha_{0}\in\mathit{IPR}(\mathcal{K},\geq)$. It follows that
$\alpha_{0}\in\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)$. We
conclude that
$\mathcal{A}^{\cap,C,\succ_{\trianglerighteq}}\subseteq\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)$.

In the other direction, let
$\alpha_{0}\in\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)$ and let
$\succ^{\prime}$ be a completion of $\succ_{\trianglerighteq}$ and
$\mathcal{A}_{\succ^{\prime}}$ be the unique optimal repair defined by
$\succ^{\prime}$. Let $\geq$ be a total preorder that extends the preorder
$\geq^{\prime}$ defined as follows: $\alpha\geq^{\prime}\beta$ if (i)
$\alpha\trianglerighteq\beta$ or (ii) $\alpha\succ^{\prime}\beta$. We show
that $\geq$ extends $\trianglerighteq$. If $\alpha\trianglerighteq\beta$ then
$\alpha\geq^{\prime}\beta$ so $\alpha\geq\beta$. Assume that
$\alpha\triangleright\beta$. If $\alpha$ and $\beta$ are in a conflict,
$\alpha\succ_{\trianglerighteq}\beta$ so $\alpha\succ^{\prime}\beta$ and
$\beta\not\succ^{\prime}\alpha$ by definition of a completion of a priority
relation. If $\alpha$ and $\beta$ are not conflicting,
$\beta\not\succ^{\prime}\alpha$ trivially. Since
$\beta\not\trianglerighteq\alpha$ and $\beta\not\succ^{\prime}\alpha$, it
follows that $\beta\not\geq^{\prime}\alpha$. Hence $\alpha>^{\prime}\beta$, so
$\alpha>\beta$ since $\geq$ extends $\geq^{\prime}$. It follows that $\geq$
extends $\trianglerighteq$. Thus
$\alpha_{0}\in\mathit{IPR}(\mathcal{K},\geq)$. We show that
$\mathcal{A}_{\succ^{\prime}}\in\mathit{OptRep}(\mathcal{K},\geq)$, which
implies that
$\mathit{IPR}(\mathcal{K},\geq)\subseteq\mathcal{A}_{\succ^{\prime}}$, so that
$\alpha_{0}\in\mathcal{A}_{\succ^{\prime}}$. Since
$\mathit{OptRep}(\mathcal{K},\geq)=\mathit{CRep}(\mathcal{K}_{\succ_{\geq}})$,
it is sufficient to show that $\succ^{\prime}$ is a completion of
$\succ_{\geq}$. Let $\alpha\succ_{\geq}\beta$. By definition of
$\succ_{\geq}$, $\alpha$ and $\beta$ are in a conflict and $\alpha>\beta$.
Since $\succ^{\prime}$ is a total priority relation and $\alpha$, $\beta$ are
in a conflict, it must be the case that $\alpha\succ^{\prime}\beta$ or
$\beta\succ^{\prime}\alpha$. However, $\beta\not\succ^{\prime}\alpha$. Indeed,
otherwise $\beta\geq^{\prime}\alpha$ by construction of $\geq^{\prime}$, and
since $\geq$ extends $\geq^{\prime}$, it follows that $\beta\geq\alpha$,
contradicting $\alpha>\beta$. Hence $\alpha\succ^{\prime}\beta$. It follows
that $\succ^{\prime}$ is indeed a completion of $\succ_{\geq}$, so that
$\alpha_{0}\in\mathcal{A}_{\succ^{\prime}}$. We conclude that
$\mathit{Partial}_{PR}(\mathcal{K},\trianglerighteq)\subseteq\mathcal{A}^{\cap,C,\succ_{\trianglerighteq}}$.
∎