# Strong Equivalence for Epistemic Logic Programs Made Easy (Extended Version)

Wolfgang Faber  Michael Morak
Alpen-Adria-Universität Klagenfurt
Klagenfurt, Austria Stefan Woltran
TU Wien
Vienna, Austria

###### Abstract

Epistemic Logic Programs (ELPs), that is, Answer Set Programming (ASP)
extended with epistemic operators, have received renewed interest in recent
years, which led to a flurry of new research, as well as efficient solvers. An
important question is under which conditions a sub-program can be replaced by
another one without changing the meaning, in any context. This problem is
known as strong equivalence, and is well-studied for ASP. For ELPs, this
question has been approached by embedding them into epistemic extensions of
equilibrium logics. In this paper, we consider a simpler, more direct
characterization that is directly applicable to the language used in state-of-
the-art ELP solvers. This also allows us to give tight complexity bounds,
showing that strong equivalence for ELPs remains coNP-complete, as for ASP. We
further use our results to provide syntactic characterizations for
tautological rules and rule subsumption for ELPs.

##  1 Introduction

Epistemic Logic Programs (ELPs) are an extension of the well-established
formalism of Answer Set Programming (ASP), a generic, fully declarative logic
programming language that allows for encoding problems such that the resulting
answers (called _answer sets_) directly correspond to solutions of the encoded
problem (?; ?). Negation in ASP is generally interpreted according to the
stable model semantics (?), that is, as negation-as-failure, also called
default negation. Such a default negation $\neg a$ of an atom $a$ is true if
there is no justification for $a$ in the same answer set, making it a “local”
operator in the sense that it is defined relative to one considered answer
set. ELPs (in the version of (?)), on the other hand, extend ASP with the
epistemic negation operator $\mathbf{not}\,$ that allows for a form of meta-
reasoning, that is, reasoning over multiple answer sets. Intuitively, an
epistemically negated atom $\mathbf{not}\,a$ expresses that $a$ cannot be
_proven_ true, meaning that it is not true in every answer set. Thus,
epistemic negation is defined relative to a collection of answer sets,
referred to as a _world view_. Deciding whether a world view exists, is
$\Sigma_{\mathit{P}}^{\mathit{3}}$-complete (?), one level higher on the
polynomial hierarchy than deciding answer set existence (?).

? (?; ?) recognized epistemic negation as a desired construct for ASP early on
and introduced the modal operators $\mathbf{K}$ (“known” or “provably true”)
and $\mathbf{M}$ (“possible” or “not provably false”) to address this.
$\mathbf{K}a$ and $\mathbf{M}a$ correspond to $\neg\mathbf{not}\,a$ and
$\mathbf{not}\,\neg a$, respectively. Renewed interest in recent years has
revealed several flaws in the original semantics, and various new approaches
(cf. e.g. (?; ?; ?; ?; ?)) were proposed. Also the development of ELP solving
systems (?; ?; ?) has gained momentum.

A main application and major motivation of ELPs is the formalization of the
Closed World Assumption (CWA), as pointed out already by ? (?). Interestingly,
there are two formalizations of the CWA using ELPs in the literature. The
first, given in (?)111? (?) proposed the rule
$\mathbf{\sim}\,p\leftarrow\neg\mathbf{M}p$, where $\mathbf{\sim}\,$ is a
third kind of negation, usually referred to as strong negation, not considered
in this paper. It can be simulated by replacing occurrences of
$\mathbf{\sim}\,p$ by a fresh atom $p^{\prime}$ and adding a constraint rule
$\leftarrow p,p^{\prime}$ that excludes $p$ and $p^{\prime}$ to hold
simultaneously. , shall be referred to as Gelfond-CWA and introduces one rule
for each atom $p$:

$p^{\prime}\leftarrow\neg\mathbf{not}\,\neg p.$ (1)

Intuitively, this says that $p^{\prime}$ (i.e. the negation of $p$) shall be
true if there is no possible world where $p$ is true. ? (?) propose a
different rule for CWA, which we will refer to as Shen-Eiter-CWA for $p$:

$p^{\prime}\leftarrow\mathbf{not}\,p.$ (2)

Again, intuitively, this formulation makes $p^{\prime}$ true iff there is a
possible world where $p$ is false.

A natural question is whether $(\ref{eq:gelfond-cwa})$ and $(\ref{eq:shen-
eiter-cwa})$ yield the same results in any context, which will be answered in
this paper. To this end, we study notions of equivalence between ELPs. For
instance, two ELPs $\Pi_{1}$ and $\Pi_{2}$ are strongly ELP-WV-equivalent iff,
for any third ELP $\Pi$, the combined programs $\Pi_{1}\cup\Pi$ and
$\Pi_{2}\cup\Pi$ are equivalent (i.e. have the same world views). This notion
is useful to transform ELPs into equivalent versions where one wants to verify
that a local change preserves equivalence without considering the whole
program. Other notions of strong equivalence can be defined for comparing
candidate world views (rather than world views) or considering only the
addition of programs that do not contain epistemic operators. In (plain) ASP,
strong equivalence is a well-studied problem. ? (?) have provided an elegant
characterization of the problem in terms of Heyting’s logic of here-and-there
(HT). Strong equivalence also proved useful as a means to simplify programs
(?; ?; ?).

It has been shown in (?) and (?), among others, that epistemic extensions of
logic HT can be used to characterize strong equivalence of ELPs. These
approaches, however, are very general and lead to a very abstract
characterization that cannot be immediately used for ELPs written in the
language of current solving systems. It is also not easy to obtain tight
complexity results in such a general setting. The semantics considered in (?)
is the original one of (?), which is now considered obsolete, while (?)
consider a different semantics from the one in (?), which is what we use. An
in-depth comparison of the differences in the semantics can also be found in
(?).

In this paper, we therefore propose a simpler, more direct characterization
for the well-understood ELP semantics given in (?). Our characterization is in
the spirit of (?), which is useful to study ELPs written in the input language
of the ELP solvers mentioned above, as it can be directly applied in this
setting. This also allows us to obtain tight complexity bounds for checking
strong equivalence of ELPs. We further investigate several use cases of strong
equivalence by using our technique to syntactically characterize tautological
rules and rule subsumptions.

#### Contributions.

The main contributions of this paper are the following:

  * •

We propose different notions of strong equivalence of ELPs (based on the input
language of ELP solvers) that strictly generalize strong equivalence for plain
ASP.

  * •

We provide a model-theoretic characterization of strong equivalence for ELPs
showing that the different notions proposed coincide.

  * •

We use our characterization to show that, surprisingly, testing strong
equivalence of two ELPs remains in coNP, that is, the complexity of this test
does not increase when considering ELPs instead of plain ASP.

  * •

Finally, we use our proposed notion to syntactically characterize tautological
ELP rules and when one ELP rule subsumes another.

##  2 Preliminaries

#### Answer Set Programming (ASP).

A _ground logic program_ with nested negation (also called answer set program,
ASP program, or, simply, logic program) is a pair
$\Pi=(\mathcal{A},\mathcal{R})$, where $\mathcal{A}$ is a set of propositional
(i.e. ground) atoms and $\mathcal{R}$ is a set of rules of the form

$a_{1}\vee\cdots\vee a_{l}\leftarrow
a_{l+1},\ldots,a_{m},\neg\ell_{1},\ldots,\neg\ell_{n};$ (3)

where the comma symbol stands for conjunction, $0\leq l\leq m$, $0\leq n$,
$a_{i}\in\mathcal{A}$ for all $1\leq i\leq m$, and each $\ell_{i}$ is a
_literal_ , that is, either an atom $a$ or its (default) negation $\neg a$ for
any atom $a\in\mathcal{A}$. Note that, therefore, doubly negated atoms may
occur. We will sometimes refer to such rules as _standard rules_. Each rule
$r\in\mathcal{R}$ of form (3) consists of a _head_
${\mathit{H}(r)}=\\{a_{1},\ldots,a_{l}\\}$ and a _body_
${\mathit{B}(r)}=\\{a_{l+1},\ldots,a_{m},\neg\ell_{1},\ldots,\neg\ell_{n}\\}$.
We denote the _positive_ body by
${\mathit{B}^{+}(r)}=\\{a_{l+1},\ldots,a_{m}\\}$.

An _interpretation_ $I$ (over $\mathcal{A}$) is a set of atoms, that is,
$I\subseteq\mathcal{A}$. A literal $\ell$ is true in an interpretation
$I\subseteq\mathcal{A}$, denoted $I\vDash\ell$, if $a\in I$ and $\ell=a$, or
if $a\not\in I$ and $\ell=\neg a$; otherwise $\ell$ is false in $I$, denoted
$I\not\vDash\ell$. Finally, for some literal $\ell$, we define that
$I\vDash\neg\ell$ if $I\not\vDash\ell$. This notation naturally extends to
sets of literals. An interpretation $M$ is called a _model_ of $r$, denoted
$M\vDash r$, if, whenever $M\vDash{\mathit{B}(r)}$, it holds that
$M\vDash{\mathit{H}(r)}$. We denote the set of models of $r$ by
$\mathit{mods}(r)$; the models of a logic program
$\Pi=(\mathcal{A},\mathcal{R})$ are given by
$\mathit{mods}(\Pi)=\bigcap_{r\in\mathcal{R}}\mathit{mods}(r)$. We also write
$I\vDash r$ (resp. $I\vDash\Pi$) if $I\in\mathit{mods}(r)$ (resp.
$I\in\mathit{mods}(\Pi)$).

The GL-reduct $\Pi^{I}$ of a logic program $\Pi=(\mathcal{A},\mathcal{R})$
with respect to an interpretation $I$ is the program
$(\mathcal{A},\mathcal{R}^{I})$, where
$\mathcal{R}^{I}=\\{{\mathit{H}(r)}\leftarrow{\mathit{B}^{+}(r)}\mid
r\in\mathcal{R},\forall\neg\ell\in{\mathit{B}(r)}:I\vDash\neg\ell\\}$.

######  Definition 1.

(?; ?; ?) $M\subseteq\mathcal{A}$ is an _answer set_ of a logic program $\Pi$
if (1) $M\in\mathit{mods}(\Pi)$ and (2) there is no subset $M^{\prime}\subset
M$ such that $M^{\prime}\in\mathit{mods}(\Pi^{M})$.

The set of answer sets of a logic program $\Pi$ is denoted by
$\mathit{AS}(\Pi)$. The _consistency problem_ of ASP, that is, to decide
whether for a given logic program $\Pi$ it holds that
$\mathit{AS}(\Pi)\neq\emptyset$, is
$\Sigma_{\mathit{P}}^{\mathit{2}}$-complete (?), and remains so also in the
case where doubly negated atoms are allowed in rule bodies (?).

#### Strong Equivalence for Logic Programs.

Two logic programs $\Pi_{1}=(\mathcal{A},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A},\mathcal{R}_{2})$ are _equivalent_ iff they have the
same set of answer sets, that is, $\mathit{AS}(\Pi_{1})=\mathit{AS}(\Pi_{2})$.
The two logic programs are _strongly equivalent_ iff for any third logic
program $\Pi=(\mathcal{A},\mathcal{R})$ it holds that the combined logic
program $\Pi_{1}\cup\Pi=(\mathcal{A},\mathcal{R}_{1}\cup\mathcal{R})$ is
equivalent to the combined logic program
$\Pi_{2}\cup\Pi=(\mathcal{A},\mathcal{R}_{2}\cup\mathcal{R})$. Note that
strong equivalence implies equivalence, since the empty program
$\Pi=(\mathcal{A},\emptyset)$ would already contradict strong equivalence for
two non-equivalent programs $\Pi_{1}$ and $\Pi_{2}$.

An _SE-model_ (?) of a logic program $\Pi=(\mathcal{A},\mathcal{R})$ is a
tuple $(X,Y)$, where $X\subseteq Y\subseteq\mathcal{A}$, $Y\vDash\Pi$, and
$X\vDash\Pi^{Y}$. The set of SE-models of a logic program $\Pi$ is denoted
$\mathcal{S}\mathcal{E}(\Pi)$. Note that for every model $Y$ of $\Pi$, $(Y,Y)$
is an SE-model of $\Pi$, since $Y\vDash\Pi$ implies that $Y\vDash\Pi^{Y}$.

Two logic programs (over the same atoms) are strongly equivalent iff they have
the same SE-models (?; ?). Checking whether two logic programs are strongly
equivalent is coNP-complete (?; ?).

#### Epistemic Logic Programs.

An _epistemic literal_ is a formula $\mathbf{not}\,\ell$, where $\ell$ is a
literal and $\mathbf{not}\,$ is the epistemic negation operator. A _ground
epistemic logic program (ELP)_ is a triple
$\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$, where $\mathcal{A}$ is a set of
propositional atoms, $\mathcal{E}$ is a set of epistemic literals over the
atoms $\mathcal{A}$, and $\mathcal{R}$ is a set of _ELP rules_ , which are

$a_{1}\vee\cdots\vee
a_{k}\leftarrow\ell_{1},\ldots,\ell_{m},\xi_{1},\ldots,\xi_{j},\neg\xi_{j+1},\ldots,\neg\xi_{n},$

where each $a_{i}\in\mathcal{A}$ is an atom, each $\ell_{i}$ is a literal, and
each $\xi_{i}\in\mathcal{E}$ is an epistemic literal. Note that usually
$\mathcal{E}$ is defined implicitly to be the set of all epistemic literals
appearing in the rules $\mathcal{R}$; however, making the domain of epistemic
literals explicit will prove useful for our purposes. The _union_ of two ELPs
$\Pi_{1}=(\mathcal{A}_{1},\mathcal{E}_{1},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A}_{2},\mathcal{E}_{2},\mathcal{R}_{2})$ is the ELP
$\Pi_{1}\cup\Pi_{2}=(\mathcal{A}_{1}\cup\mathcal{A}_{2},\mathcal{E}_{1}\cup\mathcal{E}_{2},\mathcal{R}_{1}\cup\mathcal{R}_{2})$.

For a set $\mathcal{E}$ of epistemic literals, a subset
$\Phi\subseteq\mathcal{E}$ of epistemic literals is called an _epistemic
guess_ (or, simply, a _guess_). The following definition provides a way to
check whether a set of interpretations is compatible with a guess $\Phi$.

######  Definition 2.

Let $\mathcal{A}$ be a set of atoms, $\mathcal{E}$ be a set of epistemic
literals over $\mathcal{A}$, and $\Phi\subseteq\mathcal{E}$ be an epistemic
guess. A set $\mathcal{I}$ of interpretations over $\mathcal{A}$ is called
_$\Phi$ -compatible w.r.t. $\mathcal{E}$_, iff

  1. 1.

$\mathcal{I}\neq\emptyset$;

  2. 2.

for each epistemic literal $\mathbf{not}\,\ell\in\Phi$, there exists an
interpretation $I\in\mathcal{I}$ such that $I\not\vDash\ell$; and

  3. 3.

for each epistemic literal $\mathbf{not}\,\ell\in\mathcal{E}\setminus\Phi$,
for all interpretations $I\in\mathcal{I}$ it holds that $I\vDash\ell$.

For an ELP $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$, the _epistemic reduct_
(?) of the program $\Pi$ w.r.t. a guess $\Phi$, denoted $\Pi^{\Phi}$, consists
of the rules $\mathcal{R}^{\Phi}=\\{r^{\neg}\mid r\in\mathcal{R}\\}$, where
$r^{\neg}$ is defined as the rule $r\in\mathcal{R}$ where all occurrences of
epistemic literals $\mathbf{not}\,\ell\in\Phi$ are replaced by $\top$, and all
remaining epistemic negation symbols $\mathbf{not}\,$ are replaced by default
negation $\neg$. Note that, after this transformation,
$\Pi^{\Phi}=(\mathcal{A},\mathcal{R}^{\Phi})$ is a logic program without
epistemic negation222In fact, $\Pi^{\Phi}$ may contain triple-negated atoms
$\neg\neg\neg a$. But, according to the definition of the GL-reduct in (?),
such formulas are equivalent to simple negated atoms $\neg a$, and we treat
them as such.. This leads to the following, central definition.

######  Definition 3.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP. A set $\mathcal{M}$
of interpretations over $\mathcal{A}$ is a _candidate world view (CWV)_ of
$\Pi$ if there is an epistemic guess $\Phi\subseteq\mathcal{E}$ such that
$\mathcal{M}=\mathit{AS}(\Pi^{\Phi})$ and $\mathcal{M}$ is compatible with
$\Phi$ w.r.t. $\mathcal{E}$. The set of all CWVs of an ELP $\Pi$ is denoted by
$\mathit{cwv}(\Pi)$.

Let us reconsider the CWA formulations as examples.

######  Example 4.

Let $\mathcal{A}_{C}=\\{p,p^{\prime}\\}$,
$\mathcal{E}_{C}=\\{\mathbf{not}\,p,\mathbf{not}\,\neg p\\}$,
$\Pi_{G}=(\mathcal{A}_{C},\mathcal{E}_{C},\mathcal{R}_{G})$ with
$\mathcal{R}_{G}$ containing only rule $(\ref{eq:gelfond-cwa})$, and
$\Pi_{S}=(\mathcal{A}_{C},\mathcal{E}_{C},\mathcal{R}_{S})$ with
$\mathcal{R}_{S}$ containing only rule $(\ref{eq:shen-eiter-cwa})$.

We obtain $\mathit{cwv}(\Pi_{G})=\\{\\{\\{p^{\prime}\\}\\}\\}$ as guess
$\Phi=\\{\mathbf{not}\,p\\}$ is compatible with
$\mathit{AS}(\Pi_{G}^{\Phi}=\\{p^{\prime}\leftarrow\neg
p\\})=\\{\\{p^{\prime}\\}\\}$, while no other guesses are compatible with the
answer sets of the respective epistemic reducts. We also obtain
$\mathit{cwv}(\Pi_{S})=\\{\\{\\{p^{\prime}\\}\\}\\}$ as $\Phi$ is compatible
with
$\mathit{AS}(\Pi_{S}^{\Phi}=\\{p^{\prime}\leftarrow\top\\})=\\{\\{p^{\prime}\\}\\}$,
while no other guesses are compatible with the answer sets of the respective
epistemic reducts.

Following the principle of knowledge minimization, ? (?) define a _world view_
as follows.

######  Definition 5.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP.
$\mathcal{C}\in\mathit{cwv}(\Pi)$ is called _world view (WV)_ of $\Pi$ if its
associated guess $\Phi$ is subset-maximal, i.e. there is no
$\mathcal{C}^{\prime}\in\mathit{cwv}(\Pi)$ with associated guess
$\Phi^{\prime}\supset\Phi$.

Note that in Example 4 there is only one CWV per program; hence the associated
guesses are subset-maximal, and the sets of CWVs and WVs coincide.

One of the main reasoning tasks regarding ELPs is the _world view existence
problem_ , that is, given an ELP $\Pi$, decide whether a WV (or, equivalently,
CWV) exists. This problem is $\Sigma_{\mathit{3}}^{\mathit{P}}$-complete (?).

We close this section with a statement that shows that extending $\mathcal{A}$
or $\mathcal{E}$ of an ELP does not change their CWVs (and hence also not
their WVs).

######  Theorem 6.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP and let
$\Pi^{\prime}=(\mathcal{A}^{\prime},\mathcal{E}^{\prime},\mathcal{R})$ be an
ELP with the same set of rules, but with
$\mathcal{A}^{\prime}\supset\mathcal{A}$ and
$\mathcal{E}^{\prime}\supset\mathcal{E}$. Then,
$\mathit{cwv}(\Pi)=\mathit{cwv}(\Pi^{\prime})$.

The proof can be found in Appendix A. The above theorem implies that, given
two ELPs $\Pi_{1}=(\mathcal{A}_{1},\mathcal{E}_{1},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A}_{2},\mathcal{E}_{2},\mathcal{R}_{2})$, we can always
assume that $\mathcal{A}_{1}=\mathcal{A}_{2}$ and
$\mathcal{E}_{1}=\mathcal{E}_{2}$ (since the domains can be extended without
changing the CWVs, as per the above theorem).

##  3 Strong Equivalence for ELPs

In this section, we will investigate notions of equivalence of ELPs, in
particular, focusing on how to extend the concept of strong equivalence (?; ?)
from logic programs to ELPs. We will start by defining (ordinary) equivalence
of two ELPs.

######  Definition 7.

Two ELPs are _WV-equivalent_ (resp.  _CWV-equivalent_) iff their WVs (resp.
CWVs) coincide.

We observe that CWV-equivalence is the stronger notion, as it immediately
implies WV-equivalence. Moreover, for two ELPs to be equivalent as defined
above, not only must the set of guesses leading to WVs/CWVs be the same, but
also the answer sets in each of these WVs/CWVs.

We now continue by defining strong equivalence for ELPs. One motivation for
such a kind of equivalence is modularization: we want to be able to replace a
sub-program by another one such that the semantics (i.e. WVs or CWVs) of the
overall program does not change. Based on the two equivalence notions defined
above and using ideas from work done in the area of logic programs (?), we
propose four notions of strong equivalence for ELPs.

######  Definition 8.

Let $\Pi_{1}$ and $\Pi_{2}$ be two ELPs. $\Pi_{1}$ and $\Pi_{2}$ are

  * •

_strongly ELP-WV-equivalent_ iff, for every ELP $\Pi$, $\Pi_{1}\cup\Pi$ and
$\Pi_{2}\cup\Pi$ are WV-equivalent;

  * •

_strongly ASP-WV-equivalent_ iff, for every (plain) logic program $\Pi$,
$\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ are WV-equivalent;

  * •

_strongly ELP-CWV-equivalent_ iff, for every ELP $\Pi$, $\Pi_{1}\cup\Pi$ and
$\Pi_{2}\cup\Pi$ are CWV-equivalent;

  * •

_strongly ASP-CWV-equivalent_ iff, for every (plain) logic program $\Pi$,
$\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ are CWV-equivalent.

Having defined these equivalence notions for ELPs, the main aim of this
section is to characterize strong equivalence in a similar fashion as was done
for logic programs by ? (?). Note that one could be tempted to define strong
equivalence for ELPs simply in terms of ?’s SE-models of the epistemic
reducts, for each possible epistemic guess. However, this approach does not
capture our intentions, as the following example shows:

######  Example 9.

Take the two ELPs $\Pi_{1}=(\mathcal{A},\mathcal{E},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A},\mathcal{E},\mathcal{R}_{2})$ with
$\mathcal{R}_{1}=\\{p\leftarrow\mathbf{not}\,p\\}$,
$\mathcal{R}_{2}=\\{p\leftarrow\neg p\\}$ and
$\mathcal{E}=\\{\mathbf{not}\,p\\}$. Now, for the guess $\Phi_{1}=\emptyset$,
note that $\Pi_{1}^{\Phi_{1}}=\Pi_{2}^{\Phi_{1}}$ and hence, trivially, the
SE-models are also the same. However, for the guess $\Phi_{2}=\mathcal{E}$,
$\Pi_{1}^{\Phi_{2}}$ consists of the rule $p\leftarrow\top$, while
$\Pi_{2}^{\Phi_{2}}$ reduces to $p\leftarrow\neg p$. It can be checked that
the SE-models of these two epistemic reducts w.r.t. $\Phi_{2}$ are not the
same, hence these two programs are not strongly equivalent in the sense of
(?). However, it turns out that the guess $\Phi_{2}$ can never give rise to a
CWV, since it requires that there is an answer set not containing $p$, but
both $\Pi_{1}^{\Phi_{2}}$ and $\Pi_{2}^{\Phi_{2}}$ require that $p$ is true in
all answer sets of the CWV. Hence, it seems that the epistemic reducts for
$\Phi_{2}$ should not have any bearing on evaluating strong equivalence.

The example above implies that, when establishing strong equivalence for ELPs,
we should discard guesses that can never give rise to a CWV. We formalize this
as follows:

######  Definition 10.

Let $\mathcal{I}$ be a set of interpretations over a domain of atoms
$\mathcal{A}$, let $\mathcal{E}$ be a set of epistemic literals over
$\mathcal{A}$, and $\Phi\subseteq\mathcal{E}$ be a guess. Then, $\Phi$ is
_realizable_ in $\mathcal{I}$ iff there is a subset
$\mathcal{I}^{\prime}\subseteq\mathcal{I}$ such that $\mathcal{I}^{\prime}$ is
compatible with $\Phi$ w.r.t. $\mathcal{E}$.

Given an ELP $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ and a guess
$\Phi\subseteq\mathcal{E}$, we say that $\Phi$ is _realizable in $\Pi$_ iff
$\Phi$ is realizable in the set of models of $\Pi^{\Phi}$. We say that $\Phi$
is _realizable in a set of SE-models $\mathcal{S}$_ iff $\Phi$ is realizable
in the set $\\{Y\mid(X,Y)\in\mathcal{S}\\}$. We are now ready to define our
central construct, the SE-function $\mathcal{S}\mathcal{E}_{\Pi}$ of an ELP,
which will be the key concept to characterize strong equivalence for ELPs.
Note that realizability plays an important role in this.

######  Definition 11.

The _SE-function_ $\mathcal{S}\mathcal{E}_{\Pi}(\cdot)$ of an ELP
$\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ maps guesses
$\Phi\subseteq\mathcal{E}$ for $\Pi$ to sets of SE-models as follows.

$\mathcal{S}\mathcal{E}_{\Pi}(\Phi)=\left\\{\begin{array}[]{@{}lr@{}}\mathcal{S}\mathcal{E}(\Pi^{\Phi})&\text{if
}\Phi\text{ realizable in }\Pi\\\
\emptyset&\text{otherwise.}\end{array}\right.$

######  Example 12.

Recall that programs $\Pi_{G}$ and $\Pi_{S}$ of Example 4 are both CWV- and
WV-equivalent. However, we find that their respective SE-functions differ:
$\mathcal{S}\mathcal{E}_{\Pi_{G}}(\\{\mathbf{not}\,p\\})$ contains the tuple
$(\emptyset,\\{p\\})$, but
$\mathcal{S}\mathcal{E}_{\Pi_{S}}(\\{\mathbf{not}\,p\\})$ does not; yet
$\\{\mathbf{not}\,p\\}$ is realizable in both $\Pi_{G}$ and $\Pi_{S}$.

Note that if $\Phi$ is realizable in $\Pi$, then
$\\{Y\mid(X,Y)\in\mathcal{S}\mathcal{E}_{\Pi}(\Phi)\\}=\mathit{mods}(\Pi^{\Phi})$.
Before proceeding to our main results, we first state some observations that
can be made about the SE-function of an ELP.

######  Lemma 13.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP with
$\mathcal{S}\mathcal{E}_{\Pi}$ its SE-function. Further, let $\mathcal{M}$ be
a set of interpretations, and $\Phi\subseteq\mathcal{E}$ be a guess. Then,
$\mathcal{M}$ is a CWV of $\Pi$ w.r.t. $\Phi$ iff
$\mathcal{M}=\\{Y\mid(Y,Y)\in\mathcal{S}\mathcal{E}_{\Pi}(\Phi),\neg\exists
X\subset Y\ (X,Y)\in\mathcal{S}\mathcal{E}_{\Pi}(\Phi)\\}$ and $\mathcal{M}$
is compatible with $\Phi$.

###### Proof.

The left-to-right direction can be shown as follows. By definition of the SE-
function it holds that for each CWV $\mathcal{M}$ w.r.t. a guess $\Phi$ for
$\Pi$, $\mathcal{S}\mathcal{E}_{\Pi}(\Phi)$ contains the set $\\{(Y,Y)\mid
Y\in\mathcal{M}\\}$, and, since $\mathcal{M}$ contains only answer sets of the
epistemic reduct $\Pi^{\Phi}$, there cannot be a pair $(X,Y)$ in
$\mathcal{S}\mathcal{E}_{\Pi}(\Phi)$ with $X\subset Y$. There also cannot be
some other pair $(Y^{\prime},Y^{\prime})\in\mathcal{S}\mathcal{E}_{\Pi}(\Phi)$
for which no pair $(X^{\prime},Y^{\prime})$ with $X^{\prime}\subset
Y^{\prime}$ exists, since then this would mean that $Y^{\prime}$ is an answer
set of $\Pi^{\Phi}$, and therefore must be in $\mathcal{M}$. Finally, since by
assumption $\mathcal{M}$ is a CWV, it is compatible with $\Phi$ by definition.

For the right-to-left direction, note that $\mathcal{M}$ clearly contains all
those sets of atoms $Y$ that are models of $\Pi^{\Phi}$, such that there is no
subset of $Y$ model of the GL-reduct $[\Pi^{\Phi}]^{Y}$. Hence, $\mathcal{M}$
contains precisely the answer sets of $\Pi^{\Phi}$. Since, by assumption,
$\mathcal{M}$ is compatible with $\Phi$, this immediately implies that
$\mathcal{M}$ is a CWV of $\Pi$ as per Definition 3. ∎

The next statement is a direct consequence of the previous lemma, since, as we
have seen, the SE-function of an ELP defines its CWVs.

######  Lemma 14.

Programs with the same SE-function are CWV-equivalent (and hence WV-
equivalent).

We are now ready to state the main result of this section, namely that the SE-
function precisely characterizes strong equivalence for ELPs.

######  Theorem 15.

Let $\Pi_{1}$ and $\Pi_{2}$ be two ELPs. The following statements are
equivalent:

  1. 1.

$\Pi_{1}$ and $\Pi_{2}$ are ELP-CWV-equivalent;

  2. 2.

$\Pi_{1}$ and $\Pi_{2}$ are ASP-CWV-equivalent;

  3. 3.

$\Pi_{1}$ and $\Pi_{2}$ are ELP-WV-equivalent;

  4. 4.

$\Pi_{1}$ and $\Pi_{2}$ are ASP-WV-equivalent; and

  5. 5.

$\mathcal{S}\mathcal{E}_{\Pi_{1}}=\mathcal{S}\mathcal{E}_{\Pi_{2}}$.

###### Proof.

$(\ref{thm:strongequivalence:1})\Rightarrow(\ref{thm:strongequivalence:2})\Rightarrow(\ref{thm:strongequivalence:4}),(\ref{thm:strongequivalence:1})\Rightarrow(\ref{thm:strongequivalence:3})\Rightarrow(\ref{thm:strongequivalence:4})$.
These follow directly from Definition 8 and from the fact that every WV is a
CWV and every ASP program is an ELP.

$(\ref{thm:strongequivalence:5})\Rightarrow(\ref{thm:strongequivalence:1})$.
Assume that statement $(5)$ holds. We need to show that for any third program
$\Pi$ it holds that $\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ are equivalent. To
this end, pick any guess $\Phi$. Then,

$\mathcal{S}\mathcal{E}_{\Pi_{1}\cup\Pi}(\Phi)=$
$\left\\{\begin{array}[]{@{}lr@{}}\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)\cap\mathcal{S}\mathcal{E}_{\Pi}(\Phi)&\text{if
}\Phi\text{ is realizable in }\\\
&\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)\cap\mathcal{S}\mathcal{E}_{\Pi}(\Phi)\\\\[8.61108pt]
\emptyset&\text{otherwise}\end{array}\right\\}$
$=\mathcal{S}\mathcal{E}_{\Pi_{2}\cup\Pi}(\Phi),$

since
$\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)=\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)$
by assumption, and thus
$\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)\cap\mathcal{S}\mathcal{E}_{\Pi}(\Phi)=\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)\cap\mathcal{S}\mathcal{E}_{\Pi}(\Phi)$.
Lemma 14 then proves that $\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ are
equivalent.

$(\ref{thm:strongequivalence:4})\Rightarrow(\ref{thm:strongequivalence:5})$.
We will prove the contrapositive. Let
$\Pi_{1}=(\mathcal{A}_{1},\mathcal{E}_{1},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A}_{2},\mathcal{E}_{2},\mathcal{R}_{2})$ be two ELPs and
assume, w.l.o.g., that $\mathcal{A}_{1}=\mathcal{A}_{2}=\mathcal{A}$ and
$\mathcal{E}_{1}=\mathcal{E}_{2}=\mathcal{E}$ (cf. Theorem 6). Further, let
$\Phi\subseteq\mathcal{E}$ be a guess such that
$\mathcal{Y}_{1}=\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)\neq\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)=\mathcal{Y}_{2}$.
Finally, assume that there is a pair $(X,Y)$ in $\mathcal{Y}_{1}$ but not in
$\mathcal{Y}_{2}$ (again, w.l.o.g., by symmetry). We need to show that there
exists a logic program $\Pi$ (i.e. without epistemic literals) such that the
WVs of the ELP $\Pi_{1}\cup\Pi$ differ from those of $\Pi_{2}\cup\Pi$. We only
need to consider the case where $\Pi_{1}$ and $\Pi_{2}$ are WV-equivalent,
since the claim is trivially true otherwise.

By Definition 11, with $\mathcal{Y}_{1}$ non-empty by assumption, there is a
subset $\mathcal{C}\subseteq\\{Y\mid(X,Y)\in\mathcal{Y}_{1}\\}$ compatible
with $\Phi$, since $\Phi$ is realizable in $\Pi$. Let
$\mathcal{C}=\\{Y_{1},\ldots,Y_{m}\\}$ and let
$\\{Y_{m+1},\ldots,Y_{n}\\}=2^{\mathcal{A}}\setminus\mathcal{C}$.

The idea is to construct $\Pi$ in such a way that the potential WV represented
by $\mathcal{C}$ is actually realized in $\Pi_{1}\cup\Pi$. To construct $\Pi$,
let $y_{1},\ldots,y_{n}$ be fresh atoms not occurring in $\mathcal{A}$. Let
$\Pi$ contain the rule $y_{1}\vee\ldots\vee y_{n}\leftarrow\top,$ and,
furthermore, for all $1\leq i\leq n$ and $a\in Y_{i}$, the rule
$\bot\leftarrow y_{i},\neg a$, and for all $a\in\mathcal{A}\setminus Y_{i}$,
the rule $\bot\leftarrow y_{i},a$. This makes sure that for every model
$Y_{i}$ of $\Pi_{1}^{\Phi}$, the corresponding model $Y_{i}^{\prime}$ of
$(\Pi_{1}\cup\Pi)^{\Phi}$ contains the atom $y_{i}$ (i.e.
$Y_{i}^{\prime}=Y_{i}\cup\\{y_{i}\\}$).

Now, take the pair $(X,Y)$ that is, by assumption, contained in
$\mathcal{Y}_{1}$ (but not in $\mathcal{Y}_{2}$). Clearly, there is some
integer $k$, $1\leq k\leq n$, such that $Y=Y_{k}$. Now, for each model
$Y_{i}$, $1\leq i\leq m$, $i\neq k$, and each atom $a\in Y_{i}$, add the rule
$a\leftarrow y_{i}$ to $\Pi$. For each model $Y_{i}$, $m<i\leq n$, $i\neq k$,
add the rule $\bot\leftarrow y_{i}$ to $\Pi$. This makes sure that, in
$(\Pi_{1}\cup\Pi)^{\Phi}$, exactly the models from $\mathcal{C}$ (except
$Y_{k}$, if $k\leq m$) become answer sets, and all other models are destroyed,
except for the model $Y=Y_{k}$, if $k>m$.

At this point, if we have that
$\\{Y_{1},\ldots,Y_{m}\\}\not\subseteq\mathit{mods}(\Pi_{2}^{\Phi})$, we
simply do the same as above also for the model $Y=Y_{k}$ (i.e. realize $Y_{k}$
as an answer set if $k\leq m$, or destroy $Y_{k}$ in case $k>m$). Then,
clearly, $(\Pi_{1}\cup\Pi)^{\Phi}$ will have the answer sets
$\\{Y_{1}\cup\\{y_{1}\\},\ldots,Y_{m}\cup\\{y_{m}\\}\\}$ which form a CWV of
$\Pi_{1}\cup\Pi$, but not of $\Pi_{2}\cup\Pi$. Since all other models are
destroyed, independent of the guess $\Phi$, this CWV is actually the only CWV
of $\Pi_{1}\cup\Pi$, and hence, it is a WV, proving our claim that
$\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ are not WV-equivalent ($\star$). It
therefore remains to show the claim for the case where the set
$\\{Y_{1},\ldots,Y_{m}\\}\subseteq\mathit{mods}(\Pi_{2}^{\Phi})$. To this end,
we need to distinguish the following two cases:

Case (1). Assume that $Y\not\vDash\Pi_{2}^{\Phi}$. In this case, for each atom
$a\in Y$, add the rule $a\leftarrow y_{k}$ to $\Pi$. Now, $Y\cup\\{y_{k}\\}$
is an answer set of $(\Pi_{1}\cup\Pi)^{\Phi}$, but not of
$(\Pi_{2}\cup\Pi)^{\Phi}=\Pi_{2}^{\Phi}\cup\Pi$.

Case (2). Assume that $Y\vDash\Pi_{2}^{\Phi}$. In this case, for each atom
$a\in X$, add the rule $a\leftarrow y_{k}$ to $\Pi$, and, in addition, for all
atoms $a,b\in Y\setminus X$, add the rule $a\leftarrow b,y_{k}$ to $\Pi$. We
will show that, in this case, $Y$ is an answer set of
$(\Pi_{2}\cup\Pi)^{\Phi}$, but not of $(\Pi_{1}\cup\Pi)^{\Phi}$. Since
$Y\vDash\Pi_{2}^{\Phi}$ and every model of a program is also a model of its
GL-reduct, by definition of SE-models we know that $Y\neq X$, since, by
assumption, $(X,Y)\in\mathcal{Y}_{1}$ but $(X,Y)\not\in\mathcal{Y}_{2}$. Since
$(X,Y)\in\mathcal{Y}_{1}$, we have that $X\vDash[\Pi_{1}^{\Phi}]^{Y}$. But
then, by construction of $\Pi$ it holds that
$X\cup\\{y_{k}\\}\vDash[(\Pi_{1}\cup\Pi)^{\Phi}]^{Y}=[\Pi_{1}^{\Phi}]^{Y}\cup[\Pi^{\Phi}]^{Y}$
and therefore $Y\cup\\{y_{k}\\}$ is not an answer set of
$(\Pi_{1}\cup\Pi)^{\Phi}$. On the other hand, for $(\Pi_{2}\cup\Pi)^{\Phi}$,
assume that there is some $X^{\prime}\subset Y$ such that
$X^{\prime}\cup\\{y_{k}\\}\vDash[(\Pi_{2}\cup\Pi)^{\Phi}]^{Y}$. Clearly, by
construction of $\Pi$, $X\subset X^{\prime}$. Thus, there is some atom $a$ in
$X^{\prime}\subseteq Y$ but not in $X$. But, by construction of $\Pi$, we then
have that $X^{\prime}=Y$. Hence, $Y\cup\\{y_{k}\\}$ is an answer set of
$(\Pi_{2}\cup\Pi)^{\Phi}$, as desired.

The above shows that, for both cases (1) and (2), the set
$\mathcal{C}^{\prime}=\\{Y_{1}\cup\\{y_{1}\\},\ldots,Y_{m}\cup\\{y_{m}\\}\\}$
is the set of answer sets of one of the two programs $(\Pi_{1}\cup\Pi)^{\Phi}$
and $(\Pi_{2}\cup\Pi)^{\Phi}$, and therefore, by assumption, a CWV of that
program. But, by construction of $\Pi$, $\mathcal{C}^{\prime}$ cannot be a CWV
for the other program (because $Y\cup\\{y_{k}\\}$ is an answer set of one of
the two programs, but not both, and hence distinguishes the CWVs)333Note that,
in particular, in case (1), $\mathcal{C}^{\prime}$ is a CWV of
$\Pi_{1}\cup\Pi$ but not of $\Pi_{2}\cup\Pi$, and in case (2), the same holds
if $k\leq m$, and the reverse holds if $k>m$.. It remains to show that
$\mathcal{C}^{\prime}$ is not only a CWV but also a WV of exactly one of the
two programs, which can be done via the argument for ($\star$). This concludes
the proof. ∎

The above theorem states that the SE-function precisely characterizes all the
notions of strong equivalence for ELPs and that these notions are all
equivalent. We therefore will, from now on, jointly refer to these four
equivalent notions as _strong equivalence_. The next statement follows
immediately.

######  Corollary 16.

ELPs are strongly equivalent iff they have the same SE-function.

######  Example 17.

Continuing from Example 12, we observe that the difference in the SE-function
can be made manifest by combining the two programs with the program
$\Pi=(\mathcal{A}_{C},\mathcal{E}_{C},\mathcal{R})$, where
$\mathcal{R}=\\{p\leftarrow\neg p^{\prime}\\}$. We observe that
$\mathit{cwv}(\Pi_{G}\cup\Pi)=\\{\\{\\{p\\}\\}\\}$ (due to guess
$\\{\mathbf{not}\,p\\}$) and
$\mathit{cwv}(\Pi_{S}\cup\Pi)=\\{\\{\\{p^{\prime}\\}\\}\\}$ (due to guess
$\\{\mathbf{not}\,\neg p\\}$).

We close this section by showing that our definition of strong equivalence for
ELPs generalizes the established notion of strong equivalence for logic
programs.

######  Corollary 18.

Let $\Pi_{1}=(\mathcal{A},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A},\mathcal{R}_{2})$ be two logic programs, and let
$\Pi_{1}^{\prime}=(\mathcal{A},\emptyset,\mathcal{R}_{1})$ and
$\Pi^{\prime}_{2}=(\mathcal{A},\emptyset,\mathcal{R}_{2})$ be two ELPs with
the same sets of rules as $\Pi_{1}$ and $\Pi_{2}$, respectively. Then,
$\Pi_{1}$ and $\Pi_{2}$ are strongly equivalent iff $\Pi_{1}^{\prime}$ and
$\Pi_{2}^{\prime}$ are.

###### Proof.

(Sketch) For $\Pi^{\prime}_{1}$ and $\Pi^{\prime}_{2}$ there is only one
possible guess, namely, $\Phi=\emptyset$. Moreover, in this setting it holds
that $\mathcal{S}\mathcal{E}_{\Pi}(\emptyset)=\mathcal{S}\mathcal{E}(\Pi)$ for
any ELP $\Pi$: the crucical observation is that $\mathcal{S}\mathcal{E}(\Pi)$
is compatible with $\Phi$ w.r.t. the empty domain of epistemic literals,
exactly if $\mathcal{S}\mathcal{E}(\Pi)\neq\emptyset$. ∎

##  4 Complexity of ELP Strong Equivalence

We now make use of our characterization to settle the computational complexity
of deciding strong equivalence between ELPs. The following lemma shows that to
check the realizability of a guess $\Phi$ for a given ELP $\Pi$ it suffices to
consider a polynomially-sized subset of the models of $\Pi$.

######  Lemma 19.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP,
$\Phi\subseteq\mathcal{E}$ a guess for $\Pi$, and
$\mathcal{Y}=\mathcal{S}\mathcal{E}_{\Pi}(\Phi)$ be non-empty. Then, there is
a set $\mathcal{C}\subseteq\\{Y\mid(X,Y)\in\mathcal{Y}\\}$ of polynomial size
in $\Pi$ that is compatible with $\Phi$ w.r.t. $\mathcal{E}$.

###### Proof.

According to Definition 11, since $\Phi$ is realizable in $\Pi$, there is a
subset $\mathcal{Y}^{\prime}\subseteq\mathcal{Y}$, such that the set
$\mathcal{C}^{\prime}=\\{Y\mid(X,Y)\in\mathcal{Y}^{\prime}\\}$ is compatible
with $\Phi$. By Definition 2, for each $\mathbf{not}\,\ell\in\mathcal{E}$,
when $\Phi$ contains $\mathbf{not}\,\ell$, there is a
$Y_{\mathbf{not}\,\ell}\in\mathcal{C}^{\prime}$ such that $\ell$ is false in
$Y_{\mathbf{not}\,\ell}$. Take the subset
$\mathcal{C}\subseteq\mathcal{C}^{\prime}$ containing $Y_{\mathbf{not}\,\ell}$
for each $\mathbf{not}\,\ell\in\mathcal{E}$, or, if $\Phi=\emptyset$, let
$\mathcal{C}$ be any singleton subset of $\mathcal{C}^{\prime}$. Note that
$\mathcal{C}$ is of polynomial size in $\Pi$. Clearly, $\mathcal{C}$ is also
compatible with $\Phi$. ∎

With this crucial observation in place, we are now ready to state the
complexity of checking strong equivalence for ELPs, which remains in coNP as
for plain logic programs. This is surprising, since reasoning tasks for ELPs
generally are one level higher on the polynomial hierarchy than the
corresponding tasks for logic programs (cf. Section 2).

######  Theorem 20.

Checking whether two ELPs are strongly equivalent is coNP-complete.

###### Proof.

We give a non-deterministic polynomial time procedure for checking that two
ELPs are _not_ strongly equivalent, that is, that there is a difference in
their respective SE-functions. W.l.o.g. let
$\Pi_{1}=(\mathcal{A},\mathcal{E},\mathcal{R}_{1})$ and
$\Pi_{2}=(\mathcal{A},\mathcal{E},\mathcal{R}_{2})$. The procedure works as
follows:

  1. 1.

Guess an epistemic guess $\Phi\subseteq\mathcal{E}$.

  2. 2.

Guess a polynomially-sized, non-empty set of interpretations $\mathcal{C}$
over $\mathcal{A}$, compatible with $\Phi$.

  3. 3.

Verify in polynomial time that each $Y\in\mathcal{C}$ is a model of both
$\Pi_{1}^{\Phi}$ and $\Pi_{2}^{\Phi}$. If not, REJECT.

  4. 4.

Guess a pair $(X,Y)$ with $X\subseteq Y\subseteq\mathcal{A}$.

  5. 5.

Verify in polynomial time that
$(X,Y)\in\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)$ but
$(X,Y)\not\in\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)$ or vice versa. If so,
ACCEPT. If not, REJECT.

Clearly, the above procedure terminates in polynomial time, since it is known
that model checking for SE-models can be done in polynomial time (?). To
obtain correctness, it is not difficult to verify that the above procedure is
sound and complete given the following two observations. Firstly, note that
Lemma 19 implies that we only need to focus on polynomially sized subsets when
evaluating the realizability of a guess as stated in Definition 11; hence
guessing a polynomially sized set of interpretations is enough in step 2.
Secondly, assume that two programs $\Pi_{1}$ and $\Pi_{2}$ have differing SE-
functions. Then this means that there must be some guess $\Phi$, such that
both sets $\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)$ and
$\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)$ are non-empty (clearly, as otherwise
$\mathcal{S}\mathcal{E}_{\Pi_{1}}(\Phi)=\mathcal{S}\mathcal{E}_{\Pi_{2}}(\Phi)=\emptyset$
for all guesses $\Phi$). But, by Definition 11, this means that both sets
contain a potential CWV. Now there are two cases: either they do not share any
potential CWVs, or if they do, then there is at least one SE-model $(X,Y)$
contained in one but not both of the two sets.

Corollary 18 allows us to inherit the coNP lower bound from the case of logic
programs (?), which completes the proof. ∎

##  5 Case Studies

In this section, we apply our characterisation to investigate basic principles
for simplifying ELPs.

### Tautological Rules

Tautological rules are rules that can simply be removed from any program
without affecting its outcome.

######  Definition 21.

An ELP rule $r$ is _tautological_ iff the single-rule ELP
$\Pi_{r}=(\mathcal{A},\mathcal{E},\\{r\\})$ is strongly equivalent to the
empty program $\Pi_{\emptyset}=(\mathcal{A},\mathcal{E},\emptyset)$.

Let $\mathcal{E}$ be a set of epistemic literals over $\mathcal{A}$. We say
that an epistemic guess $\Phi\subseteq\mathcal{E}$ is _consistent_ iff,
whenever $\mathcal{E}$ contains both $\mathbf{not}\,a$ and $\mathbf{not}\,\neg
a$ for some atom $a\in\mathcal{A}$, it holds that $\Phi$ contains at least one
of $\\{\mathbf{not}\,a,\mathbf{not}\,\neg a\\}$.444Clearly, if $\Phi$ contains
neither of the two epistemic literals, then $\Phi$ can never be realizable in
any ELP, since there is no (non-empty) set of models where $a$ is both always
true and always false. Moreover, let $\mathcal{S}_{\mathcal{A}}$ denote the
set of all pairs $(X,Y)$ such that $X\subseteq Y\subseteq\mathcal{A}$.

######  Lemma 22.

An ELP rule $r$ is tautological iff for the single-rule ELP
$\Pi_{r}=(\mathcal{A},\mathcal{E},\\{r\\})$ it holds that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\mathcal{S}_{\mathcal{A}}$ for each
consistent guess $\Phi\subseteq\mathcal{E}$.

###### Proof.

This follows from the fact that for the empty program
$\Pi_{\emptyset}=(\mathcal{A},\mathcal{E},\emptyset)$,
$\mathcal{S}\mathcal{E}_{\Pi_{\emptyset}}(\Phi)=\mathcal{S}_{\mathcal{A}}$ for
each consistent guess $\Phi\subseteq\mathcal{E}$, and the observation that if
$\mathcal{S}\mathcal{E}(\Pi^{\Phi})=\mathcal{S}_{\mathcal{A}}$, then $\Phi$ is
realizable in $\Pi$. ∎

Before syntactically characterizing tautological ELP rules, we recall a
corresponding result for standard ASP rules from the literature. For
convenience, we shall denote ASP rules of the form (3) as

$A\leftarrow B,\neg C,\neg\neg D,$ (4)

using sets of atoms $A$, $B$, $C$, and $D$ as is common practice. In what
follows, we denote single-rule logic programs consisting of a rule $r$ by
$\Pi_{r}=(\mathcal{A},\mathcal{R})$ with $\mathcal{R}=\\{r\\}$ and call $r$
tautological if $\Pi_{r}$ is strongly equivalent to the empty program
$\Pi=(\mathcal{A},\emptyset)$, i.e.
$\mathcal{S}\mathcal{E}(\Pi_{r})=S_{\mathcal{A}}$. The following result is due
to (?, Lemma 2).

######  Lemma 23.

A rule $r$ of the form (4) is tautological iff ($\alpha$) $A\cap
B\neq\emptyset$, ($\beta$) $B\cap C\neq\emptyset$, or ($\gamma$) $C\cap
D\neq\emptyset$.

We are now ready to characterize tautological ELP rules. For the sake of
presentation let us write them as

$A\leftarrow B,\neg C,\mathbf{not}\,D,\mathbf{not}\,\neg
E,\neg\mathbf{not}\,F,\neg\mathbf{not}\,\neg G,$ (5)

where, again, each capital letter represents a set of atoms, analogously to
ASP rules of the form (4). Note that $D$ here plays a different role than in
(4); this is due to the fact that in ELP rules we have no explicit double
negation.

Let us also consider the notion of epistemic reduct w.r.t. the above notation.
Analogously to the ASP case, let
$\Pi_{r}=(\mathcal{A},\mathcal{E},\mathcal{R})$ be the single-rule ELP with
$\mathcal{R}=\\{r\\}$. Now, for $\Phi\subseteq\mathcal{E}$, we have
$\Pi_{r}^{\Phi}=(\mathcal{A},\mathcal{E},\mathcal{R}^{\Phi})$ with
$\mathcal{R}^{\Phi}=\emptyset$ if $\mathbf{not}\,f\in\Phi$ for some $f\in F$
or if $\mathbf{not}\,\neg g\in\Phi$ for $g\in G$; otherwise,

$\mathcal{R}^{\Phi}=\\{r^{\Phi}\\}=\\{A\leftarrow B,\neg C,\neg
D^{\Phi},\neg\neg E^{\Phi},\neg\neg F,\neg G\\}$

with $D^{\Phi}=\\{d\in D,\mathbf{not}\,d\notin\Phi\\}$, $E^{\Phi}=\\{e\in
E,\mathbf{not}\,\neg e\notin\Phi\\}$. We are now ready to give our full
syntactical characterization of tautological ELP rules. It shows that deciding
whether a rule is tautological amounts to a simple syntactic check and can be
done individually, for each rule.

######  Theorem 24.

An ELP rule $r$ of form (5) is tautological iff (a) $A\cap B\neq\emptyset$,
(b) $B\cap(C\cup G)\neq\emptyset$, (c) $C\cap F\neq\emptyset$, (d) $D\cap
F\neq\emptyset$, (e) $E\cap G\neq\emptyset$, or (f) $F\cap G\neq\emptyset$.

###### Proof.

Let $\Pi_{r}=(\mathcal{A},\mathcal{E},\mathcal{R})$ be the single-rule ELP
with $\mathcal{R}=\\{r\\}$, and, for an epistemic guess $\Phi$, let $r^{\Phi}$
denote the unqiue rule in $\mathcal{R}^{\Phi}$ in case
$\mathcal{R}^{\Phi}\neq\emptyset$.

($\Rightarrow$) Let $r$ be an ELP rule satisfying at least one of the
conditions (a)–(f), and let $\Phi\subseteq\mathcal{E}$ be a consistent guess.
By Lemma 22, we have to show that either $\mathcal{R}^{\Phi}=\emptyset$ or
that $r^{\Phi}$ fulfills the conditions of Lemma 23. This can be easily
verified for conditions (a)–(c). For (d), note that if
$\mathbf{not}\,f\in\Phi$ for some $f\in F$ we get
$\mathcal{R}^{\Phi}=\emptyset$; otherwise for all $f\in F$ it holds that
$\mathbf{not}\,f\notin\Phi$, and thus that $D\cap F\neq\emptyset$, and it
follows that $f\in D^{\Phi}$ for some $f\in F$. Hence we have $\neg f$ and
$\neg\neg f$ in $r^{\Phi}$, which is tautological as per Lemma 23, condition
($\gamma$). The argument is similar for (e), Finally, for (f) note that since
$\Phi$ is consistent, it must contain one of $\mathbf{not}\,a$ and
$\mathbf{not}\,\neg a$ for each $a\in F\cap G$. It follows that
$\mathcal{R}^{\Phi}=\emptyset$.

($\Leftarrow$) Let $r$ be an ELP rule such that none of (a)–(f) hold. Let
$\Phi=\mathcal{E}\setminus(\mathbf{not}\,F\cup\mathbf{not}\,\neg G)$. $\Phi$
is consistent since (f) does not hold. Moreover,
$\mathbf{not}\,D\cup\mathbf{not}\,\neg E\subseteq\Phi$ (since neither (d) nor
(e) holds). Suppose, $\Phi$ is realizable in $\Pi_{r}$. By construction of
$\Phi$, $\mathcal{R}^{\Phi}=\\{A\leftarrow B,\neg C,\neg\neg F,\neg G\\}$; by
Lemma 23 and the fact that ($\alpha$)–($\gamma$) of that lemma do not hold for
$r^{\Phi}$, we have that $r^{\Phi}$ is not tautological, i.e.
$\mathcal{S}\mathcal{E}(\Pi_{r^{\Phi}})\neq S_{\mathcal{A}}$, and thus
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\neq\mathcal{S}_{\mathcal{A}}$.
Otherwise, we get $\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$. Hence,
for both cases, $r$ is not tautological by Lemma 22. ∎

### Rule Subsumption

Rule subsumption identifies when a rule $s$ can safely be removed from a
program $\Pi$, given another rule $r$ is in $\Pi$.

######  Definition 25.

An ELP rule $s$ is _subsumed_ by an ELP rule $r$ iff $\Pi_{r}$ is strongly
equivalent to $\Pi_{r}\cup\Pi_{s}$.

The next result follows from the definition of the SE-function for a union of
two ELPs (cf. proof of Theorem 15).

######  Lemma 26.

An ELP rule $s$ is subsumed by an ELP rule $r$ iff, for ELPs
$\Pi_{r}=(\mathcal{A},\mathcal{E},\\{r\\})$ and
$\Pi_{s}=(\mathcal{A},\mathcal{E},\\{s\\})$, it holds that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$,
for all guesses $\Phi\subseteq\mathcal{E}$.

Clearly, a tautological rule $s$ is subsumed by any other rule, hence in what
follows we focus on subsumption of non-tautological rules only. Again, we
exploit known results from ASP. With some abuse of terminology, we say that an
ASP rule $r$ subsumes another such rule $s$ iff
$\Pi_{r}=(\mathcal{A},\\{r\\})$ is strongly equivalent to
$\Pi_{r,s}=(\mathcal{A},\\{r,s\\})$, i.e. iff
$\mathcal{S}\mathcal{E}(\Pi_{r})\subseteq\mathcal{S}\mathcal{E}(\Pi_{s})$. We
first adapt a result from (?, Theorem 7) to our notation.

######  Lemma 27.

An ASP rule $r=A\leftarrow B,\neg C,\neg\neg D$ subsumes a non-tautological
ASP rule $s=A^{\prime}\leftarrow B^{\prime},\neg C^{\prime},\neg\neg
D^{\prime}$ iff the following conditions jointly hold: ($\alpha$) $A\subseteq
A^{\prime}\cup C^{\prime}$, ($\beta$) $B\subseteq B^{\prime}\cup D^{\prime}$,
($\beta$’) if $A\cap(A^{\prime}\setminus C^{\prime})\neq\emptyset$ then
$B\subseteq B^{\prime}$, ($\gamma$) $C\subseteq C^{\prime}$, and ($\delta$)
$D\subseteq B^{\prime}\cup D^{\prime}$.

We can now give a syntactic criterion for ELP rule subsumption, which turns
out to be somewhat involved, but still feasible to check. It requires two
technical notions that link a rule $r$ to a rule $s$ whenever $r$ has
sufficiently many elements that are not “absorbed” by default-negated
epistemic literals in $s$.

We are now ready to give our syntactic characterization.

######  Theorem 28.

Let $r$ be an ELP-rule of form (5) and $s=A^{\prime}\leftarrow B^{\prime},\neg
C^{\prime},\mathbf{not}\,D^{\prime},\mathbf{not}\,\neg
E^{\prime},\neg\mathbf{not}\,F^{\prime},\neg\mathbf{not}\,\neg G^{\prime}$ be
non-tautological. Furthermore, let $r\rhd s$ denote that $|(A\cup C\cup
D)\setminus G^{\prime}|>1$ or $(B\cup E)\setminus F^{\prime}\neq\emptyset$,
and $r\RHD s$ denote that $(A\cup C\cup D)\setminus G^{\prime}\neq\emptyset$
or $|(B\cup E)\setminus F^{\prime}|>1$.

Then, $r$ subsumes $s$ iff the following conditions jointly hold:

  1. (a)

$A\subseteq A^{\prime}\cup C^{\prime}\cup D^{\prime}\cup G^{\prime}$;

  2. (a∗)

if $r\rhd s$ then $A\subseteq A^{\prime}\cup C^{\prime}\cup G^{\prime}$;

  3. (b)

$B\subseteq B^{\prime}\cup E^{\prime}\cup F^{\prime}$;

  4. (b∗)

if $r\RHD s$ then $B\subseteq B^{\prime}\cup F^{\prime}$;

  5. (b’)

if $A\cap(A^{\prime}\setminus(C^{\prime}\cup D^{\prime}\cup
G^{\prime}))\neq\emptyset$ then $B\subseteq B^{\prime}$;

  6. (b∗’)

if $r\rhd s$ and $A\cap(A^{\prime}\setminus(C^{\prime}\cup
G^{\prime}))\neq\emptyset$ then $B\subseteq B^{\prime}$;

  7. (c)

$C\cup D\subseteq C^{\prime}\cup D^{\prime}\cup G^{\prime}$;

  8. (c∗)

if $r\rhd s$ then $C\subseteq C^{\prime}\cup G^{\prime}$;

  9. (d)

$E\subseteq B^{\prime}\cup E^{\prime}\cup F^{\prime}$;

  10. (e)

$F\subseteq F^{\prime}$ and $G\subseteq G^{\prime}$.

Note that, in the above, items (a)–(d) generalize the same items in Lemma 27,
and the proof for those parts is a generalization of the proof of that lemma.
The full proof can be found in Appendix B.

Interestingly, applying the above theorem shows, for example, that
$r=p\leftarrow\mathbf{not}\,p$ subsumes $s=p\leftarrow\neg p$ and vice versa
(in particular, since neither $r\rhd s$ nor $s\rhd r$), showing that the two
programs in Example 9 are strongly equivalent.

##  6 Conclusions

In this paper, a simple characterization of strong equivalence for epistemic
logic programs was proposed, which also demonstrates that various notions of
strong equivalence coincide. The characterization generalizes strong
equivalence for plain logic programs, and, somewhat unexpectedly, shows that
checking strong equivalence for ELPs is not harder than for ASP in terms of
computational complexity. The results also give rise to a syntactic
characterization of tautological ELP rules and ELP rule subsumption.

As another byproduct, we studied the relationship between two formalizations
of CWA, Gelfond-CWA and Shen-Eiter-CWA, as our running example. Indeed, while
they are (ordinarily) equivalent, they are not strongly equivalent, as shown
in Examples 12 and 17. In particular, Example 17 shows that, combining $\Pi$
in that example with the Shen-Eiter-CWA rule, yields the world view
$\\{\\{p^{\prime}\\}\\}$, which does not seem intuitive in this setting.
However, in (?), it seems that the CWA rule is proposed for Reiter’s CWA (?),
and thus was not intended to work with rules containing default negation.

For future work, we want to apply our findings to obtain a normal form for
ELPs, as was done for ASP in (?). Furthermore, we plan to study weaker forms
of equivalence (?) for ELPs. In particular, it will be interesting to see
whether our notion of SE-functions can be similarly re-used for characterizing
uniform equivalence like SE-models did serve as a basis for UE-models.

## Acknowledgements

Michael Morak and Stefan Woltran were supported by the Austrian Science Fund
(FWF) under grant number Y698.

##  Appendix A Proof of Theorem 6

We start by re-stating a folklore result from the world of ASP, namely that
the universe of atoms of a logic program can be extended without changing its
answer sets.

######  Proposition 29.

Let $\Pi=(\mathcal{A},\mathcal{R})$ be a logic program and let
$\Pi^{\prime}=(\mathcal{A}^{\prime},\mathcal{R})$ be a logic program with the
same set of rules, but with $\mathcal{A}^{\prime}\supset\mathcal{A}$. Then,
$\mathit{AS}(\Pi)=\mathit{AS}(\Pi^{\prime})$.

It is easy to see that the above proposition holds by noting that any atom
$a\in\mathcal{A}^{\prime}\setminus\mathcal{A}$ can clearly not appear in the
rules $\mathcal{R}$, and hence any such $a$ must be false in any answer set of
$\Pi^{\prime}$ (i.e. for all $M\in\mathit{AS}(\Pi^{\prime})$ it holds that
$a\not\in M$). From this result, it is easy to obtain a similar result for
ELPs.

######  Proposition 30.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP and let
$\Pi^{\prime}=(\mathcal{A}^{\prime},\mathcal{E},\mathcal{R})$ be an ELP with
the same set of rules and domain of epistemic literals, but with
$\mathcal{A}^{\prime}\supset\mathcal{A}$. Then,
$\mathit{cwv}(\Pi)=\mathit{cwv}(\Pi^{\prime})$.

###### Proof.

Note that, clearly, any atom $a\in\mathcal{A}^{\prime}\setminus\mathcal{A}$
cannot appear anywhere in $\mathcal{R}$ or $\mathcal{E}$. Hence, for every
guess $\Phi\subseteq\mathcal{E}$, $a$ also does not appear in the rules of the
epistemic reduct $\Pi^{\prime\Phi}$ and thus also not in any answer set of
$\Pi^{\prime\Phi}$. But then,
$\mathit{AS}(\Pi^{\prime\Phi})=\mathit{AS}(\Pi^{\Phi})$. ∎

From the above, we can see that the atom domain of an ELP can be arbitrarily
extended without changing the CWVs of the ELP. We will now show that the same
is the case for the domain of epistemic literals.

######  Proposition 31.

Let $\Pi=(\mathcal{A},\mathcal{E},\mathcal{R})$ be an ELP and let
$\Pi^{\prime}=(\mathcal{A},\mathcal{E}^{\prime},\mathcal{R})$ be an ELP with
the same set of rules and atom domain, but with
$\mathcal{E}^{\prime}\supset\mathcal{E}$ and
$\mathcal{E}^{\prime}\setminus\mathcal{E}=\\{\mathbf{not}\,\ell\\}$. Then,
$\mathit{cwv}(\Pi)=\mathit{cwv}(\Pi^{\prime})$.

###### Proof.

Note that the epistemic literal $\mathbf{not}\,\ell$ cannot appear anywhere in
$\mathcal{R}$, but the atom in $\ell$ can be in $\mathcal{A}$ and appear in
$\mathcal{R}$. Now consider any guess $\Phi\subseteq\mathcal{E}$, which we
will relate to $\Phi^{\prime}=\Phi\cup\\{\mathbf{not}\,\ell\\}$. The rules of
the epistemic reducts $\Pi^{\Phi}$, $\Pi^{\prime\Phi}$, and
$\Pi^{\prime\Phi^{\prime}}$ coincide, thus
$\mathit{AS}(\Pi^{\Phi})=\mathit{AS}(\Pi^{\prime\Phi^{\prime}})=\mathcal{M}$.
First, consider the case that $\mathcal{M}$ is not compatible with $\Phi$, it
is not hard to see that then $\mathcal{M}$ is not compatible with
$\Phi^{\prime}$ either. Now assume that $\mathcal{M}$ is compatible with
$\Phi$, and thus $\mathcal{M}\in\mathit{cwv}(\Pi)$. We distinguish two cases:
(1) $\forall M\in\mathcal{M}:M\vDash\ell$, in this case $\Phi$ is compatible
with $\mathcal{M}$ (with respect to $\mathcal{E}^{\prime}$) and therefore
$\mathcal{M}\in\mathit{cwv}(\Pi^{\prime})$; (2) $\exists
M\in\mathcal{M}:M\not\vDash\ell$, in this case $\Phi^{\prime}$ is compatible
with $\mathcal{M}$ and thus $\mathcal{M}\in\mathit{cwv}(\Pi^{\prime})$. ∎

From Propositions 30 and 31 in that order, and their respective proofs,
Theorem 6 follows.

##  Appendix B Proof of Theorem 28

Let $\Pi_{r}=(\mathcal{A},\mathcal{E},\mathcal{R}_{r})$ and
$\Pi_{s}=(\mathcal{A},\mathcal{E},\mathcal{R}_{s})$ be the two single rule
ELPs with $\mathcal{R}_{r}=\\{r\\}$ and $\mathcal{R}_{s}=\\{s\\}$, and let
$r^{\Phi}$ and $s^{\Phi}$ be as in the previous section (cf. the paragraph
before Theorem 24).

($\Leftarrow$) Let $r,s$ be such that (a)–(e) hold. By Lemma 26 we need to
show that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$,
for all guesses $\Phi\subseteq\mathcal{E}$. If $\Phi$ is not consistent
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$
holds by trivial means. Hence, let $\Phi\subseteq\mathcal{E}$ be consistent.
If $\Pi_{s}^{\Phi}=\emptyset$, we get
$\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)=\mathcal{S}_{\mathcal{A}}$ and are
done. So suppose $\Pi_{s}^{\Phi}\neq\emptyset$. By (e) and definition of the
epistemic reduct, it follows that $\Pi_{r}^{\Phi}\neq\emptyset$. We next show
that either $\Phi$ is not realizable in $\Pi_{r}$ (hence,
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$ and
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$
obviously holds) or $r^{\Phi}$ and $s^{\Phi}$ apply to conditions
($\alpha$)–($\delta$) of Lemma 27. In the latter case, due to this lemma then
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Phi})\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Phi})$,
and it remains to show that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$.
Towards a contradiction suppose this inclusion does not hold. In the light of
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Phi})\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Phi})$,
it must be the case that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\mathcal{S}\mathcal{E}(\Pi_{r}^{\Phi})$
and $\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)=\emptyset$, i.e. $\Phi$ is not
realizable in $\Pi_{s}^{\Phi}$. By definition this means that there is no
subset of $\mathit{mods}(\Pi_{s}^{\Phi})$ that is compatible with $\Phi$.
However, since
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Phi})\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Phi})$,
it also follows that
$\mathit{mods}(\Pi_{r}^{\Phi})\subseteq\mathit{mods}(\Pi_{s}^{\Phi})$. Hence,
$\Phi$ cannot be realizable in $\Pi_{r}^{\Phi}$ either and thus
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$; a contradiction.

We continue to show that either $\Phi$ is not realizable in $\Pi_{r}$, or
$r^{\Phi}$ and $s^{\Phi}$ fulfill the conditions ($\alpha$)–($\delta$) of
Lemma 27. Recall that we assume that $r^{\Phi}$ and $s^{\Phi}$ exist, i.e. the
epistemic reducts are not empty. Hence,
$\Phi\subseteq\mathcal{E}\setminus(\mathbf{not}\,F^{\prime}\cup\mathbf{not}\,\neg
G^{\prime})$. In fact, the epistemic reducts are of the form
$r^{\Phi}=A\leftarrow B,\neg C,\neg D^{\Phi},\neg\neg E^{\Phi},\neg\neg F,\neg
G$ and $s^{\Phi}=A^{\prime}\leftarrow B^{\prime},\neg C^{\prime},\neg
D^{\prime\Phi},\neg\neg E^{\prime\Phi},\neg\neg F^{\prime},\neg G^{\prime}$,
where for $\Delta\in\\{D,D^{\prime}\\}$ we let
$\Delta^{\Phi}=\\{d\in\Delta\mid\mathbf{not}\,d\notin\Phi\\}$, and for
$\Gamma\in\\{E,E^{\prime}\\}$ we let
$\Gamma^{\Phi}=\\{e\in\Gamma\mid\mathbf{not}\,\neg e\notin\Phi\\}$.

We first show that condition ($\delta$) of Lemma 27 holds for $r^{\Phi}$ and
$s^{\Phi}$. Observe that for each $e\in E^{\Phi}$ with $e\in E^{\prime}$, also
$e\in E^{\prime\Phi}$. Hence from (d) we get $E^{\Phi}\subseteq B^{\prime}\cup
E^{\prime\Phi}\cup F^{\prime}$ and using $F\subseteq F^{\prime}$ from (e) we
observe $E^{\Phi}\cup F\subseteq B^{\prime}\cup E^{\prime\Phi}\cup F^{\prime}$
as desired.

We continue with condition ($\gamma$) of Lemma 27. Suppose it does not hold
for $r^{\Phi}$ and $s^{\Phi}$. We have to show that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$. Since the condition does
not hold for $r^{\Phi}$ and $s^{\Phi}$, we have $C\cup D^{\Phi}\cup
G\not\subseteq C^{\prime}\cup D^{\prime\Phi}\cup G^{\prime}$. Since
$G\subseteq G^{\prime}$ by (e), $C\cup D^{\Phi}\subseteq C^{\prime}\cup
D^{\prime\Phi}\cup G^{\prime}$. Note that $D^{\Phi}\subseteq C^{\prime}\cup
D^{\prime\Phi}\cup G^{\prime}$ follows from (c) and the fact that for each
$d\in D^{\Phi}$ with $d\in D^{\prime}$, also $d\in D^{\prime\Phi}$. Thus
$C\not\subseteq C^{\prime}\cup D^{\prime\Phi}\cup G^{\prime}$. Let $c\in
C\setminus(C^{\prime}\cup D^{\prime\Phi}\cup G^{\prime})$. Since we assume by
(c) $C\subseteq C^{\prime}\cup D^{\prime}\cup G^{\prime}$, we have two
observations: (i) $\mathbf{not}\,c\in\Phi$ (otherwise $c\in D^{\prime\Phi}$);
(ii) due to condition (c∗), we need that $r\not\rhd s$, since otherwise
$C\subseteq C^{\prime}\cup G^{\prime}$ would hold. From $r\not\rhd s$, it
follows that there is neither an element in $(A\cup C\cup D)\setminus
G^{\prime}$ that is different from $c$ nor is there an element in $B\cup E$
different from $F^{\prime}$. We show that no subset of models of $r^{\Phi}$ is
$\Phi$-compatible. First, observe that we would need for each such model that
all $f\in F^{\prime}$ are set ot true and all $g\in G^{\prime}$ are set to
false. Since $\mathbf{not}\,c\in\Phi$, we need among those models one that
sets $c$ to false. However, such a model does not exist: the only “positive”
atoms in $r^{\Phi}$ besides $c$ occur also in $G^{\prime}$ and are already set
to false; all “negative” atoms in $r^{\Phi}$ are also in $F^{\prime}$ and thus
are set to true. Hence, $\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$.

Next, we treat condition ($\beta$) of Lemma 27. Suppose it does not hold for
$r^{\Phi}$ and $s^{\Phi}$. Again, we need to show
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$. Since the condition does
not hold for $r^{\Phi}$ and $s^{\Phi}$, we have $B\not\subseteq B^{\prime}\cup
E^{\prime\Phi}\cup F^{\prime}$. Let $b\in B\setminus(B^{\prime}\cup
E^{\prime\Phi}\cup F^{\prime})$. Since we assume by (b) $B\subseteq
B^{\prime}\cup E^{\prime}\cup F^{\prime}$, we have two observations: (i)
$\mathbf{not}\,\neg b\in\Phi$ (otherwise $b\in E^{\prime\Phi}$); (ii) due to
condition (b∗), we need $r\not\RHD s$ since otherwise $B\subseteq
B^{\prime}\cup F^{\prime}$ would hold. From $r\not\RHD s$, it follows that
there is neither an element in $(B\cup E)\setminus F^{\prime}$ that is
different from $b$ nor is there an element in $A\cup C\cup D$ different from
$G^{\prime}$. We show that no subset of models of $r^{\Phi}$ is
$\Phi$-compatible. First, observe that we would need for each such model that
all $f\in F^{\prime}$ are set ot true and all $g\in G^{\prime}$ are set to
false. Since $\mathbf{not}\,\neg b\in\Phi$, we need among those models one
that sets $b$ to true. However, such a model does not exist: all “positive”
atoms in $r^{\Phi}$ occur also in $G^{\prime}$ and are already set to false;
the only “negative” atoms in $r^{\Phi}$ different to $b$ are also in
$F^{\prime}$ and thus are set to true. Hence,
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$.

For Condition ($\beta$’) of Lemma 27, once more suppose that is does not hold
for $r^{\Phi}$ and $s^{\Phi}$. We have
$X=A\cap(A^{\prime}\setminus(C^{\prime}\cup D^{\prime\Phi}\cup
G^{\prime}))\neq\emptyset$ and $B\not\subseteq B^{\prime}$. It follows that
$A\cap(A^{\prime}\setminus(C^{\prime}\cup G^{\prime}))\neq\emptyset$, and,
since (b∗’) holds, $r\not\rhd s$. On the other hand, since (b’) holds, we know
that for each $x\in X$, $x\in D^{\prime}$ and, hence $\mathbf{not}\,x\in\Phi$
(since $X$ does not contain an element from $D^{\prime\Phi}$). Fix some $a\in
X$. From $r\not\rhd s$ it follows that there is neither an element in $(A\cup
C\cup D)\setminus G^{\prime}$ that is different from $a$ nor is there an
element in $B\cup E$ different from $F^{\prime}$. We show that no subset of
models of $r^{\Phi}$ is $\Phi$-compatible. First, observe that we would need
for each such model that all $f\in F^{\prime}$ are set ot true and all $g\in
G^{\prime}$ are set to false. Since $\mathbf{not}\,a\in\Phi$, we need among
those models one that sets $a$ to false. However, such a model does not exist:
the only “positive” atoms in $r^{\Phi}$ besides $a$ occur also in $G^{\prime}$
and are already set to false; all “negative” atoms in $r^{\Phi}$ are also in
$F^{\prime}$ and thus are set to true. Hence,
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$.

It remains to show that condition ($\alpha$) of Lemma 27 applies to $r^{\Phi}$
and $s^{\Phi}$. The argument is similar to the one for condition ($\gamma$).
So, suppose the condition does not hold for $r^{\Phi}$ and $s^{\Phi}$, i.e. we
have $A\not\subseteq A^{\prime}\cup C^{\prime}\cup D^{\prime\Phi}\cup
G^{\prime}$. Let $a\in A\setminus(A\cup C^{\prime}\cup D^{\prime\Phi}\cup
G^{\prime})$. Due to assumption (a), (i) $\mathbf{not}\,a\in\Phi$ (otherwise
$a\in D^{\prime\Phi}$); (ii) $r\not\rhd s$, since otherwise $A\subseteq
A^{\prime}\cup C^{\prime}\cup G^{\prime}$ via assumption (a∗). From $r\not\rhd
s$, it follows that there is neither an element in $(A\cup C\cup D)\setminus
G^{\prime}$ that is different from $a$ nor is there an element in $B\cup E$
different from $F^{\prime}$. Showing that no subset of models of $r^{\Phi}$ is
$\Phi$-compatible follows essentially the same arguments as used for condition
(c) above. Hence, we end up with
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\emptyset$ as desired. This concludes
the proof of the only-if direction.

($\Rightarrow$) Suppose one of the conditions (a)–(e) is violated. We show
that there exists a guess $\Phi$, such that
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)\not\subseteq\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)$.

Let us first consider (e) is violated and let
$\Phi=\mathcal{E}\setminus(\mathbf{not}\,F^{\prime}\cup\mathbf{not}\,\neg
G^{\prime})$. We get $r^{\Phi}=\emptyset$ and thus
$\mathcal{S}\mathcal{E}_{\Pi_{r}}(\Phi)=\mathcal{S}_{\mathcal{A}}$, while
$s^{\Phi}=A^{\prime}\leftarrow B^{\prime},\neg C^{\prime},\neg\neg
F^{\prime},\neg G^{\prime}$ (note that $D^{\prime}$ and $E^{\prime}$
dissappear since we assume $s$ to be non-tautological). It can be checked
that, since $s$ is non-tautological, so is $s^{\Phi}$, and thus
$\mathcal{S}\mathcal{E}_{\Pi_{s}}(\Phi)\subset\mathcal{S}_{\mathcal{A}}$. For
the remaining cases, let us assume (e) holds. Note that then $r^{\Phi}$ is
non-empty as well. In fact, it is of the form $r^{\Phi}=A\leftarrow B,\neg
C,\neg D^{\Phi},\neg\neg E^{\Phi},\neg\neg F,\neg G$ with $D^{\Phi}=\\{d\in
D\mid\mathbf{not}\,d\notin\Phi\\}$ and $E^{\Phi}=\\{e\in
E\mid\mathbf{not}\,\neg e\notin\Phi\\}$.

First, suppose (d) is violated. We consider
$\Psi=\Phi\setminus\\{\mathbf{not}\,\neg e\\}$ with $e\in
E\setminus(B^{\prime}\cup E^{\prime}\cup F^{\prime})$. Since
$\Psi\subseteq\Phi$, $r^{\Psi}$ and $s^{\Psi}$ are non-empty. In fact,
$s^{\Psi}=s^{\Phi}$ since $e\notin E^{\prime}$. Moreover in $r^{\Psi}$ we have
$e\in E^{\Psi}$. We observe that condition ($\delta$) of Lemma 27 is violated,
and, from the same lemma, we get that
$\mathcal{S}\mathcal{E}(\Pi^{\Psi}_{r})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\mathit{mods}(\Pi^{\Psi}_{r})$ realizes $\Psi$. Note
that any interpretation that sets $e$ to false is a model of $r^{\Psi}$. We
thus take $\mathcal{I}$ as the set of interpretations where $e$ is set to
false, all $f\in F^{\prime}$ are set to true, and all $g\in G^{\prime}$ are
set to false. Indeed, $\mathcal{I}\subseteq\mathit{mods}(r^{\Psi})$ since
$\mathcal{I}$ is a set of well-formed interpretations (recall that $e\notin
F^{\prime}$, and $F^{\prime}\cap G^{\prime}=\emptyset$ since we assumed $s$ to
be non-tautological). We show that the three conditions for $\mathcal{I}$
being $\Psi$-compatible hold. (i) $\mathcal{I}\neq\emptyset$ by definition;
(ii) for any $\mathbf{not}\,\ell\in\Psi$, there exists an $I\in\mathcal{I}$,
such that $I\not\vDash\ell$: by definition $\ell\notin\\{\neg e\\}\cup
F^{\prime}\cup\neg G^{\prime}$. For $\ell=e$, $I\not\vDash e$ hold for all
$I\in\mathcal{I}$. Similary this is true for $\ell\in\neg F^{\prime}$ and for
all $\ell\in G^{\prime}$. For all other $\ell$ such that
$\mathbf{not}\,\ell\in\Psi$, there is one $I\in\mathcal{I}$ such that
$I\not\vDash\ell$ by construction of $\mathcal{I}$; (iii) we show that for any
$\mathbf{not}\,\ell\in\mathcal{E}\setminus\Psi$, and for each each
$I\in\mathcal{I}$, $I\vDash\ell$. Indeed, by construction of $\Psi$, $\ell$ is
either $\neg e$, $f\in F^{\prime}$ or $\neg g\in\neg G^{\prime}$; by
definition, for each $I\in\mathcal{I}$ it holds that $I\vDash\ell$.

Suppose (c) is violated. We consider $\Psi=\Phi\setminus\\{\mathbf{not}\,c\\}$
with $c\in(C\cup D)\setminus(C^{\prime}\cup D^{\prime}\cup G^{\prime})$. Since
$\Psi\subseteq\Phi$, $r^{\Psi}$ and $s^{\Psi}$ are non-empty. In fact,
$s^{\Psi}=s^{\Phi}$ since $c\notin D^{\prime}$. Moreover in $r^{\Psi}$ we have
$c\in D^{\Psi}$, for the case $c\notin C$. Thus, $c\in C\cup D^{\Psi}$. We
observe that condition ($\gamma$) of Lemma 27 is thus violated, and, by the
same lemma, we get that
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Psi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\Psi$ is realizable in
$\mathit{mods}(\Pi_{r}^{\Psi})$. Indeed, any interpretation that sets $c$ to
true is a model of $r^{\Psi}$. We take $\mathcal{I}$ as the set of
interpretations where $c$ is set to true, all $f\in F^{\prime}$ are set to
true, and all $g\in G^{\prime}$ are set to false. As before, one can show that
$\mathcal{I}$ is a set of well-formed interpretations (in paricular, since
$c\notin G^{\prime}$) and $\Psi$-compatible.

Suppose (c∗) is violated, i.e. we have $|(A\cup C\cup D)\setminus
G^{\prime}|>1$ or $(B\cup E)\setminus F^{\prime}\neq\emptyset$, but
$C\not\subseteq C^{\prime}\cup G^{\prime}$. Let $c\in
C\setminus(C^{\prime}\cup G^{\prime})$. Hence, (1) there exists at least one
atom $x$ different from $c$ that appears in $A\cup C\cup D$ but not in
$G^{\prime}$, or (2) there is some atom $y$ in $(B\cup E)\setminus
F^{\prime}$. Let $\ell=x$ for case (1) and $\ell=\neg y$ for case (2), and
consider $\Psi=\Phi\setminus\\{\mathbf{not}\,\ell\\}$. Since
$\Psi\subseteq\Phi$, $r^{\Psi}$ and $s^{\Psi}$ are non-empty. We observe that
$s^{\Psi}=A^{\prime}\leftarrow B^{\prime},\neg C^{\prime},\neg
D^{\prime\Psi},\neg\neg E^{\prime\Psi},\neg\neg F^{\prime},\neg G^{\prime}$
satisfies $c\notin D^{\prime\Psi}$ (for case (1) recall that $c\neq x$).
Hence, we have $c\in C$ but $c\notin C^{\prime}\cup D^{\prime\Psi}\cup
G^{\prime}$. As before, condition ($\gamma$) of Lemma 27 is thus violated, and
we conclude
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Psi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\mathit{mods}(\Pi_{r}^{\Psi})$ realizes $\Psi$. Here,
any interpretation $I$ that satisfies $\ell$ (i.e. where $x\in I$ in case (1);
otherwise $y\notin I$) is a model of $r^{\Psi}$. We take $\mathcal{I}$ as the
set of interpretations in which $\ell$ is true, all $f\in F^{\prime}$ are set
to true, and all $g\in G^{\prime}$ are set to false. Indeed, $\mathcal{I}$
contains well-formed interpretations, since $x\notin G^{\prime}$ and likewise,
$y\notin F^{\prime}$. As before, one can show that $\mathcal{I}$ is
$\Psi$-compatible.

Suppose (b) is violated. We consider $\Psi=\Phi\setminus\\{\mathbf{not}\,\neg
b\\}$ with $b\in B\setminus(B^{\prime}\cup E^{\prime}\cup F^{\prime})$. Since
$\Psi\subseteq\Phi$, $r^{\Psi}$ and $s^{\Psi}$ are non-empty. In fact,
$s^{\Psi}=s^{\Phi}$ since $b\notin E^{\prime}$. Thus, condition ($\beta$) of
Lemma 27 is violated, and, by the same lemma, we have
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Psi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\mathit{mods}(\Pi_{r}^{\Psi})$ realizes $\Psi$.
Indeed, any interpretation that sets $b$ to false is a model of $r^{\Psi}$. We
take $\mathcal{I}$ as the set of interpretations where $b$ is set to false,
all $f\in F^{\prime}$ are set to true, and all $g\in G^{\prime}$ are set to
false. This is again sound since $b\notin F^{\prime}$. As before, one can show
that $\mathcal{I}$ is $\Psi$-compatible.

Suppose (b∗) is violated, i.e. we have $(A\cup C\cup D)\setminus
G^{\prime}\neq\emptyset$ or $|(B\cup E)\setminus F^{\prime}|>1$, but
$B\not\subseteq B^{\prime}\cup F^{\prime}$. Let $b\in
B\setminus(B^{\prime}\cup F^{\prime})$. Hence, there exists (1) an atom $x$ in
$(A\cup C\cup D)\setminus G^{\prime}$, or (2) an atom $y$ different to $b$
that appears in $(B\cup E)\setminus F^{\prime}$. Let $\ell=x$ in case (1) and
$\ell=\neg y$ in case (2), and consider
$\Psi=\Phi\setminus\\{\mathbf{not}\,\ell\\}$. Since $\Psi\subseteq\Phi$,
$r^{\Psi}$ and $s^{\Psi}$ are non-empty. We observe that
$s^{\Psi}=A^{\prime}\leftarrow B^{\prime},\neg C^{\prime},\neg
D^{\prime\Psi},\neg\neg E^{\prime\Psi},\neg\neg F^{\prime},\neg G^{\prime}$
satisfies $b\notin E^{\prime\Psi}$ (for case (2) recall that $b\neq y$).
Hence, we have $b\in B$ but $b\notin B^{\prime}\cup E^{\prime\Psi}\cup
F^{\prime}$. As before, condition ($\beta$) of Lemma 27 is violated, and we
conclude
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Psi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\mathit{mods}(\Pi_{r}^{\Psi})$ realizes $\Psi$. Here,
any interpretation that sets $\ell$ to true (i.e. $x$ is set true in case (1);
otherwise $y$ is set to false) is a model of $r^{\Psi}$. We take $\mathcal{I}$
as the set of all interpretations wherein $\ell$ is true, all $f\in
F^{\prime}$ are set to true, and all $g\in G^{\prime}$ are set to false.
Indeed, $\mathcal{I}$ contains well-formed interpretations, since $x\notin
G^{\prime}$ and likewise, $y\notin F^{\prime}$. One can show that
$\mathcal{I}$ is $\Psi$-compatible by the usual argument.

Suppose (b’) is violated, i.e. we have
$X=A\cap(A^{\prime}\setminus(C^{\prime}\cup D^{\prime}\cup
G^{\prime}))\neq\emptyset$ and $B\not\subseteq B^{\prime}$. Consider
$\Psi=\Phi\setminus\\{\mathbf{not}\,a\\}$ with $a\in X$. In particular, this
implies $a\notin D^{\prime}$. Since $\Psi\subseteq\Phi$, $r^{\Psi}$ and
$s^{\Psi}$ are non-empty. In fact, $s^{\Psi}=s^{\Phi}$ since $a\notin
D^{\prime}$. We observe that condition ($\beta^{\prime}$) of Lemma 27 is thus
violated, and, by the same lemma, we get that
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Psi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Psi})$.
It remains to show that $\mathit{mods}(\Pi_{r}^{\Psi})$ realizes $\Psi$.
Indeed, any interpretation that sets $a$ to true is a model of $r^{\Psi}$. We
take $\mathcal{I}$ as the set of interpretations where $a$ is set to true, all
$f\in F^{\prime}$ are set to true, and all $g\in G^{\prime}$ are set to false.
This is again sound since $a\notin G^{\prime}$ (by construction of $X$).

Suppose (b∗’) is violated, i.e. $|(A\cup C\cup D)\setminus G^{\prime}|>1$ or
$(B\cup E)\setminus F^{\prime}\neq\emptyset$, as well as
$X=A\cap(A^{\prime}\setminus(C^{\prime}\cup G^{\prime}))\neq\emptyset$ and
$B\not\subseteq B^{\prime}$. For this case, we consider the rules $r^{\Phi}$
and $s^{\Phi}$ directly. In fact, for these rules, $X$ and $B\not\subseteq
B^{\prime}$ immediately imply that condition ($\beta^{\prime}$) of Lemma 27 is
violated, and we conclude
$\mathcal{S}\mathcal{E}(\Pi_{r}^{\Phi})\not\subseteq\mathcal{S}\mathcal{E}(\Pi_{s}^{\Phi})$.
We show that $\mathcal{M}=\mathit{mods}(\Pi_{r}^{\Phi})$ realizes $\Phi$. Note
that in this particular case, $r^{\Phi}$ has at least two literals not
“absorbed” by $F^{\prime}$ and $G^{\prime}$; viz. $x\in X$ and some $\ell\neq
x$ from $(A\cup C\cup D)\setminus(G^{\prime}\cup\\{x\\})$ or from $(B\cup
E)\setminus F^{\prime}$. If we consider the set
$\mathcal{M}^{\prime}\subseteq\mathcal{M}$ of models where all $f\in
F^{\prime}$ are set to true, and all $g\in G^{\prime}$ are set to false, we
observe that for all other atoms $y$, there exists at least one model in
$\mathcal{M}^{\prime}$ where $y$ is set to false and another one where $y$ is
set to true. In particular, there is an $M\in\mathcal{M}$ where $x$ is false
(namely the one where $\ell$ is set to true), and likewise there is an
$M\in\mathcal{M}$ where $\ell$ is false (namely the one where $x$ is set to
true).

Cases (a) and (a∗) are similar to (c) and (c∗): simply apply Lemma 27 via
condition ($\alpha$) instead of ($\gamma$).

## References

  * [Bichler, Morak, and Woltran 2018] Bichler, M.; Morak, M.; and Woltran, S.  2018\.  Single-shot epistemic logic program solving.  In Lang, J., ed., Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., 1714–1720.  ijcai.org.
  * [Brewka, Eiter, and Truszczynski 2011] Brewka, G.; Eiter, T.; and Truszczynski, M.  2011\.  Answer set programming at a glance.  Commun. ACM 54(12):92–103.
  * [Cabalar, Pearce, and Valverde 2007] Cabalar, P.; Pearce, D.; and Valverde, A.  2007\.  Minimal logic programs.  In Dahl, V., and Niemelä, I., eds., Logic Programming, 23rd International Conference, ICLP 2007, Porto, Portugal, September 8-13, 2007, Proceedings, volume 4670 of Lecture Notes in Computer Science, 104–118.  Springer.
  * [Eiter and Gottlob 1995] Eiter, T., and Gottlob, G.  1995\.  On the computational cost of disjunctive logic programming: Propositional case.  Ann. Math. Artif. Intell. 15(3-4):289–323.
  * [Eiter et al. 2007] Eiter, T.; Faber, W.; Fink, M.; and Woltran, S.  2007\.  Complexity results for answer set programming with bounded predicate arities and implications.  Ann. Math. Artif. Intell. 51(2-4):123–165.
  * [Eiter et al. 2013] Eiter, T.; Fink, M.; Pührer, J.; Tompits, H.; and Woltran, S.  2013\.  Model-based recasting in answer-set programming.  Journal of Applied Non-Classical Logics 23(1-2):75–104.
  * [Eiter, Fink, and Woltran 2007] Eiter, T.; Fink, M.; and Woltran, S.  2007\.  Semantical characterizations and complexity of equivalences in answer set programming.  ACM Trans. Comput. Log. 8(3).
  * [Fariñas del Cerro, Herzig, and Su 2015] Fariñas del Cerro, L.; Herzig, A.; and Su, E. I.  2015\.  Epistemic equilibrium logic.  In Yang, Q., and Wooldridge, M., eds., Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, 2964–2970.  AAAI Press.
  * [Gelfond and Lifschitz 1988] Gelfond, M., and Lifschitz, V.  1988\.  The stable model semantics for logic programming.  In Kowalski, R. A., and Bowen, K. A., eds., Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, August 15-19, 1988 (2 Volumes), 1070–1080.  MIT Press.
  * [Gelfond and Lifschitz 1991] Gelfond, M., and Lifschitz, V.  1991\.  Classical negation in logic programs and disjunctive databases.  New Generation Comput. 9(3/4):365–386.
  * [Gelfond 1991] Gelfond, M.  1991\.  Strong introspection.  In Dean, T. L., and McKeown, K. R., eds., Proceedings of the 9th National Conference on Artificial Intelligence, Anaheim, CA, USA, July 14-19, 1991, Volume 1, 386–391.  AAAI Press / The MIT Press.
  * [Gelfond 1994] Gelfond, M.  1994\.  Logic programming and reasoning with incomplete information.  Ann. Math. Artif. Intell. 12(1-2):89–116.
  * [Gelfond 2011] Gelfond, M.  2011\.  New semantics for epistemic specifications.  In Delgrande, J. P., and Faber, W., eds., Logic Programming and Nonmonotonic Reasoning - 11th International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings, volume 6645 of Lecture Notes in Computer Science, 260–265.  Springer.
  * [Kahl et al. 2015] Kahl, P. T.; Watson, R.; Balai, E.; Gelfond, M.; and Zhang, Y.  2015\.  The language of epistemic specifications (refined) including a prototype solver.  J. Log. Comput. 25\.
  * [Kahl 2014] Kahl, P. T.  2014\.  Refining the Semantics for Epistemic Logic Programs.  Ph.D. Dissertation, Texas Tech University, Texas, USA.
  * [Lifschitz, Pearce, and Valverde 2001] Lifschitz, V.; Pearce, D.; and Valverde, A.  2001\.  Strongly equivalent logic programs.  ACM Trans. Comput. Log. 2(4):526–541.
  * [Lifschitz, Tang, and Turner 1999] Lifschitz, V.; Tang, L. R.; and Turner, H.  1999\.  Nested expressions in logic programs.  Ann. Math. Artif. Intell. 25(3-4):369–389.
  * [Lin and Chen 2007] Lin, F., and Chen, Y.  2007\.  Discovering classes of strongly equivalent logic programs.  J. Artif. Intell. Res. 28:431–451.
  * [Pearce, Tompits, and Woltran 2009] Pearce, D.; Tompits, H.; and Woltran, S.  2009\.  Characterising equilibrium logic and nested logic programs: Reductions and complexity.  TPLP 9(5):565–616.
  * [Reiter 1977] Reiter, R.  1977\.  On closed world data bases.  In Logic and Data Bases, Symposium on Logic and Data Bases, Centre d’études et de recherches de Toulouse, France, 1977., 55–76.
  * [Schaub and Woltran 2018] Schaub, T., and Woltran, S.  2018\.  Special issue on answer set programming.  KI 32(2-3).
  * [Shen and Eiter 2016] Shen, Y., and Eiter, T.  2016\.  Evaluating epistemic negation in answer set programming.  Artif. Intell. 237:115–135.
  * [Son et al. 2017] Son, T. C.; Le, T.; Kahl, P. T.; and Leclerc, A. P.  2017\.  On computing world views of epistemic logic programs.  In Sierra, C., ed., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, 1269–1275.  ijcai.org.
  * [Truszczynski 2011] Truszczynski, M.  2011\.  Revisiting epistemic specifications.  In Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday.
  * [Turner 2003] Turner, H.  2003\.  Strong equivalence made easy: nested expressions and weight constraints.  TPLP 3(4-5):609–622.
  * [Wang and Zhang 2005] Wang, K., and Zhang, Y.  2005\.  Nested epistemic logic programs.  In Baral, C.; Greco, G.; Leone, N.; and Terracina, G., eds., Logic Programming and Nonmonotonic Reasoning, 8th International Conference, LPNMR 2005, Diamante, Italy, September 5-8, 2005, Proceedings, volume 3662 of LNCS, 279–290.  Springer.