# Thirty years of Epistemic Specifications

Jorge Fandinno12 Wolfgang Faber3 and Michael Gelfond4
1University of Nebraska Omaha  USA
2University of Potsdam  Germany

3Alpen-Adria-Universität Klagenfurt<EMAIL_ADDRESS>Austria

4Texas Tech University<EMAIL_ADDRESS>USA

<EMAIL_ADDRESS>
###### Abstract

The language of _epistemic specifications_ and _epistemic logic programs_
extends disjunctive logic programs under the _stable model_ semantics with
modal constructs called subjective literals. Using subjective literals, it is
possible to check whether a regular literal is true in every or some stable
models of the program, those models, in this context also called _belief sets_
, being collected in a set called _world view_. This allows for representing,
within the language, whether some proposition should be understood accordingly
to the open or the closed world assumption. Several attempts for capturing the
intuitions underlying the language by means of a formal semantics were given,
resulting in a multitude of proposals that makes it difficult to understand
the current state of the art. In this paper, we provide an overview of the
inception of the field and the knowledge representation and reasoning tasks it
is suitable for. We also provide a detailed analysis of properties of proposed
semantics, and an outlook of challenges to be tackled by future research in
the area.

##  1 Introduction

The language of _epistemic specifications_ [Gelfond (1991), Gelfond and
Przymusinska (1993a), Gelfond (1994)] (a.k.a. _epistemic logic programs_),
proposed by Gelfond in 1991, extends disjunctive logic programs (under the
_stable model_ semantics; gellif88b,gellif91a) with modal constructs called
_subjective literals_. The introduction of this extension was originally
motivated by the need to correctly represent incomplete information in
programs that have several stable models. Using subjective literals, it is
possible to check whether a regular literal is true in every or some stable
models of the program, those models being collected in a set called _world
view_. This allows for representing, within the language, whether some
proposition should be understood accordingly to the open or the closed world
assumption.

Unfortunately, as first noticed by Teodor Przymusinski, world views of
epistemic specifications in this original semantics do not always correspond
to those intended by the authors. This was due to the presence of unsupported
beliefs. Attempts to get rid of these unsupported beliefs were first made by
Gelfond in gelfond94 and later in gelfond11a, followed by many other authors
who proposed several new semantics attempting to solve this problem. Somewhat
complicating matters, there were also proposals for extending or changing the
language. In this paper, we present a summary of the state of the art
regarding epistemic specifications.

The structure of the paper is as follows. In Section 2, an account of the
inception of the field is provided. This also describes the main intuitions
underlying epistemic specifications. We then review the formal details of
epistemic specifications and provide an updated view of the ideas behind the
original definition of epistemic specifications (Section 3). The language of
epistemic specifications is general enough to accommodate the syntax of most
proposals in the literature, but we also define the language of epistemic
logic programs, which is the fragment treated by most proposals. In Section 4,
we review some of the representation problems that epistemic specifications
can help to solve. We relate these problems with some formal properties that
help understanding the behavior for that specific task. Namely, we revisit the
use of epistemic specifications to express integrity constraints over
disjunctive databases, informally discussed in Section 2, but including
technical details. Then, we illustrate how epistemic specifications are also
useful when we need to reason about all the answer sets of a program at the
same time, which is not possible by simply using Answer Set Prolog. We show
also how we can extend the guess-define-and-test methodology from Answer Set
Programming to problems that lie on the second level of the polynomial
hierarchy: in particular we illustrate this methodology showing how epistemic
logic programs can be used to find conformant plans. Finally, we provide an
example from cybersecurity. In Section 5, we survey the path followed in the
attempt to get rid of self-supported beliefs and the different approaches
proposed in the literature. We also show which properties are satisfied (or
not) by the various semantics and describe some deeper relationships between
some of the semantics. Section 6 puts epistemic specifications in the broader
context of Knowledge Representation by studying the relation between epistemic
specifications and autoepistemic logics. Finally, Section 8 concludes the
paper and presents some challenges for the future.

##  2 The Inception

The idea of epistemic specifications was initially suggested in three
consecutive papers [Gelfond (1991), Gelfond and Przymusinska (1993b), Gelfond
(1994)]. This work was a part of the larger research program, originated by
John McCarthy and others in the late fifties. The program aimed to develop
knowledge representation languages capable of clear and succinct formalization
of substantial parts of commonsense knowledge and commonsense reasoning
methods. A substantial step in this direction was made by gellif91a, who
extended the language of “classical” logic programming with disjunction and
classical negation.111Often referred to as strong or explicit negation. The
new language allowed reasoning with some forms of incomplete information. For
instance, for a program with one answer set, say $S$, a statement “the truth
or falsity of $p$ is _unknown_ ” can be expressed in Answer Set Prolog as

$\displaystyle\operatorname{\text{not}}p,\,\operatorname{\text{not}}\text{-}p$

where “$\operatorname{\text{not}}$” and “-” respectively stand for default and
classical negation. The Closed World Assumption (CWA; reiter78a), stating that
“$p(X)$ is false unless there is a reason to believe it to be true” has the
form

$\displaystyle\text{-}p(X)\leftarrow\operatorname{\text{not}}p(X),$ (1)

These representations, however, do not work for programs with multiple answer
sets. The main goal of epistemic specifications was to address this
deficiency. As stated by gelfond91a, we wanted to “expand the syntax and
semantics of logic programs and deductive databases to allow for the correct
representation of incomplete information in the presence of multiple
extensions.” The main idea was to expand the syntax and semantics of Answer
Set Prolog by modal operators $\operatorname{\mathbf{K}}$ and
$\operatorname{\mathbf{M}}$ where $\operatorname{\mathbf{K}}F$ holds if $F$ is
true in all answer sets of a program and $\operatorname{\mathbf{M}}F$ holds if
$F$ is true in at least one answer set. In this notation

$\operatorname{\text{not}}\operatorname{\mathbf{K}}p,\,\operatorname{\text{not}}\operatorname{\mathbf{K}}\text{-}p$

would correspond to “the truth value of $p$ is unknown” even in the presence
of multiple answer sets; the CWA for a relation $p$ could be expressed as

$\text{-}p(X)\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{M}}p(X).$

In a language containing object constants $a$, $b$ and $c$ this rule, combined
with a rule

$\displaystyle p(a)\operatorname{\,\text{or}\,}p(b)$

would produce answer _No_ to a query $p(c)?$, but remain undecided about query
$p(a)?$. The same behavior will, of course, be produced by the original
representation (1) of CWA. However, for a more complex query, say

$\displaystyle(\text{-}p(a)\operatorname{\,\text{or}\,}\text{-}p(b))?$

the behaviors differ: the former answers the query by _Yes_ , while the latter
remains undecided. This was intended – we wanted a form of CWA not applicable
to undecided disjuncts.

The new features of epistemic specifications were not limited to modal
operators. Rules were allowed to contain more general formulas (most
importantly existential quantifiers). In addition to usual (Herbrand) objects
constants, there were also so called _generic constants_ used to refer to
_unnamed_ objects. The former were defined by atoms of the form $h(c)$ (where
$h$ stands for Herbrand), listing all the named objects of the domain,
together with the rule

$\displaystyle\text{-}h(X)\leftarrow\mbox{not }h(X).$

This separation between named and unnamed objects allowed representation of
information which would be difficult to express otherwise. In particular, it
was used to remove the Domain Closure Assumption from the semantics of logic
programs. Instead the assumption, which states that “all objects in the domain
of discourse described by a program $\Pi$ have names in the signature of
$\Pi$”, could be expressed by the constraint

$\leftarrow\exists X\,\text{-}h(X).$

Existential quantifiers combined with modal operators were shown to be
instrumental in expressing various forms of constraints understood as
statements about the content of the knowledge base as opposed to statements
about the world [Reiter (1992)]. Consider, for instance, knowledge base $T$

$\displaystyle\begin{aligned} &\mathit{h(bob)}\ \ \ \ \ \ \mathit{h(mary)}\\\
&\mathit{teach(bob,java)}\\\ &\mathit{teach(staff,python)}\\\
&\mathit{teach(bob,ai)}\operatorname{\,\text{or}\,}\mathit{teach(mary,ai)}.\end{aligned}$
(2)

where $\mathit{bob}$ and $\mathit{mary}$ are professors in the department, and
$\mathit{staff}$ refers to a professor yet to be hired. Then a constraint

$\displaystyle\exists
X\operatorname{\mathbf{K}}(h(X)\wedge\mathit{teach}(X,C))$ (3)

is satisfied by $C=\mathit{java}$ (which is taught by Bob). A weaker
constraint

$\displaystyle\exists X\operatorname{\mathbf{K}}\mathit{teach}(X,C)$ (4)

is satisfied by $C=\mathit{java}$ and by $C=\mathit{python}$;

$\displaystyle\operatorname{\mathbf{K}}\exists X\mathit{teach}(X,C)$ (5)

is satisfied by all three classes ($\mathit{java}$, $\mathit{python}$,
$\mathit{ai}$).

The semantics of the language was similar to that of Answer Set Prolog. In
both cases a program was viewed as a specification of sets of beliefs that
could be held by a rational reasoner associated with the program. But, while
in Answer Set Prolog rules constrain the formation of each set of beliefs
(i.e. each answer set) independently from others, in epistemic specifications
restrictions are put also on the relationship between such sets. This
intuition led to the notion of a _world view_ – a collection of answer sets
formed simultaneously by a rational agent to satisfy the program’s rules. The
key technical problem, as in the semantics of Answer Set Prolog, was to find
the proper definition of a reduct capturing rationality of the agent. While
the original paper [Gelfond (1991)] had an egregious error in this definition
(to the best of the author’s recollection introduced at the last moment in the
attempt to satisfy time and space requirements of the conference) other two
papers [Gelfond and Przymusinska (1993b), Gelfond (1994)] had a definition
believed to be reasonable. It soon became clear, however, that this belief was
unjustified. To see the reason, consider an epistemic specification consisting
of one rule:

$\displaystyle p\leftarrow\operatorname{\mathbf{K}}p.$ (6)

To the authors’ surprise it was noticed that, according to the definition
proposed by gelfondP93 and latter used by gelfond94, it has two world views:
$[\\{\,\\}]$ and $[\\{p\\}]$. The latter contains the unsupported belief $p$
and is clearly unintended. According to the rationality principle, which
serves as the foundation of the semantics of Answer Set Prolog, an agent is
not supposed to believe anything that it is not forced to believe, which is
the case in the second world view. For some time Gelfond had been trying to
modify the definition but, after a few years of failure, gave up on the idea.

In gelfond11a, Gelfond gave yet another attempt to modify this definition and
was soon joined by many other authors in this attempt, with several new
semantics attempting to solve this problem [Kahl et al. (2015), Fariñas del
Cerro et al. (2015), Shen and Eiter (2016), Shen and Eiter (2017), Cabalar et
al. (2019a), Iraz Su et al. (2020)].

Admittedly, rule (6) is unlikely to be written by a programmer. It is,
however, used here to distill a phenomenon that can occur as a result of more
complex and reasonable rules. As an example consider the following rule

$\displaystyle r(Y)\leftarrow\operatorname{\mathbf{K}}r(X)\wedge edge(X,Y)$

saying that if in a world view $\mathbb{W}$, property $r$ is known to be true
in state $X$, and $Y$ is a successor of $X$ then $r(Y)$ must be included in
every belief set of $\mathbb{W}$. When this rule is combined with facts
$edge(a,b)$, $edge(c,d)$ and $edge(d,c)$ representing a graph and the fact
$r(a)$ stating that the property $r$ is satisfied in state $a$, we can observe
that the resultant program suffers from the same problem as (6).

##  3 Epistemic Theories

In this section, we review the syntax of epistemic theories. We present a
language flexible enough to relate all the approaches that we will study in
this paper. We start by introducing epistemic theories in a general way and
later we review a specific subset corresponding closely to the syntax of logic
programs.

###  3.1 General Syntax

The language of epistemic specifications is that of first-order modal logic
[Fitting and Mendelsohn (1998)] extended with explicit negation. We follow the
convention of the literature on epistemic specifications for writing modal
operations. That is, symbols $\operatorname{\mathbf{K}}$ and
$\operatorname{\mathbf{M}}$ are used in place of $\Box$ and $\Diamond$,
respectively. Terms and atoms are defined as usual in first-order (non-modal)
logic. Formulas are defined according to the following grammar:

$F\ ::=\ \bot\,\mid\,\top\,\mid\,a\,\mid\,\text{-}F\,\mid\,F_{1}\wedge
F_{2}\,\mid\,F_{1}\vee F_{2}\,\mid\,F_{1}\leftarrow
F_{2}\,\mid\,\operatorname{\mathbf{K}}F\,\mid\,\operatorname{\mathbf{M}}F\,\mid\,\exists
x\,F\,\mid\,\forall x\,F$

with $a\in\text{\em At}$ an atom and $x$ an object variable. We assume that
${\operatorname{\text{not}}F}$ is an abbreviation for ${\bot\leftarrow F}$. We
call “-” _explicit negation_ and “$\operatorname{\text{not}}$” _default
negation_. An occurrence of a variable $x$ in a formula $F$ is bound if it
belongs to a subformula of $F$ that has the forms $\forall x\,G$ or $\exists
x\,G$; otherwise it is free. A _sentence_ is a formula without free variables.
An _(epistemic) theory_ $\Gamma$ is a set of sentences. We sometimes write
formulas with free variables that should be understood as their universal
closure.

An _explicit literal_ is either an atom or a formula of the form $\text{-}a$
with $a$ being an atom. Terms, atoms, explicit literals and formulas not
containing variables are called _ground_.

###  3.2 Monotonic semantics

We introduce here two monotonic semantics for epistemic theories that will be
instrumental in defining the non-monotonic semantics in the next section. The
semantics discussed here coincide with those of modal logics S5 and KD45
extended with strong negation [Nelson (1949), Vakarelov (1977)].

An _interpretation_ is a set of ground explicit literals $I$ such that either
${a\notin I}$ or ${\text{-}a\notin I}$ for every atom $a$. An _epistemic
interpretation_ $\mathbb{W}$ is a non-empty set of interpretations. A _belief
interpretation_ $\mathcal{I}=\langle\mathbb{W},I\rangle$ is a pair where $I$
is a propositional interpretation and $\mathbb{W}$ is an epistemic
interpretation. We write ${\langle\mathbb{W},I\rangle\models F}$ to represent
that a belief interpretation ${\langle\mathbb{W},I\rangle}$ _satisfies_ a
sentence $F$ and ${\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F}$ to represent
that a belief interpretation ${\langle\mathbb{W},I\rangle}$ _falsifies_ a
sentence $F$. These two relation are defined according to the following
mutually recursive conditions:

  1. 1.

$\langle\mathbb{W},I\rangle\models\top$;

  2. 2.

$\langle\mathbb{W},I\rangle\models a$ if $a\in I$, for any atom $a\in\text{\em
At}$:

  3. 3.

$\langle\mathbb{W},I\rangle\models F\wedge G$ if
$\langle\mathbb{W},I\rangle\models F$ and $\langle\mathbb{W},I\rangle\models
G$;

  4. 4.

$\langle\mathbb{W},I\rangle\models F\vee G$ if
$\langle\mathbb{W},I\rangle\models F$ or $\langle\mathbb{W},I\rangle\models
G$;

  5. 5.

$\langle\mathbb{W},I\rangle\models F\leftarrow G$ if
$\langle\mathbb{W},I\rangle\models F$ or
$\langle\mathbb{W},I\rangle\not\models G$

  6. 6.

$\langle\mathbb{W},I\rangle\models\exists x\,F(x)$ if
$\langle\mathbb{W},I\rangle\models F(t)$ for some ground term $t$;

  7. 7.

$\langle\mathbb{W},I\rangle\models\forall x\,F(x)$ if
$\langle\mathbb{W},I\rangle\models F(t)$ for all ground terms $t$;

  8. 8.

$\langle\mathbb{W},I\rangle\models\operatorname{\mathbf{K}}F$ if
$\langle\mathbb{W},I^{\prime}\rangle\models F$ for all
$I^{\prime}\in\mathbb{W}$;

  9. 9.

$\langle\mathbb{W},I\rangle\models\operatorname{\mathbf{M}}F$ if
$\langle\mathbb{W},I^{\prime}\rangle\models F$ for some
$I^{\prime}\in\mathbb{W}$;

  10. 10.

$\langle\mathbb{W},I\rangle\models\text{-}F$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F$;

  11. 11.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\bot$;

  12. 12.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;a$ if $\text{-}a\in I$, for any atom
$a\in\text{\em At}$:

  13. 13.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F\wedge G$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F$ or
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;G$;

  14. 14.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F\vee G$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F$ and
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;G$;

  15. 15.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F\leftarrow G$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F$ and
$\langle\mathbb{W},I\rangle\models G$

  16. 16.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\exists x\,F(x)$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F(t)$ for all ground terms $t$;

  17. 17.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\forall x\,F(x)$ if
$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;F(t)$ for some ground term $t$;

  18. 18.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\operatorname{\mathbf{K}}F$ if
$\langle\mathbb{W},I^{\prime}\rangle=\\!\\!\\!|\;F$ for all
$I^{\prime}\in\mathbb{W}$;

  19. 19.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\operatorname{\mathbf{M}}F$ if
$\langle\mathbb{W},I^{\prime}\rangle=\\!\\!\\!|\;F$ for some
$I^{\prime}\in\mathbb{W}$; and

  20. 20.

$\langle\mathbb{W},I\rangle=\\!\\!\\!|\;\text{-}F$ if
$\langle\mathbb{W},I\rangle\models F$.

A belief interpretation $\langle\mathbb{W},I\rangle$ that satisfies a formula
is called a  _belief model_. An epistemic interpretation $\mathbb{W}$
_satisfies_ a formula $F$, in symbols $\mathbb{W}\models F$ if
$\langle\mathbb{W},I\rangle\models F$ for all $I\in\mathbb{W}$. In this case,
$\mathbb{W}$ is also called an _epistemic model_ of $F$. Belief and epistemic
models defined in this way correspond to models in modal logics KD45 and S5,
respectively. As mentioned above, these modal logics are extended here with
strong negation (called here explicit negation).

Formulas not containing modal operators are called _objective_. Formulas in
which all atoms are in the scope of modal operators are called _subjective_. A
theory is called _objective_ or _subjective_ if all its formulas are objective
or subjective, respectively. For an objective formula $F$, the component
$\mathbb{W}$ is irrelevant. Therefore, we abbreviate
$\langle\mathbb{W},I\rangle\models F$ as $I\models F$.

###  3.3 Nonmonotonic semantics

We provide now a non-monotonic semantics for epistemic theories. This
semantics is a conservative extension of Answer Set Prolog. As mentioned
earlier, the initial work focused on a restricted language syntax that did not
allow arbitrary formulas as described in Section 3. truszczynski11b allowed
arbitrary propositional formulas, but did not include first-order constructs,
such as quantifiers. However, their ideas apply directly to the language
presented above by considering a definition of _stable models_ that covers
arbitrary objective formulas. For that definition we rely on quantified
equilibrium logic [Pearce and Valverde (2006)] with explicit negation [Aguado
et al. (2019)].

Given an objective theory $\Gamma$, by $\text{\rm SM}[\Gamma]$, we denote the
set of interpretations that are _answer sets_ (or _stable models_) of $\Gamma$
(see A for a formal definition). With this notation, we can immediately
provide an answer set based semantics to arbitrary epistemic theories.

######  Definition 1 (G94-reduct)

The _G94-reduct_ of a theory $\Gamma$ with respect to an epistemic
interpretation $\mathbb{W}$, written $\Gamma^{\mathbb{W}}$, is obtained by
replacing each maximal subformula $F$ of the forms
$\operatorname{\mathbf{K}}G$ and $\operatorname{\mathbf{M}}G$ by $\top$, if
$\mathbb{W}\models F$; or by $\bot$, otherwise.

######  Definition 2 (G94-world view)

An epistemic interpretation $\mathbb{W}$ is called a _G94-world view_ of a
theory $\Gamma$ if ${\mathbb{W}=\text{\rm SM}[\Gamma^{\mathbb{W}}]}$.

######  Definition 3 ($\mathcal{S}$-Belief set)

Given a semantics $\mathcal{S}$, an interpretation $I$ is called an
_$\mathcal{S}$ -belief set_ of a theory $\Gamma$ if there is an
$\mathcal{S}$-world view $\mathbb{W}$ of $\Gamma$ with $I\in\mathbb{W}$.

Definition 3 is stated in a general way, so it can be applied to different
semantics provided that they give a definition of $\mathcal{S}$-world views.
In particular, we get the definition of G94-belief sets by replacing
$\mathcal{S}$ by G94. This kind of parametrized definition is useful to
accommodate different semantics that we review in the following sections.

###  3.4 Epistemic Logic Programs

From a Knowledge Representation point of view, it is interesting to focus on a
particular class of theories that have the form of logic programs with modal
operators. Formally, an _objective literal_ $\ell$ is either an explicit
literal, that is $\ell\in\text{\em At}\cup\\{\text{-}a\mid a\in\text{\em
At}\\}$, a truth constant222For a simpler description of program
transformations, we allow truth constants where $\top$ denotes true and $\bot$
denotes false., that is $\ell\in\\{\top,\bot\\}$, or an explicit literal
preceded by one or two occurrences of default negation, that is
$l=\operatorname{\text{not}}\ell$ or
$l=\operatorname{\text{not}}\operatorname{\text{not}}\ell$. A _subjective
literal_ is an expression of the forms $\operatorname{\mathbf{K}}l$,
$\operatorname{\mathbf{M}}l$,
$\operatorname{\text{not}}\operatorname{\mathbf{K}}l$,
$\operatorname{\text{not}}\operatorname{\mathbf{M}}l$,
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\mathbf{K}}l$
or
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\mathbf{M}}l$
for any objective literal $l$. A _literal_ is either an objective or a
subjective literal. A _rule_ $r$ is an expression of the form:

$\displaystyle
l_{1}\operatorname{\,\text{or}\,}\dots\operatorname{\,\text{or}\,}l_{m}\leftarrow
L_{1},\dots,L_{n}$ (7)

with $m\geq 0$ and $n\geq 0$, where each $l_{i}$ is an objective literal and
each $L_{j}$ a literal. The left hand disjunction of (7) is called the rule
_head_ and it is abbreviated as $\mathit{Head}(r)$. The right hand side of (7)
is called the rule _body_ and it is abbreviated as $\mathit{Body}(r)$. An
_(epistemic) logic program_ $\Pi$ is a set of rules of the form (7).

We identify each rule of the form of (7) with the universal closure of the
formula

$\displaystyle l_{1}\vee\dots\vee l_{m}\leftarrow L_{1}\wedge\dots\wedge
L_{n}$ (8)

When $m=0$, we assume the head of the rule to be $\bot$. We also identify each
logic program with a theory containing a formula as above for each rule in the
program. Accordingly, we immediately obtain a definition for the G94-world
views of an epistemic logic program using Definition 2.

##  4 Epistemic specifications for Knowledge Representation

In this section, we review some of the potential applications of epistemic
specifications for knowledge representation. Namely, we revisit the use of
epistemic specifications to express integrity constraints over disjunctive
databases informally discussed in Section 2. Then, we illustrate how epistemic
specifications are also useful when we need to reason about all the answer
sets of an objective program at the same time, which is usually not possible
using Answer Set Prolog itself. Alongside these two applications, we also
review two formal properties (called _subjective constraint monotonicity_ and
_epistemic splitting_) that shed some light on the reasons why epistemic
specifications are useful for these two classes of problems. These properties
are also used in the forthcoming sections to compare different semantics. We
then show how we can extend the guess-define-and-test methodology of Answer
Set Programming to problems that lie on the second level of the polynomial
hierarchy: in particular we illustrate this methodology showing how epistemic
logic programs can be used to find conformant plans. This methodology is also
based on the aforementioned two properties: subjective constraint monotonicity
and epistemic splitting. Finally, we also sketch a potential application in
cybersecurity.

###  4.1 Integrity Constraints

As mentioned in the introduction, one of the initial motivations for epistemic
specifications was to express various forms of constraints about the knowledge
of disjunctive databases. We show here how the above semantics allow us to
represent constraints without free-variables, called here _integrity
constraints_. Let us now formalize some of the intuitions mentioned there.

###### Definition 4

An _epistemic specification_ is a pair $E=\langle\Gamma,\mathcal{C}\rangle$
where $\Gamma$ is an epistemic theory and $\mathcal{C}$ is a subjective theory
whose sentences are called _integrity constraints_. An _$\mathcal{S}$ -world
view_ of $E$ is an $\mathcal{S}$-world view $\mathbb{W}$ of $\Gamma$ such that
$\mathbb{W}\models\mathcal{C}$.

If we consider now a program containing the knowledge base (2), we can see
that such program has a unique world view containing two belief sets:

$\displaystyle A\cup\\{\mathit{teach(bob,ai)}\\}\hskip
56.9055ptA\cup\\{\mathit{teach(mary,ai)}\\}$

with
$A=\\{\mathit{h(bob)},\mathit{h(mary)},\mathit{teach(bob,java)},\mathit{teach(staff,python)}\\}$
being common to both belief sets. It is easy to see that formula
${h(\mathit{bob})\wedge teach(\mathit{bob},\mathit{java})}$ is satisfied by
both belief sets. This implies that the unique world view of this program
satisfies the formula ${\operatorname{\mathbf{K}}(h(\mathit{bob})\wedge
teach(\mathit{bob},\mathit{java}))}$ and, as a result, also ${\exists
X\operatorname{\mathbf{K}}(h(X)\wedge teach(X,\mathit{java}))}$. On the other
hand, neither ${\mathit{teach(bob,ai)}}$ nor ${\mathit{teach(mary,ai)}}$ are
satisfied by both belief sets and as a result, sentence ${\exists
X\operatorname{\mathbf{K}}(h(X)\wedge teach(X,\mathit{ai}))}$ is not satisfied
by the unique world view. This implies that the program does not satisfy the
universal closure of constraint (3), that is, the sentence:

$\displaystyle\forall C\,\exists
X\operatorname{\mathbf{K}}(h(X)\wedge\mathit{teach}(X,C))$ (9)

Similarly, we can see that the universal closure of constraint (4) is not
satisfied either, but the universal closure of (5) is. Note that in each
belief set there is someone teaching each of the subjects, even if that person
may vary between belief sets (in the case of $\mathit{ai}$) or may be unknown
(in the case of $\mathit{python}$).

An interesting property of some semantics is that integrity constraints can be
fully integrated into a single theory, while other semantics do not allow for
this. This property was called  _subjective constraint monotonicity_ by
cafafa19b.

######  Property 1 (Subjective constraint monotonicity)

A semantics $\mathcal{S}$ is said to satisfy _subjective constraint
monotonicity_ if, for any epistemic specification
$E=\langle\Gamma,\mathcal{C}\rangle$, an epistemic interpretation $\mathbb{W}$
is a $\mathcal{S}$-world view of $E$ iff $\mathbb{W}$ is a $\mathcal{S}$-world
view of
$\Gamma\cup\\{\bot\leftarrow\operatorname{\text{not}}\varphi\mid\varphi\in\mathcal{C}\\}$.

This property is analogous to the monotonicity of constraints in Answer Set
Prolog. Recall that an interpretation is an answer set of a program iff it
satisfies all its constraints and is an answer set of the rest of the program.
Similarly, subjective constraint monotonicity allows us to work simply with a
single theory (resp. logic program), instead of giving a special treatment to
constraints. It also ensures that certain intuitions from Answer Set Prolog
are carried to epistemic logic programs.

Note that Property 1 is enunciated in a semantics-dependent way (depends on
the semantics $\mathcal{S}$ selecting some $\mathcal{S}$-world views), so it
can be applied to alternative semantics. With respect to the semantics
corresponding to Definition 2, cafafa19b show that Property 1 is satisfied for
ground theories. It is not difficult to see that this property is also
satisfied for non-ground ones. We discuss it in the context of other semantics
below. As we point out, some semantics satisfy this property and others do not
(see Table 2 in page 2 for a quick overview).

###  4.2 Reasoning about incomplete knowledge

Beyond expressing integrity constraints about the knowledge implied by a
database, an interesting feature of epistemic specifications is their ability
to deduce new information about the knowledge in the database. To illustrate
this claim, consider the following example introduced by gelfond94.

###### Example 1

A given college uses the following set of rules to decide whether a student
$X$ is eligible for a scholarship:

$\displaystyle\mathit{eligible}(X)$ $\displaystyle\leftarrow$
$\displaystyle\mathit{high}(X)$ (10) $\displaystyle\mathit{eligible}(X)$
$\displaystyle\leftarrow$
$\displaystyle\mathit{minority}(X),\,\mathit{fair}(X)$ (11)
$\displaystyle\text{-}\mathit{eligible}(X)$ $\displaystyle\leftarrow$
$\displaystyle\text{-}\mathit{fair}(X),\,\text{-}\mathit{high}(X)$ (12)

Here, $\mathit{high}(X)$ and $\mathit{fair}(X)$ refer to the grades of student
$X$. We want to encode the additional college criterion “ _The students whose
eligibility is not determined by the college rules should be interviewed by
the scholarship committee_ ” as another rule in the program.

The interesting issue is that deciding whether $\mathit{eligible}(X)$ “ _can
be determined_ ” requires reasoning about all the stable models of the program
at the same time. For instance, if the only available information for some
student $mike$ is the disjunction

$\displaystyle\mathit{fair}(\mathit{mike})\operatorname{\,\text{or}\,}\mathit{high}(\mathit{mike})$
(13)

we get that program
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4}\,\\}$ has a unique
world view containing the following two belief sets:

$\displaystyle\\{\,\mathit{high}(\mathit{mike}),\mathit{eligible}(\mathit{mike})\,\\}$
(14) $\displaystyle\\{\,\mathit{fair}(\mathit{mike})\,\\}$ (15)

so $\mathit{eligible}(\mathit{mike})$ cannot be determined and an interview
should follow. If we are interested only in querying
$\operatorname{\mathbf{K}}\mathit{eligible}(\mathit{mike})$ or
$\operatorname{\mathbf{M}}\mathit{eligible}(\mathit{mike})$, we can do it
inside standard logic programming. For instance, the addition of constraint:

$\displaystyle\bot\leftarrow\mathit{eligible}(\mathit{mike})$

allows us to decide if $\mathit{eligible}(\mathit{mike})$ is a consequence of
all answer set of the original program by just checking that the resulting
program has no stable model. In such case, we can also conclude that
$\operatorname{\mathbf{K}}\mathit{eligible}(\mathit{mike})$ is a consequence
of the program. The difficulty comes when we try to _derive_ new information
from that knowledge. Rule

$\displaystyle\mathit{interview}(X)\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\mathit{eligible}(X),\,\operatorname{\text{not}}\operatorname{\mathbf{K}}\text{-}\mathit{eligible}(X)$
(16)

precisely allows us to derive that $\mathit{interview}(X)$ needs to hold for
every student $X$ for whom neither $\mathit{eligible}(X)$ nor
$\text{-}eligible(X)$ are satisfied in all belief sets of
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4}\,\\}$. If we now
consider the program
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\,\eqref{ex:college.5}\,\\}$,
we can see that this program has a unique world view containing the following
two belief sets:

$\displaystyle\\{\,\mathit{fair}(\mathit{mike}),\mathit{interview}(\mathit{mike})\,\\}$
(17)
$\displaystyle\\{\,\mathit{high}(\mathit{mike}),\mathit{eligible}(\mathit{mike}),\mathit{interview}(\mathit{mike})\,\\}$
(18)

The intuition behind the reasoning process followed in this example relies on
a kind of reasoning by layers. First, we compute the world views of the first
layer $\\{\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4}\\}$; then, the
second layer inspects the world views of the first layer through subjective
formulas and derives new information. We can also extend this example with a
third layer that uses the knowledge about $\mathit{interview}$ to derive
further information, for instance, by including the rule:

$\displaystyle\mathit{appointment}(X)\leftarrow\operatorname{\mathbf{K}}\mathit{interview}(X)$
(19)

The two belief sets of program
$\\{\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\eqref{ex:college.5}\\}$
contain $\mathit{interview}(\mathit{mike})$ and, as a result, we may expect
that $\mathit{appointment}(\mathit{mike})$ should be added to both belief sets
of program
$\\{\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\eqref{ex:college.5},\eqref{ex:college.6}\\}$.
Indeed, the unique world view of this program contains the two belief sets
resulting from adding $\mathit{appointment}(\mathit{mike})$ to (17) and (18).

This kind of reasoning was formalized in the form of a _splitting property_ by
cafafa19b 2019b; 2021. This property resembles the _splitting theorem_ for
Answer Set Prolog Lifschitz and Turner (1994). It is worth noting that this
splitting property was stated only for ground programs. However, it directly
extends to non-ground programs without quantifiers, by understanding each of
them as the ground program obtained by replacing all variables by all possible
object constants. It is still an open issue to generalize this property to
arbitrary theories containing quantifiers.

We introduce this property now, but we need the following notation first.
Given a ground rule $r$ of the form (7), by $\mathit{Atoms}(r)$ we denote the
set of all atoms occurring in $r$. By $\mathit{Body}_{obj}(r)$ we denote the
set of all atoms occurring in objective literals in the body of $r$. By abuse
of notation we also use $\mathit{Head}(r)$ to denote the set of all atoms
occurring in the head of $r$.

######  Definition 5 (Epistemic splitting set)

A set of ground atoms $U\subseteq\text{\em At}$ is said to be an _epistemic
splitting set_ of a ground program $\Pi$ if for any rule $r$ in $\Pi$ one of
the following conditions hold:

  1. 1.

$\mathit{Atoms}(r)\subseteq U$,

  2. 2.

$(\mathit{Body}_{obj}(r)\cup\mathit{Head}(r))\cap U=\emptyset$.

We define a _splitting_ of $\Pi$ as a pair $\langle
B_{U}(\Pi),T_{U}(\Pi)\rangle$ satisfying $B_{U}(\Pi)\cap T_{U}(\Pi)=\emptyset$
and $B_{U}(\Pi)\cup T_{U}(\Pi)=\Pi$, and also that all rules in $B_{U}(\Pi)$
satisfy (i) and all rules in $T_{U}(\Pi)$ satisfy (ii).

We also need to introduce a variation of the subjective reduct in Definition 1
that is restricted to a particular set of atoms.

###### Definition 6

The _subjective reduct_ of a ground program $\Pi$ with respect to an epistemic
interpretations $\mathbb{W}$ and a signature $U\subseteq\text{\em At}$,
written $\Pi^{\mathbb{W}}_{U}$, is obtained by replacing each subjective
literal $L$ with $\mathit{Atoms}(L)\subseteq U$ by $\top$ if
$\mathbb{W}\models L$ or by $\bot$ otherwise.

It is easy to see that, when $U=\text{\em At}$, Definition 6 coincides with
Definition 1. Given an epistemic splitting set $U$ for a program $\Pi$ and an
epistemic interpretation $\mathbb{W}$, we define
$E_{U}(\Pi,\mathbb{W})\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptscriptstyle\mathrm{def}$\cr\kern
1.0pt\cr$=$\cr\kern-0.1pt\cr}}}T_{U}(\Pi)^{\mathbb{W}}_{U}$, that is, we make
the subjective reduct of the top with respect to $\mathbb{W}$ and signature
$U$.

###### Definition 7

A pair $\langle\mathbb{W}_{b},\mathbb{W}_{t}\rangle$ is said to be an
$\mathcal{S}$-_solution_ of a ground program $\Pi$ with respect to an
epistemic splitting set $U$ if $\mathbb{W}_{b}$ is an $\mathcal{S}$-world view
of $B_{U}(\Pi)$ and $\mathbb{W}_{t}$ is an $\mathcal{S}$-world view of
$E_{U}(\Pi,\mathbb{W}_{b})$.

The following operation allows reconstructing the world view of the whole
program from the world views of its parts:

$\mathbb{W}_{b}\sqcup\mathbb{W}_{t}\ \ =\ \ \\{\ I_{b}\cup I_{t}\ |\
I_{b}\in\mathbb{W}_{b}\text{ and }I_{t}\in\mathbb{W}_{t}\ \\}$

######  Property 2 (Epistemic splitting)

A semantics $\mathcal{S}$ satisfies _epistemic splitting_ if for any epistemic
splitting set $U$ of any ground program $\Pi$, epistemic interpretation
$\mathbb{W}$ is an $\mathcal{S}$-world view of $\Pi$ iff there is an
$\mathcal{S}$-solution $\langle\mathbb{W}_{b},\mathbb{W}_{t}\rangle$ of $\Pi$
with respect to $U$ such that $\mathbb{W}=\mathbb{W}_{b}\sqcup\mathbb{W}_{t}$.

As with subjective constraint monotonicity, this property is also stated in a
semantics-dependent way, so we can study its applicability to other semantics
reviewed later. In particular, the semantics described above does satisfy this
property (Cabalar et al., 2019b, Main Theorem). Interestingly, every semantics
satisfying epistemic splitting also satisfies subjective constraint
monotonicity (Property 1; for a proof of this result see the paper by [Theorem
3]cafafa19b). A different notion of splitting in the context of this semantics
was first studied by Watson (2000).

Getting back to our running example, we can see that the set $U$, consisting
of atoms $\mathit{high}(\mathit{mike}),\mathit{fair}(\mathit{mike}),$
$\mathit{eligible}(\mathit{mike}),\mathit{minority}(\mathit{mike})$, is an
epistemic splitting set that divides the program
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\eqref{ex:college.5}\,\\}$
into a bottom $\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4}\,\\}$
and top part $\\{\,\eqref{ex:college.5}\,\\}$. The bottom part is an objective
program, without epistemic operators, which has a unique world view
$\mathbb{W}_{b}=[\eqref{f:sm1.pre},\eqref{f:sm2.pre}]$. The corresponding
simplification of the top contains (after grounding) the single rule

$\displaystyle\mathit{interview}(\mathit{mike})\leftarrow\operatorname{\text{not}}\bot,\operatorname{\text{not}}\bot$
(20)

Again, this program is objective and its unique world view is
$\mathbb{W}_{t}=[\\{interview(mike)\\}]$. Now it is easy to see how epistemic
splitting guarantees that program
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\eqref{ex:college.5}\,\\}$
has a unique world view
$\mathbb{W}_{b}\sqcup\mathbb{W}_{t}=[\eqref{f:sm1},\eqref{f:sm2}]$. We can
recursively apply this reasoning to program
$\\{\,\eqref{ex:college.1}\text{\,-\,}\eqref{ex:college.4},\eqref{ex:college.5},\eqref{ex:college.6}\,\\}$
to see that its unique world view is the result of adding
$\mathit{appointment}(\mathit{mike})$ to each belief set in
$[\,\eqref{f:sm1},\eqref{f:sm2}\,]$.

This shows that we can apply the semantics defined above to problems that
require to reason about all/some of the answer sets of a program, when this
can be done by layers. In particular, this is interesting for queering
databases that may contain disjunctive information as illustrated by Example
1.

###  4.3 A guess-define-and-test methodology for conformant planning

The problem of conformant planning consists of finding a sequence of (possibly
concurrent) actions that guarantee the achievement of some goal Smith and Weld
(1998). Different to classical planning, the action domain may be
nondeterministic, and the initial state may not be completely specified. A
conformant plan is valid if it is guaranteed to be executable and its
execution achieves the goal in all possible initial states and all possible
effects of the actions. It is well-known that the problem of finding
conformant plans of polynomially-bounded length is $\Sigma^{P}_{2}$-complete
Turner (2002). Quantified Boolean Formulas (QBFs) are one choice for encoding
problems in this complexity class. Indeed, there are QBF encodings for
conformant planning, but the logic programming encoding of the problem is much
closer to its natural language description and, thus, it is more declarative.
This makes the design, understanding and maintenance of the problem solution
substantially easier. It is also well-known that Answer Set Prolog can be used
to represent problems on the second level of the polynomial hierarchy Eiter
and Gottlob (1995). This may suggest that Answer Set Prolog may be a prime
candidate to represent conformant planning problems. However, tackling
problems on the second level of the polynomial hierarchy in Answer Set Prolog
usually comes at the cost of using highly sophisticated encodings based on
_saturation_ that break the intuitive understanding of normal programs. On the
other hand, normal (or head-cycle-free) epistemic programs can also represent
problems in the second level of the polynomial hierarchy Truszczynski (2011),
thus constituting an alternative to represent this class of problems. In
particular, semantics satisfying the epistemic splitting property (Property 2)
provide a natural guess-define-and-test methodology Marek and Truszczyński
(1999); Niemelä (1999) to represent these problems Cabalar et al. (2021). In
this methodology, each solution $\pi$ to the problem at hand corresponds to a
set $S_{\pi}$ of epistemic literals of the form $\operatorname{\mathbf{K}}a$.
The program is divided into three parts $\Pi_{\mathit{guess}}$,
$\Pi_{\mathit{define}}$ and $\Pi_{\mathit{test}}$ as follows:

  * •

The guess part $\Pi_{\mathit{guess}}$ generates world views where each of them
corresponds to a potential solution of the problem. Since solutions are
encoded using subjective literals of the form $\operatorname{\mathbf{K}}a$, we
may assume that each world view $\mathbb{W}$ of $\Pi_{\mathit{guess}}$ is a
singleton satisfying

$\displaystyle\operatorname{\mathbf{K}}a\vee\operatorname{\mathbf{K}}\operatorname{\text{not}}a$

This means that a solution does not only need to exist, but that a solution
needs to be known. For instance, in the case of conformant planning, this
means that the agent needs to know the sequence of actions that it will be
performing.

  * •

The test part $\Pi_{\mathit{test}}$ is a set of subjective constraints
imposing the conditions to be a solution. For instance, in the case of
conformant planning, this may consist of subjective constraints ensuring that
the goal is achieved and that the plan is executable.

  * •

The define part $\Pi_{\mathit{define}}$ is a program, in most cases an
objective one, defining auxiliary concepts. For instance, in the case of
conformant planning, this encodes the action domain and the initial state.

Let us now illustrate this methodology in more detail. The use of epistemic
logic programs to obtain conformant plans was first advocated by Kahl et al.
(2015). The semantics used there satisfies neither the epistemic splitting nor
the subjective constraint monotonicity properties. Then, Cabalar et al. (2021)
showed that the use of these two properties can greatly simplify the
representation. We follow here this latter approach. Consider the following
variation of the well-known Yale shooting problem Hanks and McDermott (1987)
introduced by Kahl et al. (2015).

###### Example 2

The agent is operating in a domain in which there is a turkey and a gun. The
turkey can be alive or not. The gun may be loaded or not. If the gun is loaded
and the trigger is pulled, then the turkey will be dead. Pulling the trigger
will unload the gun. The agent can load the gun, but this action is impossible
if the gun is already loaded. The goal is to kill the turkey.

The main difference between this example and the original one introduced by
hanmcd87a is that we do not know the actual initial state. The action domain
of this example can be represented by objective rules of the form

$\displaystyle\text{-}\mathit{alive}_{i+1}$
$\displaystyle\leftarrow\mathit{trigger}_{i},\,\mathit{loaded}_{i}$ (21)
$\displaystyle\text{-}\mathit{loaded}_{i+1}$
$\displaystyle\leftarrow\mathit{trigger}_{i}$ (22)
$\displaystyle\mathit{loaded}_{i+1}$
$\displaystyle\leftarrow\mathit{load}_{i}$ (23)
$\displaystyle\mathit{impossible}$
$\displaystyle\leftarrow\mathit{load}_{i},\,\mathit{loaded}_{i}$ (24)

for all ${1\leq i\leq n}$, where $n$ is a given planning horizon. Rules
(21)-(23) describe the effects of the actions, while rule (24) captures the
fact that _load_ cannot occur if the gun is already loaded. This is an
objective program whose representation of the action domain is similar to the
one usually used for classical planning in Answer Set Prolog (see for example
the paper by lifschitz02a).

The initial situation can be represented by the following two disjunctions:

$\displaystyle\mathit{alive}_{0}\operatorname{\,\text{or}\,}\text{-}\mathit{alive}_{0}\hskip
56.9055pt\mathit{loaded}_{0}\operatorname{\,\text{or}\,}\text{-}\mathit{loaded}_{0}$
(25)

The define part $\Pi_{\mathit{define}}$ for the conformant planning problem
consists of rules (21)-(25). Since this is an objective program, we can use it
together with any existing solver for Answer Set Prolog to see how the world
evolves if some sequence of actions is executed. For instance, it is easy to
check that program
$\\{\mathit{trigger}_{0},\mathit{load}_{1},\mathit{trigger}_{2}\\}\cup\Pi_{\mathit{define}}$
has four stable models, that all four contain the literal
$\text{-}\mathit{alive}_{3}$, and that none of them contain
$\mathit{impossible}$. As a result, we can deduce that
$\pi=\langle\mathit{trigger}_{0},\mathit{load}_{1},\mathit{trigger}_{2}\rangle$
is a conformant plan, since the goal is achieved in all cases and the sequence
of actions is executable. Using an epistemic logic program, we can encode this
final step in the test part. In this example, program $\Pi_{\mathit{test}}$
consists of the following two subjective constraints

$\displaystyle\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\text{-}\mathit{alive}_{n}$
(26) $\displaystyle\leftarrow\operatorname{\mathbf{M}}\mathit{impossible}$
(27)

In particular, (26) states that, in the last situation, the agent must know
that the turkey is not alive; while (27) ensures that no impossible action has
occurred. Note that, since $\Pi_{\mathit{define}}$ is an objective program, it
has a unique world view consisting of all its stable models. Furthermore,
since all those stable models contain $\text{-}\mathit{alive}_{3}$, it follows
that this unique world view satisfies
$\operatorname{\mathbf{K}}\text{-}\mathit{alive}_{3}$. Since none of them
contain $\mathit{impossible}$, we get that it does not satisfy
$\operatorname{\mathbf{M}}\mathit{impossible}$. Hence, this world view
satisfies both (26) and (27). As a result, this is the unique world view of
the program
$\\{\mathit{trigger}_{0},\mathit{load}_{1},\mathit{trigger}_{2}\\}\cup\Pi_{\mathit{define}}\cup\Pi_{\mathit{test}}$.
This is a direct consequence of subjective constraint monotonicity (Property
1).

Let us now illustrate that this method also allows to show that
$\pi^{\prime}=\langle\mathit{load},\mathit{trigger}\rangle$ is not a
conformant plan for this scenario. In this case, program
$\\{\mathit{load}_{1},\mathit{trigger}_{2}\\}\cup\Pi_{\mathit{define}}$ also
has four stable models and all four contain $\text{-}\mathit{alive}_{3}$.
However, two of them also contain $\mathit{impossible}$. As a result, the
unique world view of this program does not satisfy constraint (27), which
implies that program
$\\{\mathit{load}_{1},\mathit{trigger}_{2}\\}\cup\Pi_{\mathit{define}}\cup\Pi_{\mathit{test}}$
has no word view at all. This shows that $\pi^{\prime}$ is not a conformant
plan because it is not executable in all possible initial situations. In
particular, we cannot $\mathit{load}$ the gun when it is initially
$\mathit{loaded}$.

Epistemic logic programs can not only be used to check that a sequence of
action is a conformant plan, but it can also be used to generate all possible
conformant plans. As usual in Answer Set Prolog, this is achieved by including
a choice of the form

$\displaystyle
a_{i}\operatorname{\,\text{or}\,}\operatorname{\text{not}}a_{i}$ (28)

for all actions at each time step $1\leq i<n$. As mentioned above, for
conformant planning, this is not enough because it allows that different
actions can be performed for different initial situations. This is avoided by
introducing a rule of the form

$\displaystyle a_{i}\leftarrow\operatorname{\mathbf{M}}a_{i}$ (29)

stating that, if an action $a_{i}$ occurs in any belief set, it must occur in
all of them. In this sense, $\Pi_{\mathit{guess}}$ consists of rules of the
form (28) and (29) for each action and time step. For instance, in our running
example, $\Pi_{\mathit{guess}}$ consists of the following rules

$\displaystyle\begin{aligned}
\mathit{trigger}_{i}&\operatorname{\,\text{or}\,}\operatorname{\text{not}}\mathit{trigger}_{i}\\\
\mathit{load}_{i}&\operatorname{\,\text{or}\,}\operatorname{\text{not}}\mathit{load}_{i}\end{aligned}\hskip
56.9055pt\begin{aligned}
\mathit{trigger}_{i}&\leftarrow\operatorname{\mathbf{M}}\mathit{trigger}_{i}\\\
\mathit{load}_{i}&\leftarrow\operatorname{\mathbf{M}}\mathit{load}_{i}\end{aligned}$
(30)

for $0\leq i<3$. It can be checked that program
$\Pi_{\mathit{guess}}\cup\Pi_{\mathit{define}}\cup\Pi_{\mathit{test}}$ has a
unique world view and that this world view satisfies the subjective literals
$\operatorname{\mathbf{K}}\mathit{trigger}_{0}$,
$\operatorname{\mathbf{K}}\mathit{load}_{1}$ and
$\operatorname{\mathbf{K}}\mathit{trigger}_{2}$. That is, the unique world
view of this program corresponds to the unique conformant plan for this
scenario.

Though we have illustrated the application of the generate-define-and-test
methodology for the conformant planning problem, we believe that this
methodology can be applied to other problems that fit in the second level of
the polynomial hierarchy. As another example we could consider conformant
diagnosis, where we are tasked to find a diagnosis that explains the
observations in all possible initial situations. As with classical planning
problems, Answer Set Prolog is well suited to represent diagnostic problems,
but not conformant diagnosis ones. This methodology, not only allow us to
represent a conformant diagnosis problem, but also to reuse the existing
domain representation used in Answer Set Prolog to represent its non-
conformant variation.

###  4.4 Reasoning over attack trees and graphs

The term _attack trees_ was coined by Bruce Schneier 1999, but the concept has
most likely existed prior to that. The trees represent chains of attacks that
can lead to a goal, the root vertex. Sets of vertices in the tree serve as
preconditions (conjunctive or disjunctive) to other vertices, thus forming
trees. The idea is to identify conditions that allow for achieving the goal.
This notion can be generalized to _attack graphs_ , which model collections of
attacks and exploits. Usually these graphs are directed acyclic graphs.

In Figure 1, a simplification of a scenario described by Albanese et al.
(2012) is represented as an attack graph, which in this case forms a tree. The
elliptical vertices represent exploits, the other vertices represent
conditions or achievements. When exploits have several conditions as
predecessors, all of them have to be met to achieve the exploit. Exploits
themselves cause new conditions to hold. In turn, for a condition to hold,
only one preceding exploit needs to be achieved. Achieving an exploit by
leveraging conditions would form an attack. Attacks can lead to conditions
that allow for achieving other exploits, this is usually referred to as chains
of attacks.

In Figure 1 one exploit is ftp_rhosts(0,2), where an issue in the ftp service
is exploited to overwrite the .rhosts file of machine 2. The prerequisite is
having a user on machine 0 and ftp access from machine 0 to 2. The exploit
causes trust(2,0), which in turn allows for accessing machine 2 from machine 0
via rsh (exploit rsh(0,2)), thus getting user access on machine 2. On the
right hand side of the graph having user access to machine 1 and the ability
to reach the ssh daemon on machine 2 from machine 1 allows the exploit
sshd_bof(1,2), a buffer overflow exploit in the ssh daemon, which also allows
for having user access to machine 2. Having user access to machine 2 allows
for the exploit local_bof(2), which exploits a local buffer overflow issue to
gain root access.

ftp(0,2)user(0)ftp_rhosts(0,2)trust(2,0)rsh(0,2)sshd(1,2)user(1)sshd_bof(1,2)user(2)local_bof(2)root(2)
Figure 1: Example attack graph

It is clear that graphs of this kind can be modeled by objective rules, in
particular, one can create a rule

$\displaystyle e\leftarrow c_{1},\ldots,c_{n}$ (31)

for each exploit $e$ and conditions $c_{1},\ldots,c_{n}$ that point to it. For
conditions caused by an exploit, we create rules

$\displaystyle c\leftarrow e$ (32)

for each condition $c$ caused by exploit $e$. If some exploits are already
known to hold or not to hold, they can be affirmed as facts. For the example
in Figure 1, this would lead to the following rules:

$\displaystyle\begin{aligned}
\mathit{ftp\\_rhosts}(0,2)&\leftarrow\mathit{ftp}(0,2),\mathit{user}(0)\\\
\mathit{trust}(2,0)&\leftarrow\mathit{ftp\\_rhosts}(0,2)\\\
\mathit{rsh}(0,2)&\leftarrow\mathit{trust}(2,0)\\\
\mathit{sshd\\_bof}(1,2)&\leftarrow\mathit{sshd}(1,2),\mathit{user}(1)\\\
\mathit{user}(2)&\leftarrow\mathit{rsh}(0,2)\\\
\mathit{user}(2)&\leftarrow\mathit{sshd\\_bof}(1,2)\\\
\mathit{local\\_bof}(2)&\leftarrow\mathit{user}(2)\\\
\mathit{root}(2)&\leftarrow\mathit{local\\_bof}(2)\end{aligned}$

One advantage of Epistemic Logic Programs over the graph representation is the
ability to abstract from specific machines and thus arrive at more compact
representations. For example, the following rule represents that having ftp
access from a machine X to another machine Y and having a user on X gives rise
to the ftp_rhosts exploit from X to Y:

$\displaystyle\begin{aligned}
\mathit{ftp\\_rhosts}(X,Y)&\leftarrow\mathit{ftp}(X,Y),\mathit{user}(X)\end{aligned}$

In order to use the attack graph to establish that the exploit
$\mathit{root}(2)$ can not be reached under any circumstances, one can add a
choice of the form

$\displaystyle c\operatorname{\,\text{or}\,}\text{-}c$ (33)

for each condition $c$ with no incoming arc, and the constraint

$\displaystyle\leftarrow\operatorname{\mathbf{M}}e$ (34)

for each exploit $e$ to be checked.

In the example, this gives rise to

$\displaystyle\begin{aligned}
\mathit{ftp}(0,2)\operatorname{\,\text{or}\,}\text{-}\mathit{ftp}(0,2)\\\
\mathit{user}(0)\operatorname{\,\text{or}\,}\text{-}\mathit{user}(0)\\\
\mathit{sshd}(1,2)\operatorname{\,\text{or}\,}\text{-}\mathit{sshd}(1,2)\\\
\mathit{user}(1)\operatorname{\,\text{or}\,}\text{-}\mathit{user}(1)\\\
\leftarrow\operatorname{\mathbf{M}}\mathit{root}(2)\end{aligned}$

This modeling allows for flexibility in further reasoning. As an example, we
consider the application of hardening measures, as they are called by Albanese
et al. (2012), in order to close vulnerabilities. In the running example,
hardening measures could be to close ftp and/or ssh access to the network. One
could add “epistemic guesses” for each of hardening measures and rules that
describe their consequences as follows:

$\displaystyle\begin{aligned}
\mathit{close\\_ftp}&\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\text{-}\mathit{close\\_ftp}\\\
\text{-}\mathit{close\\_ftp}&\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\mathit{close\\_ftp}\\\
\mathit{close\\_sshd}&\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\text{-}\mathit{close\\_sshd}\\\
\text{-}\mathit{close\\_sshd}&\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\mathit{close\\_sshd}\\\
\text{-}\mathit{ftp(0,2)}&\leftarrow\mathit{close\\_ftp}\\\
\text{-}\mathit{sshd(1,2)}&\leftarrow\mathit{close\\_sshd}\end{aligned}$

Each subset of available hardening measures thus gives rise to a potential
world view, but only those that guarantee that the exploit is impossible to
achieve will be world views, due to (34). Note that this guarantee is provided
by the subjective constraint monotonicity property (Property 1). This property
is satisfied by the semantics we discuss in Section 3.3 and some other
semantics we will see in the next section. However, there are also semantics
that do satisfy this property and for which this claim may not hold.

In the example, there is one potential world view in which
$\text{-}\mathit{close\\_ftp}$ and $\text{-}\mathit{close\\_sshd}$ hold, but
clearly it contains several answer sets (containing both $\mathit{ftp}(0,2)$
and $\mathit{user}(0)$ or both $\mathit{sshd}(1,2)$ and $\mathit{user}(1)$)
that contain $\mathit{root}(2)$ and therefore violate the constraint.
Similarly, the world view in which $\mathit{close\\_ftp}$ and
$\text{-}\mathit{close\\_sshd}$ hold, will contain an answer set that contains
$\mathit{sshd}(1,2)$ and $\mathit{user}(1)$ and therefore also
$\mathit{root}(2)$, while the world view in which
$\text{-}\mathit{close\\_ftp}$ and $\mathit{close\\_sshd}$ hold, will contain
an answer set that contains $\mathit{ftp}(0,2)$ and $\mathit{user}(0)$ and
therefore also $\mathit{root}(2)$. Only the world view in which
$\mathit{close\\_ftp}$ and $\mathit{close\\_sshd}$ hold can guarantee that
$\mathit{root}(2)$ is false in each of its answer sets. Indeed, in this
example the only hardening that avoids the exploit $\mathit{root}(2)$ is to
close both ftp and ssh access.

##  5 The search for self-support-free world views

As mentioned in Section 2, early formalizations of epistemic specifications
contained unsupported beliefs. In this section, we review the major approaches
that have addressed this issue. In Subsection 5.5, we also review a new
property called _foundedness_ that aims to capture the essence of self-
supported-free world views in a formal way. We use this property, together
with the subjective constraint monotonicity and epistemic splitting properties
defined earlier, to provide a formal comparison between different approaches.
We also go deeper in this comparison by providing some translations between
approaches and identifying some agreement subclasses.

With the exception of the work by Shen and Eiter (2016), all the existing work
addressing this issue focused on ground theories. Thus, in the rest of this
section, we restrict ourselves to ground theories. Another interesting point
to mention are the languages used by different approaches. As mentioned
earlier, the original language of epistemic specifications contained two
modalities $\operatorname{\mathbf{K}}$ and $\operatorname{\mathbf{M}}$.

primitive |  | defined operators |
---|---|---|---
| $\operatorname{\mathbf{K}}F$ | $\operatorname{\mathbf{M}}F$ | $\operatorname{\mathbf{not}}F$
$\operatorname{\mathbf{K}}$ | - | $\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}F$ | $\operatorname{\text{not}}\operatorname{\mathbf{K}}F$
$\operatorname{\mathbf{M}}$ | $\operatorname{\text{not}}\operatorname{\mathbf{M}}\operatorname{\text{not}}F$ | - | $\operatorname{\mathbf{M}}\operatorname{\text{not}}F$
$\operatorname{\mathbf{not}}$ | $\operatorname{\text{not}}\operatorname{\mathbf{not}}F$ | $\operatorname{\mathbf{not}}\operatorname{\text{not}}F$ | -
Table 1: Interdefinability of epistemic operators. If the rewriting produces a
formula of the form
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\text{not}}\varphi$,
it is replaced by $\operatorname{\text{not}}\varphi$. For instance, rewriting
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\mathbf{M}}\varphi$
produces
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}\varphi$
and, thus, we get
$\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}\varphi$.

Interestingly, according to the semantics given so far, these two modalities
are interdefinable as shown it Table 1. This interdefinability holds for all
approaches we review below with two exceptions: Fariñas del Cerro et al.
(2015) presented a semantics where the above equivalences do not hold, and
Cabalar et al. (2019a) leaves the discussion about the modal operator
$\operatorname{\mathbf{M}}$ for future work.

Shen and Eiter (2017) introduced a third modal operator
$\operatorname{\mathbf{not}}$ where $\operatorname{\mathbf{not}}F$ can be read
as “there is no evidence proving that $F$ is true.” Interestingly, this third
modal operator is also interdefinable with the other two. In view of these
facts, in the following we focus on reviewing the different semantics for the
$\operatorname{\mathbf{K}}$ operator and assume that, unless stated otherwise,
$\operatorname{\mathbf{M}}$ and $\operatorname{\mathbf{not}}$ are treated as
abbreviations following Table 1.

###  5.1 Gelfond 2011

Gelfond (2011) was the first to discuss the existence of unintended world
views in the early works on epistemic specifications and to propose an
alternative semantics. As mentioned in the introduction, an example of these
unintended world views is the existence of the unsupported belief $p$ in one
of the world views of the program consisting of rule

$\displaystyle p\leftarrow\operatorname{\mathbf{K}}p.$ (6)

We can check that, according to Definition 2, this program has two world
views: $[\\{\,\\}]$ and $[\\{p\\}]$. For the former, note that
$[\\{\,\\}]\not\models\operatorname{\mathbf{K}}p$. Then, the G94-reduct of
$p\leftarrow\operatorname{\mathbf{K}}p$ with respect to $[\\{\,\\}]$ is the
tautological rule

$\displaystyle p\leftarrow\bot.$ (35)

It is easy to see that this objective program is equivalent to the empty
program and, thus, it has the empty set as its unique stable model. As a
result, we obtain that $[\\{\,\\}]$ is indeed a world view of program
$\\{p\leftarrow\operatorname{\mathbf{K}}p\\}$. On the other hand, we can see
that $[\\{p\\}]\models\operatorname{\mathbf{K}}p$. As a result, the G94-reduct
of $p\leftarrow\operatorname{\mathbf{K}}p$ with respect to $[\\{p\\}]$ is

$\displaystyle p\leftarrow\top.$ (36)

The unique stable model of this objective program is $\\{p\\}$ and, therefore,
$[\\{p\\}]$ is also a G94-world view of
$\\{p\leftarrow\operatorname{\mathbf{K}}p\\}$.

Motivated by this issue, Gelfond (2011) proposed the following variation of
the reduct. The definition of G11-world views is exactly as the definition of
G94-world views, but it uses this new reduct instead of the G94-reduct.

######  Definition 8 (G11-reduct and world views)

Given a logic program $\Pi$, its G11-reduct with respect to a non-empty set of
interpretations $\mathbb{W}$ is the program obtained by:

  1. 1.

replacing by $\bot$ every subjective literal $L$ such that
$\mathbb{W}\not\models L$;

  2. 2.

removing all other occurrences of subjective literals in the scope of default
negation;

  3. 3.

replacing all other occurrences of subjective literals of the form
$\operatorname{\mathbf{K}}l$ by $l$.

An epistemic interpretation $\mathbb{W}$ is a G11-world view of $\Pi$ iff
$\mathbb{W}$ is the set of all stable models of the G11-reduct of $\Pi$ with
respect to $\mathbb{W}$.

Definition 8 was an attempt to find a formalization of the Rationality
Principle. The main technical tool used for this purpose was this new reduct.
Unlike other existing ASP reducts which normally remove a program’s rule or
some extended literal from the rule’s body, the new reduct allowed replacement
of an epistemic literal $\operatorname{\mathbf{K}}l$ by its corresponding
objective literal $l$. The intention was to ensure that the rule allows the
inclusion of the head in a particular belief set only if it already contains
the objective literals corresponding to all the epistemic literals in its
body. It worked for rules like $p\leftarrow\operatorname{\mathbf{K}}p$ and
other simple examples, but failed to completely eliminate unintended beliefs
(see an example below).

Continuing with our running example, we can see now that the G11-reduct of
$p\leftarrow\operatorname{\mathbf{K}}p$ with respect to the epistemic
interpretation $[\\{\,\\}]$ is the same as its G94-reduct. Therefore,
$[\\{\,\\}]$ is also a G11-world view of
$\\{p\leftarrow\operatorname{\mathbf{K}}p\\}$. In contrast, the G11-reduct of
$p\leftarrow\operatorname{\mathbf{K}}p$ with respect to $[\\{p\\}]$ is the
tautology

$\displaystyle p\leftarrow p.$ (37)

The unique stable model of this program is the empty set and, thus,
$[\\{p\\}]$ is not a G11-world view of
$\\{p\leftarrow\operatorname{\mathbf{K}}p\\}$.

It worth noting that, if all occurrences of epistemic literals are in the
scope of negation, this semantics coincide with the G94-semantics introduced
above. On the other hand, if no epistemic literal occurs in the scope of
negation, this semantics coincide with the K15-semantics introduced in the
next section.

Despite the success of this semantics in removing the unsupported belief $p$
in the simple example given above, it still presents unsupported beliefs in
more complex examples. Take for instance the following program used by Cabalar
et al. (2019a) to illustrate this fact:

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055ptp\leftarrow\operatorname{\mathbf{K}}q\hskip
56.9055ptq\leftarrow\operatorname{\mathbf{K}}p.$ (38)

We can see that this program has two G94-world views, $[\\{p\\},\\{q\\}]$ and
$[\\{p,q\\}]$. Here, the belief ${p\wedge q}$ in the second world view is
unsupported. Note that the first rule does not support ${p\wedge q}$ and the
other two rules only can support this fact if $p$ or $q$ were supported in all
belief sets, which is not the case. Still, this second G94-world view is also
a G11-world view. To see why, note that the G11-reduct of program
$\\{\eqref{theory:larger.set.of.worlds}\\}$ with respect to $[\\{p,q\\}]$ is
the objective program:

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip 56.9055ptp\leftarrow
q\hskip 56.9055ptq\leftarrow p$

which has the unique stable model $\\{p,q\\}$. In fact, we can see below that
this example (or a slight variations of it) provides a major challenge to most
existing approaches.

It is worth mentioning that this semantics satisfies subjective constraint
monotonicity (Property 1; see the paper by fandinno19a), although it does not
satisfy the epistemic splitting property (Property 2). To see that this
semantics does not satisfy epistemic splitting, take the following program
from the paper by Cabalar et al. (2021):

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055pts\leftarrow\operatorname{\mathbf{K}}p\hskip
56.9055pt\leftarrow\operatorname{\text{not}}s$ (39)

This program has no G94-world view. Note that $U=\\{p,q\\}$ is a splitting set
for this program that divides it in a bottom part
$\\{p\operatorname{\,\text{or}\,}q\\}$ and a top part
$\\{s\leftarrow\operatorname{\mathbf{K}}p,\,\leftarrow\operatorname{\text{not}}s\\}$.
It is easy to see that the unique world view of the bottom part is
$[\\{p\\},\,\\{q\\}]$ and, simplifying the top part with respect to this world
view, we obtain the unsatisfiable program

$\displaystyle c\leftarrow\bot\hskip
56.9055pt\leftarrow\operatorname{\text{not}}c$

Since the G94-semantics satisfies the epistemic splitting property, this
immediately implies that this program has no G94-world view. Similarly, if the
G11-semantics would satisfy the epistemic splitting property, we would expect
that this program had no G11-world view either. However, this program does
have the G11-world view $[\\{p,s\\}]$. To see this fact, note that the
G11-reduct of the program containing the rules (39) with respect to
$[\\{p,s\\}]$ is

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip 56.9055pts\leftarrow
p\hskip 56.9055pt\leftarrow\operatorname{\text{not}}s.$

The unique stable model of this objective program is $\\{p,s\\}$. This program
also illustrates another example of unsupported beliefs: here neither of the
beliefs $p$ and $s$ are supported. This can be easily seen by removing the
constraint $\leftarrow\operatorname{\text{not}}s$. The resulting program

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055pts\leftarrow\operatorname{\mathbf{K}}p$ (40)

has a unique world view $[\\{p\\},\\{q\\}]$ in all semantics discussed in this
paper. Here, neither $p$ nor $s$ are believed, and adding the constraint
$\leftarrow\operatorname{\text{not}}s$ does not provide any reason to believe
either of them.

###  5.2 Kahl, Watson, Balai, Gelfond &Zhang 2015

Kahl et al. (2015) revised the semantics introduced by Gelfond (2011) in order
to avoid the presence of multiple world views due to recursion through the
operator $\operatorname{\mathbf{M}}$. As an example of this issue consider the
program consisting of rule

$\displaystyle p\leftarrow\operatorname{\mathbf{M}}p.$ (41)

With respect to the G94- and the G11-semantics, this program has two worlds
views, namely $[\\{\,\\}]$ and $[\\{p\\}]$. Kahl et al. (2015) argue that this
program should have a unique world view and that it should be $[\\{p\\}]$.
This argument is based on the following observation.

> It was observed by looking at the definitions for satisfiability that a
> rational agent should find it easier to accept certain extended literals
> over others. This is clear when we look at the fact that, e.g. given a
> belief interpretation333Kahl et al. (2015) use the term “pointed ES
> structure” instead of “belief interpretation.” We made the replacement here
> to keep the coherence with the rest of the text.
> $\langle\mathbb{W},I\rangle$, in order to establish
> $\operatorname{\mathbf{K}}l$, it must be demonstrated that $l$ belongs to
> all belief sets in $\mathbb{W}$. To establish $l$, it must be demonstrated
> that $l$ belongs to a particular belief set in $\mathbb{W}$, namely $I$. But
> to establish $\operatorname{\mathbf{M}}l$, it is sufficient to demonstrate
> that $l$ belongs to some belief set in $\mathbb{W}$.

As a result, a preference order among literals $\operatorname{\mathbf{K}}l$,
$l$ and $\operatorname{\mathbf{M}}l$ is established, where
$\operatorname{\mathbf{K}}l$ is the hardest to accept (or it is the one that
requires the highest degree of conviction) and $\operatorname{\mathbf{M}}l$ is
the easiest to accept. Taken into account this preference order, one can
deduce that the fact that accepting $l$ requires it to be self-support-free
does not imply that accepting $\operatorname{\mathbf{M}}l$ should require it
to be self-support-free, too. Unfortunately, this observation does not imply
the contrary either; and other authors, like Su et al. (2020), have opted to
require that $\operatorname{\mathbf{M}}l$ should be self-support-free.
According to Su et al. (2020), the unique world view of this program should be
$[\\{\,\\}]$. The intuition of recursion through the
$\operatorname{\mathbf{M}}$ operator is subject of open debate and one could
even develop a semantics with two different $\operatorname{\mathbf{M}}$-like
modal operators, where one of them requires to be self-support-free and the
other does not.

Focusing on the semantics introduced by Kahl et al. (2015), recall that
following our convention (see Table 1), rule (41) is an abbreviation for rule

$\displaystyle
p\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}p.$
(42)

Note that
$[\\{\,\\}]\models\operatorname{\mathbf{K}}\operatorname{\text{not}}p$.
Therefore, the G94-reduct of (42) with respect to $[\\{\,\\}]$ is

$\displaystyle p\leftarrow\operatorname{\text{not}}\top,$

while its G11-reduct is

$\displaystyle p\leftarrow\bot.$

It is easy to see that these two rules are equivalent and their unique stable
model is the empty set. As a result, $[\\{\,\\}]$ is both a G94- and a
G11-world view.

Motivated by this issue, Kahl et al. (2015) proposed a new variation of the
reduct. The definition of K15-world views is exactly as the definition of G94-
and G11-world views, but using this new reduct instead. We present here the
definition introduced by (Kahl et al., 2015, Appendix C).

######  Definition 9 (K15-reduct and world view)

The _K15-reduct_ of a ground program $\Pi$ with respect to an epistemic
interpretation $\mathbb{W}$ is obtained by replacing each maximal subformula
of the form $\operatorname{\mathbf{K}}l$ by $l$, if
$\mathbb{W}\models\operatorname{\mathbf{K}}l$, or by $\bot$, otherwise.444If
replacing $\operatorname{\mathbf{K}}l$ by $l$ results in more than two nested
default negations we simplify it using the following rewriting rule
recursively:
$\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\text{not}}F\mapsto\operatorname{\text{not}}F$.

An epistemic interpretation $\mathbb{W}$ is a K15-world view of $\Pi$ iff
$\mathbb{W}$ is the set of all stable models of the K15-reduct of $\Pi$ with
respect to $\mathbb{W}$.

Continuing with our running example, we can now see that the K15-reduct of
(42) with respect to $[\\{\,\\}]$ is

$\displaystyle
p\leftarrow\operatorname{\text{not}}\operatorname{\text{not}}p,$

and the resulting program has two stable models: $\\{\,\\}$ and $\\{p\\}$.
Therefore, $[\\{\,\\}]$ is not a K15-world view. In a similar way, we can
check that $[\\{p\\}]$ is indeed a K15-world view. Note that the K15-reduct
with respect to this epistemic interpretation is

$\displaystyle p\leftarrow\operatorname{\text{not}}\bot.$

It is worth mentioning that for programs, in which the epistemic operator does
not occur under the scope of default negation, this semantics coincides with
G11. As a result, the arguments stated in Section 5.1 for programs (38) and
(39) also apply to this semantics. This implies that this semantics also
manifests unsupported beliefs and that it does not satisfy epistemic
splitting. Besides, as observed by Leclerc and Kahl (2018a), this semantics
does not satisfy subjective constraint monotonicity (Property 1), while G11
does. The following program taken from the paper by Leclerc and Kahl (2018a)
illustrates this fact:

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055pt\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p.$ (43)

This program has a unique K15-world view $[\\{p\\}]$. Note however that the
program $\\{p\operatorname{\,\text{or}\,}q\\}$ is objective and has two stable
models $\\{p\\}$ and $\\{q\\}$. Thus, it has the unique world view
$[\\{p\\},\\{q\\}]$, which does not satisfy the subjective constraint
$\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p$. We can see
that adding this subjective constraint makes $[\\{p\\}]$ a world view, which
contradicts this property.

An interesting observation about this semantics is that it can be considered
as the _reflexive_ counterpart of G94 in a sense similar to the relation
between Moore’s autoepistemic logic and reflexive autoepistemic logic Schwarz
(1991). In fact, we can use the embedding from reflexive autoepistemic logic
into Moore’s autoepistemic logic (Marek and Truszczyński, 1993, page 304) to
illustrate this fact. This embedding $(\,\cdot\,)^{B}$ is defined recursively
as follows:

  1. 1.

$F^{B}=F$ if $F$ is an atom or $F=\bot$;

  2. 2.

$(\text{-}F)^{B}=\text{-}(F^{B})$

  3. 3.

$(F\otimes G)^{B}=F^{B}\otimes G^{B}$ for $\otimes\in\\{\wedge,\vee,\to\\}$;

  4. 4.

$(Qx\,F(x))^{B}=Qx\,F(x)^{B}$ for $Q\in\\{\forall,\exists\\}$; and

  5. 5.

$(\operatorname{\mathbf{K}}F)^{B}=F^{B}\wedge\operatorname{\mathbf{K}}F^{B}$.

For a theory $\Gamma$, the embedding is defined as $\Gamma^{B}=\\{F^{B}\mid
F\in\Gamma\\}$.

###### Proposition 1

The K15-word views of any program $\Pi$ coincide with the G94-world views of
$\Pi^{B}$.

It is enough to show that the K15-reduct of $\Gamma$ is equivalent to the
G94-reduct of $\Gamma^{B}$ for any epistemic interpretation $\mathbb{W}$. Pick
any maximal subformula of the form $\operatorname{\mathbf{K}}l$. We proceed by
cases.

  * •

If $\mathbb{W}\models\operatorname{\mathbf{K}}l$, then the K15-reduct replaces
it by $l$. On the other hand, the G94-reduct of
$(\operatorname{\mathbf{K}}l)^{B}=l^{B}\wedge\operatorname{\mathbf{K}}l^{B}=l\wedge\operatorname{\mathbf{K}}l$
is $l\wedge\top$. Clearly these two formulas are equivalent. Note also that
$l^{B}=l$ because $l$ is an objective literal.

  * •

Otherwise, the K15-reduct replaces $\operatorname{\mathbf{K}}l$ by $\bot$
while the G94-reduct of
$(\operatorname{\mathbf{K}}l)^{B}=l\wedge\operatorname{\mathbf{K}}l$ is
$l\wedge\bot$, which are also equivalent.

Proposition 1 gives us a straightforward way to extend the K15-semantics from
ground logic programs to arbitrary theories: we can define the K15-world views
of any theory $\Gamma$ as the G94-world views of $\Gamma^{B}$.

A converse embedding $(\,\cdot\,)^{K}$ from the G94- into the K15-semantics is
also possible. This embedding is defined recursively as follows:

  1. 1.

$F^{K}=F$ if $F$ is an atom or $F=\bot$;

  2. 2.

$(\text{-}F)^{K}=\text{-}(F^{K})$

  3. 3.

$(F\otimes G)^{K}=F^{K}\otimes G^{K}$ for $\otimes\in\\{\wedge,\vee,\to\\}$;

  4. 4.

$(Qx\,F(x))^{K}=Qx\,F(x)^{K}$ for $Q\in\\{\forall,\exists\\}$; and

  5. 5.

$(\operatorname{\mathbf{K}}F)^{K}=\operatorname{\mathbf{M}}\operatorname{\mathbf{K}}F^{K}$.

Note that $\cdot^{K}$ differs from $\cdot^{B}$ only in the last condition.

###### Proposition 2

The K15-word views of any theory $\Gamma$ coincide with the G94-world views of
$(\Gamma^{K})^{B}$.

It is enough to show that the G94-reduct of $\Gamma$ is equivalent to
G94-reduct of $(\Gamma^{K})^{B}$ for any epistemic interpretation
$\mathbb{W}$. Pick any maximal subformula of the form
$\operatorname{\mathbf{K}}F$. We proceed by cases.

  * •

If $\mathbb{W}\models\operatorname{\mathbf{K}}F$, then the G94-reduct replaces
it by $\top$. On the other hand, we have

$\displaystyle((\operatorname{\mathbf{K}}F)^{K})^{B}$
$\displaystyle=(\operatorname{\mathbf{M}}\operatorname{\mathbf{K}}F^{K})^{B}$
$\displaystyle=(\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}\operatorname{\mathbf{K}}F^{K})^{B}$
$\displaystyle=\operatorname{\text{not}}(\operatorname{\mathbf{K}}\operatorname{\text{not}}\operatorname{\mathbf{K}}F^{K})^{B}$
$\displaystyle=\operatorname{\text{not}}(\operatorname{\text{not}}\operatorname{\mathbf{K}}(F^{K})^{B}\wedge\operatorname{\mathbf{K}}\operatorname{\text{not}}\operatorname{\mathbf{K}}(F^{K})^{B})$
$\displaystyle\equiv\operatorname{\text{not}}\operatorname{\text{not}}\operatorname{\mathbf{K}}(F^{K})^{B}\vee\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}\operatorname{\mathbf{K}}(F^{K})^{B})$
$\displaystyle\equiv\operatorname{\mathbf{K}}(F^{K})^{B}\vee\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}\operatorname{\mathbf{K}}(F^{K})^{B})$

Furthermore, it can be checked by induction that
$\mathbb{W}\models\operatorname{\mathbf{K}}F$ iff
$\mathbb{W}\models\operatorname{\mathbf{K}}(F^{K})^{B}$. Hence, the G94 reduct
of $((\operatorname{\mathbf{K}}F)^{K})^{B}$ is
$\top\vee\operatorname{\text{not}}\bot\equiv\top$ and, thus, equivalent to the
G94-reduct of $\operatorname{\mathbf{K}}F$.

  * •

Otherwise, the G94-reduct replaces $\operatorname{\mathbf{K}}F$ by $\bot$
while the G94 reduct of $((\operatorname{\mathbf{K}}F)^{K})^{B}$ is
$\bot\vee\operatorname{\text{not}}\top\equiv\bot$ and, thus, equivalent to the
G94-reduct of $\operatorname{\mathbf{K}}F$.

###### Corollary 1

The G94-world views of any program $\Pi$ coincide with the K15-world views of
$\Pi^{K}$.

######  Proof 5.1.

From Proposition 1, the K15-world views of $\Pi^{K}$ coincide with the
G94-world views of $(\Pi^{K})^{B}$ which, from Proposition 2 coincide with
with the G94-world views of $\Pi$.

Propositions 1 and Corollary 1 provide a formal correspondence between the G94
and the K15 semantics. Furthermore, they also show that any tool to compute
the world views of one semantics can be used to compute the world views of the
other, with the minimum effort of applying this translation. Note however
that, in general, even if $\Pi$ is a program, neither $\Pi^{B}$ nor $\Pi^{K}$
are necessarily programs. For instance, $\eqref{eq:self-
supported.M.translated}^{B}$ is

$\displaystyle
p\leftarrow\operatorname{\text{not}}\,(\operatorname{\text{not}}p\wedge\operatorname{\mathbf{K}}\operatorname{\text{not}}p)$
(44)

which syntactically is not a valid rule. However, this formula can be
transformed into a set of rules that is equivalent modulo the original
signature (similar to the tseitin68a transformation from tseitin68a). In this
case, we may rewrite (44) as

$\displaystyle p$ $\displaystyle\leftarrow\operatorname{\text{not}}aux$ (45)
$\displaystyle aux$
$\displaystyle\leftarrow\,\operatorname{\text{not}}p\wedge\operatorname{\mathbf{K}}\operatorname{\text{not}}p$
(46)

The unique G94-world view of this program is $[\\{p\\}]$, which coincides with
the unique K15-world view of $\eqref{eq:self-supported.M.translated}$. This
translation was used (without proof) by the solver eclingo to compute the G94-
and K15-world views using the same tool Cabalar et al. (2020).

###  5.3 Shen & Eiter 2016

sheeit16 (sheeit16,sheeit17a) introduced the operator
$\operatorname{\mathbf{not}}$ with the intention to evaluate
$\operatorname{\mathbf{not}}l$ to true if $l$ is false in at least one belief
set of a world view, which intuitively corresponds to
$\operatorname{\text{not}}\operatorname{\mathbf{K}}l$ or
$\operatorname{\mathbf{M}}\operatorname{\text{not}}l$, as noted earlier. Their
key idea was to treat $\operatorname{\mathbf{not}}$ in a similar way as
$\operatorname{\text{not}}$ (default negation) and assume the truth of
$\operatorname{\mathbf{not}}l$ whenever possible. This notion was named
_knowledge minimization with epistemic negation_.

According to Shen and Eiter (2016), _candidate world views_ are defined as a
first step, followed by a minimization criterion (by maximizing negative
knowledge). The following equivalent definition, which relates S16 to
K15-world views, has been proposed by Kahl et al. (2016) and by Son et al.
(2017).

######  Definition 5.2 (S16-world views).

Let $\Pi$ be a logic program $\Pi$ and $E_{\Pi}$ be the set of epistemic
literals that contains $\operatorname{\text{not}}\operatorname{\mathbf{K}}l$
for every epistemic literal of the form $\operatorname{\mathbf{K}}l$ that
occurs in $\Pi$. Let
$\Phi_{\mathbb{W}}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptscriptstyle\mathrm{def}$\cr\kern
1.0pt\cr$=$\cr\kern-0.1pt\cr}}}\\{\ L\in E_{\Pi}\ |\ \mathbb{W}\models L\ \\}$
be the subset of $E_{\Pi}$ satisfied by an epistemic interpretation
$\mathbb{W}$. Then, epistemic interpretation $\mathbb{W}$ is a S16-world view
iff it is a K15-world view and there is no other K15-world view
$\mathbb{W}^{\prime}$ such that
$\Phi_{\mathbb{W}^{\prime}}\supset\Phi_{\mathbb{W}}$.

Given this definition, it is clear that the single K15-world view $[\\{p\\}]$
of the program $\eqref{eq:leckah18b}$ reported earlier is also the single
S16-world view. This shows that S16 does not satisfy the subjective constraint
monotonicity nor the epistemic splitting properties either.

The following example from the paper by Shen and Eiter (2016) illustrate
differences between semantics K15 and S16.

$\displaystyle
p\leftarrow\operatorname{\mathbf{M}}q,\operatorname{\text{not}}q.\hskip
28.45274ptq\leftarrow\operatorname{\mathbf{M}}p,\operatorname{\text{not}}p.$
(47)

Expanding $\operatorname{\mathbf{M}}$ according to Table 1 yields:

$\displaystyle
p\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}q,\operatorname{\text{not}}q.\hskip
28.45274ptq\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}p,\operatorname{\text{not}}p.$
(48)

There are two K15-world views, $\mathbb{W}_{1}=[\\{p\\},\\{q\\}]$ and
$\mathbb{W}_{2}=[\\{\,\\}]$. As
$\mathbb{W}_{1}\not\models\operatorname{\mathbf{K}}\operatorname{\text{not}}q$
and
$\mathbb{W}_{1}\not\models\operatorname{\mathbf{K}}\operatorname{\text{not}}p$,
the K15-reduct of $\eqref{eq:sheeit16-ex1.translated}$ with respect to
$\mathbb{W}_{1}$ is

$\displaystyle
p\leftarrow\operatorname{\text{not}}\bot,\operatorname{\text{not}}q.\hskip
28.45274ptq\leftarrow\operatorname{\text{not}}\bot,\operatorname{\text{not}}p.$
(49)

the stable models of which are $\\{p\\}$ and $\\{q\\}$, so $\mathbb{W}_{1}$ is
a K15-world view. Next observe that
$\mathbb{W}_{2}\models\operatorname{\mathbf{K}}\operatorname{\text{not}}q$ and
$\mathbb{W}_{2}\models\operatorname{\mathbf{K}}\operatorname{\text{not}}p$, so
the K15-reduct of $\eqref{eq:sheeit16-ex1.translated}$ with respect to
$\mathbb{W}_{2}$ is

$\displaystyle
p\leftarrow\operatorname{\text{not}}\operatorname{\text{not}}q,\operatorname{\text{not}}q.\hskip
28.45274ptq\leftarrow\operatorname{\text{not}}\operatorname{\text{not}}p,\operatorname{\text{not}}p.$
(50)

which has the single stable model $\\{\,\\}$, so $\mathbb{W}_{2}$ is also a
K15-world view.

Finally, observe that
$\Phi_{\mathbb{W}_{1}}=\\{\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}p,\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}q\\}$
and $\Phi_{\mathbb{W}_{2}}=\\{\,\\}$, so $\mathbb{W}_{1}$ is an S16-world
view, but $\mathbb{W}_{2}$ is not, because
$\Phi_{\mathbb{W}_{1}}\supset\Phi_{\mathbb{W}_{2}}$.

###  5.4 Fariñas del Cerro, Herzig & Iraz Su 2015

Fariñas del Cerro et al. (2015) tackle the issue of self-supported beliefs by
introducing a modal extension of equilibrium logic rather than a variation of
the reduct approaches. Defining a modal extension follows the common practice
in intuitionistic modal logics Fischer Servi (1977); Fariñas del Cerro and
Raggio (1983); Simpson (1994); Bierman and de Paiva (2000). In this case,
equilibrium logic is extended with modal logic S5. As usual, this modal
extension properly distinguishes between the modal operators
$\operatorname{\mathbf{K}}$ and $\operatorname{\mathbf{M}}$ that, to date, are
not known to be interdefinable. We mostly follow here the revised presentation
by Iraz Su et al. (2020). Note that the operator $\operatorname{\mathbf{M}}$
is written as $\hat{\operatorname{\mathbf{K}}}$ there.

Formally, an _F15-interpretation_ is a pair $\langle\mathbb{W},h\rangle$ where
$\mathbb{W}$ is an epistemic interpretation and $h:\mathbb{W}\longrightarrow
2^{\text{\em At}}$ is a function mapping each interpretation $T\in\mathbb{W}$
to some subset of atoms such that $h(T)\subseteq T$. Satisfaction of formulas
with respect to F15-interpretations is defined in a similar way as with
respect to belief interpretations. Satisfaction of a formula $F$ with respect
to an F15-interpretation $\langle\mathbb{W},h\rangle$ and a propositional
interpretation $I$ is recursively defined as follows:

  1. 1.

$\langle\mathbb{W},h\rangle,I\models a$ iff $a\in I$, for any atom
$a\in\text{\em At}$;

  2. 2.

$\langle\mathbb{W},h\rangle,I\models G_{1}\wedge G_{2}$ iff
$\langle\mathbb{W},h\rangle,I\models G_{1}$ and
$\langle\mathbb{W},h\rangle,I\models G_{2}$;

  3. 3.

$\langle\mathbb{W},h\rangle,I\models G_{1}\vee G_{2}$ iff
$\langle\mathbb{W},h\rangle,I\models G_{1}$ or
$\langle\mathbb{W},h\rangle,I\models G_{2}$;

  4. 4.

$\langle\mathbb{W},h\rangle,I\models G_{1}\to G_{2}$ iff
$\langle\mathbb{W},h^{\prime}\rangle,I\not\models G_{1}$ or
$\langle\mathbb{W},h^{\prime}\rangle,I\models G_{2}$ for both
$h^{\prime}\in\\{h,\mathit{id}\\}$;

  5. 5.

$\langle\mathbb{W},h\rangle,I\models\operatorname{\mathbf{K}}G$ iff
$\langle\mathbb{W},h,J\rangle\models G$ for all $J\in\mathbb{W}$; and

  6. 6.

$\langle\mathbb{W},h\rangle,I\models\operatorname{\mathbf{M}}G$ iff
$\langle\mathbb{W},h,J\rangle\models G$ for some $J\in\mathbb{W}$.

where $id:\mathbb{W}\longrightarrow 2^{\text{\em At}}$ is the identity
function, that is, $id(T)=T$ for every $T\in\mathbb{W}$. We say that an
F15-interpretation $\langle\mathbb{W},h\rangle$ _satisfies_ a formula $F$ when
$\langle\mathbb{W},h\rangle,I\models F$ for all $I\in\mathbb{W}$. In this case
$\langle\mathbb{W},h\rangle$ is also called an _F15-model_ of $F$. We say that
$\langle\mathbb{W},h\rangle$ is an _F15-model_ of a theory $\Gamma$, written
$\langle\mathbb{W},h\rangle\models\Gamma$, if it is an F15-model of all its
formulas $F\in\Gamma$.

Given an epistemic interpretation $\mathbb{W}$ and an F15-interpretation
${\mathcal{I}=\langle\mathbb{W}^{\prime},h\rangle}$, we write
${\mathcal{I}\preceq\mathbb{W}}$ if ${\mathbb{W}=\mathbb{W}^{\prime}}$ and
$h(I)\subseteq I$ for all $I\in\mathbb{W}$. We write
${\mathcal{I}\prec\mathbb{W}}$ if ${\mathcal{I}\preceq\mathbb{W}}$ and $h\neq
id$. Then, equilibrium models are defined as follows:

######  Definition 5.3 (F15-equilibrium model).

An epistemic interpretation $\mathbb{W}$ is called an _F15-equilibrium model_
of a theory $\Gamma$ if it is a model of $\Gamma$ and there is no F15-model
$\mathcal{I}$ of $\Gamma$ with ${\mathcal{I}\prec\mathbb{W}}$.

The F15-world views are obtained from a selection among equilibrium
F15-models. For defining that selection, we need to introduce the following
terminology. A function $h:\mathbb{W}\longrightarrow 2^{\text{\em At}}$ is
said to be _total on_ a set $\mathbb{X}\subseteq\mathbb{W}$ iff $h(I)=I$ for
every $I\in\mathbb{X}$.

######  Definition 5.4.

Given a theory $\Gamma$, an epistemic interpretation $\mathbb{W}$ and a subset
$\mathbb{X}\subseteq\mathbb{W}$ of it, we write
$\mathbb{W},\mathbb{X}\models^{*}\Gamma$ if the following two conditions are
satisfied:

  1. 1.

$\langle\mathbb{W},id\rangle,I\models\Gamma$ for all $I\in\mathbb{X}$, and

  2. 2.

every ${h\neq id}$ that is total on ${\mathbb{W}\setminus\mathbb{X}}$ satifies
$\langle\mathbb{W},h\rangle,I\not\models\Gamma$ for some ${I\in\mathbb{X}}$.

For any epistemic interpretations $\mathbb{W}$ and $\mathbb{W}^{\prime}$ we
write $\mathbb{W}\leq_{\Gamma}\mathbb{W}^{\prime}$ if

$\displaystyle\mathbb{W}\cup\\{I\\},\mathbb{W}\models^{*}\Gamma\quad\text{implies}\quad\mathbb{W}^{\prime}\cup\\{I\\},\mathbb{W}^{\prime}\models^{*}\Gamma$

for every $I$ that belongs to some F15-equilibrium model of $\Gamma$. As usual
$\mathbb{W}<_{\Gamma}\mathbb{W}^{\prime}$ stands for
$\mathbb{W}\leq_{\Gamma}\mathbb{W}^{\prime}$ and
$\mathbb{W}^{\prime}\not\leq_{\Gamma}\mathbb{W}$.

###### Observation 1

If $I\in\mathbb{W}$, then $\mathbb{W}\cup\\{I\\},\mathbb{W}\models^{*}\Gamma$
iff $\mathbb{W},\mathbb{W}\models^{*}\Gamma$ iff $\mathbb{W}$ is a
F15-equilibrium of $\Gamma$.

######  Definition 5.5 (F15-world view).

An epistemic interpretation $\mathbb{W}$ is called an _F15-world view_ of a
theory $\Gamma$ if it is an F15-equilibrium model of $\Gamma$ and there is no
other F15-equilibrium model $\mathbb{W}^{\prime}$ such that
$\mathbb{W}\subset\mathbb{W}^{\prime}$ or
$\mathbb{W}<_{\Gamma}\mathbb{W}^{\prime}$.

The following observation eases finding the F15-word views of many interesting
programs.

###### Observation 2

If some theory $\Gamma$ has a unique F15-equilibrium model $\mathbb{W}$, then
this is also its unique F15-world view.

Let us now show that a program consisting of rule

$\displaystyle p\leftarrow\operatorname{\mathbf{K}}p$ (6)

has $[\\{\,\\}]$ as its unique F15-world view, as expected. First, it is easy
to see that $[\\{\,\\}]$ is an epistemic model of (6) and there is no
$\mathcal{I}\prec[\\{\,\\}]$. Hence, this is an F15-equilibrium model. On the
other hand, if we consider $\mathcal{I}=\langle[\\{p\\}],h\rangle$ with
$h(\\{p\\})=\emptyset$, then we can see that $\mathcal{I}\prec[\\{p\\}]$ and
that $\mathcal{I}$ is an F15-model of (6). Therefore, $[\\{p\\}]$ is not an
F15-equilibrium model. In fact, we can check that $[\\{\,\\}]$ is the unique
F15-equilibrium model of $\\{\eqref{es:self-supported}\\}$ and, from
Observation 2, its unique F15-world view.

As mentioned earlier, a distinct characteristic of this semantics is that
$\operatorname{\mathbf{M}}F$ cannot be understood as an abbreviation for
$\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}F$.
In particular, the program consisting of the single rule

$\displaystyle p\leftarrow\operatorname{\mathbf{M}}p$ (41)

has the unique world view $[\\{\,\\}]$; while the program consisting of the
single rule

$\displaystyle
p\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}\operatorname{\text{not}}p$
(42)

has the unique world view $[\\{p\\}]$. The latter coincides with the semantics
K15 and S16 presented above, but the former differs. Beyond the difference on
this particular example, this illustrates a major difference between the F15
semantics and the semantics K15 and S16: while the F15 semantics tries to
reject self-supported beliefs through the operator
$\operatorname{\mathbf{M}}$, both K15 and S16 force them. Note that the G94
and the G11 semantics take an intermediate position with both programs having
the same two world views: $[\\{p\\}]$ and $[\\{\,\\}]$.

Let us now show why $[\\{\,\\}]$ is the unique F15-world view of (41). For
this, note that interpretation $\mathcal{I}=\langle[\\{p\\}],h\rangle$ with
$h(\\{p\\})=\emptyset$ is an F15-model of (41) and that it satisfies
$\mathcal{I}\prec[\\{p\\}]$. Hence, $[\\{p\\}]$ is neither an F15-equilibrium
model nor an F15-world view of this program. On the other hand, $[\\{\,\\}]$
is trivially an F15-equilibrium model and, since there are no other
F15-equilibrium models, it is the unique F15-world view.

Despite the fact that this semantics rejects more self-supported believes than
previous semantics, it still manifests some self-supported believes as can be
illustrated using the following program.

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055ptp\leftarrow\operatorname{\mathbf{K}}q\hskip
56.9055ptq\leftarrow\operatorname{\mathbf{K}}p\hskip
56.9055pt\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p$ (51)

This program is the result of adding the constraint
$\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p$ to the program
(38). This constraint is important to ensure that the program has a unique
F15-equilibrium logic and, therefore, we can make use of Observation 2. Note
that $[\\{p\\},\\{q\\}]$ does not satisfy this constraint and, therefore,
cannot be an F15-equilibrium model. In fact, it is easy to check that
$[\\{p,q\\}$ is the unique epistemic model of (51) and, thus, the only
candidate to be an F15-equilibrium model. To show that this is indeed an
F15-equilibrium model, we need to check that there is no F15-model
$\mathcal{I}=\langle[\\{p,q\\}],h\rangle$ with
$\mathcal{I}\prec[\\{p\\},\\{q\\}]$. Note that such an interpretation must
satisfy $h(\\{p,q\\})=\emptyset$, or $h(\\{p,q\\})=\\{p\\}$ or or
$h(\\{p,q\\})=\\{q\\}$. In the first case the interpretation does not satisfy
the first disjunction; in the other two cases, it fails to satisfy one of the
other two rules. Hence, $[\\{p\\},\\{q\\}]$ is the unique F15-equilibrium
model and the unique F15-world view of this program.

It is also worth mentioning that the F15-semantics satisfies neither
subjective constraint monotonicity (Property 1) nor epistemic splitting
(Property 2). To illustrate this fact, consider the program consisting of the
following two rules

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055pt\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p,$ (43)

which has a unique F15-equilibrium model and a unique F15-world view
$[\\{p\\}]$. However, the program $\\{p\operatorname{\,\text{or}\,}q\\}$ is
objective and has two stable models $\\{a\\}$ and $\\{b\\}$. Thus, it has the
unique world view $[\\{p\\},\\{q\\}]$. Therefore adding the subjective
constraint $\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}a$
produces a new world view, which violates the subjective constraint
monotonicity property.

###  5.5 Foundedness property

So far, we have seen that the search for self-supported-free beliefs was
driven by a series of examples used to evaluate the different semantics for
epistemic specifications. Cabalar et al. (2019a) presented a property called
_foundedness_ that aims to capture the essence of this search in a general
way. This property is based on the notion of unfounded sets introduced by
Leone et al. (1997) for Answer Set Prolog. Intuitively, an unfounded set is a
collection of atoms that is not derivable from a given program and a fixed set
of assumptions.

In order to formalize the foundedness property, we need the following
notation. Given a ground rule $r$, the set $\mathit{Body}^{+}_{obj}(r)$
collects all explicit literals occurring in its positive body while
$\mathit{Body}^{+}_{sub}(r)$ collects all explicit literals occurring in
positive subjective literals.

######  Definition 5.6 (Unfounded set).

Let $\Pi$ be a ground program and $\mathbb{W}$ an epistemic interpretation. An
_unfounded set_ $\mathbb{S}$ with respect to $\Pi$ and $\mathbb{W}$ is a non-
empty set of pairs where, for each $\langle X,I\rangle\in\mathbb{S}$, both $X$
and $I$ are sets of explict literals and there is no rule $r\in\Pi$ with
$\mathit{Head}(r)\cap X\neq\emptyset$ satisfying all of the following:

  1. 1.

$\langle\mathbb{W},I\rangle\models\mathit{Body}(r)$

  2. 2.

$\mathit{Body}^{+}_{obj}(r)\cap X=\emptyset$

  3. 3.

$(\mathit{Head}(r)\setminus X)\cap I=\emptyset$

  4. 4.

$\forall\langle X^{\prime},I^{\prime}\rangle\in\mathbb{S}:$
$\mathit{Body}^{+}_{sub}(r)\cap X^{\prime}=\emptyset$

The definition is similar to unfounded sets for objective programs (Leone et
al., 1997, Definition 3.1). In fact, the latter corresponds to the first three
conditions above, except that $\langle\mathbb{W},I\rangle$ is used to check
satisfaction of $\mathit{Body}(r)$, as it may contain now subjective literals.
Intuitively, each $I$ represents some potential belief set and $X$ is some set
of atoms without a “justifying” rule. In other words, there is no $r\in\Pi$
allowing a founded derivation of atoms in $X$. A rule like that should have a
true $\mathit{Body}(r)$ (condition 1) but not because of positive literals in
$X$ (condition 2) and is not used to derive other head atoms outside $X$
(condition 3). The novelty for the epistemic case is the addition of condition
4: to consider $r$ a justifying rule, it is additionally required to not use
any positive literal $\operatorname{\mathbf{K}}a$ in the body such that atom
$a$ also belongs to any of the unfounded components $X^{\prime}$ in
$\mathbb{S}$.

######  Definition 5.7 (Founded world view).

Let $\Pi$ be a ground program and $\mathbb{W}$ be an epistemic interpretation.
We say that $\mathbb{W}$ is _unfounded_ if there is some unfounded set
$\mathbb{S}$ such that every $\langle X,I\rangle\in\mathbb{S}$ satisfies
$I\in\mathbb{W}$ and $X\cap I\neq\emptyset$. We say that $\mathbb{W}$ is
_founded_ otherwise.

If we consider now the program in the introduction consisting of rule

$\displaystyle p\leftarrow\operatorname{\mathbf{K}}p$ (6)

we can observe that $\mathbb{S}=[\langle\\{p\\},\\{p\\}\rangle]$ makes
$[\emptyset,\\{p\\}]$ unfounded because (6) does not fulfill condition 4: we
cannot derive atom $a$ from a rule that contains
$a\in\mathit{Body}^{+}_{sub}(r)$. On the other hand, the other G94-world view,
$[\emptyset]$, is trivially founded.

######  Property 3 (Foundedness)

A semantics $\mathcal{S}$ satisfies _foundedness_ when all the
$\mathcal{S}$-world views of any ground program $\Pi$ are founded.

As illustrated by the above example, it is easy to see that the G94-semantics
does not satisfy foundedness. Note also that, as we have illustrated above,
all the approaches presented so far present some self-supported beliefs. Those
self-supported beliefs are unfounded sets and, thus, we also can see that none
of the approaches discussed so far satisfy this property. Recall that the
following program was used to illustrate the existence of self-supported
beliefs in Sections 5.1 and 5.2:

$\displaystyle a\operatorname{\,\text{or}\,}b\hskip
56.9055pta\leftarrow\operatorname{\mathbf{K}}b\hskip
56.9055ptb\leftarrow\operatorname{\mathbf{K}}a$ (38)

This program has two world views, namely $[\\{a\\},\\{b\\}]$ and
$[\\{a,b\\}]$, according to the G94, G11 and and K15 semantics. World view
$[\\{a\\},\\{b\\}]$ is founded because the first rule justifies both belief
sets. Note that $[\langle\\{a\\},\\{a\\}\rangle]$ and
$[\langle\\{b\\},\\{b\\}\rangle]$ are not unfounded sets. However, for the
world view $[\\{a,b\\}]$, we have the unfounded set
$\mathbb{S}^{\prime}=[\langle\\{a\\},\\{a,b\\}\rangle,\,\langle\\{b\\},\\{a,b\\}\rangle]$
which violates condition 3 for the first rule and condition 4 for the other
two rules. That is, the world view $[\\{a,b\\}]$ is unfounded and, therefore,
we can conclude that none of the G94, G11, and K15 semantics satisfy the
foundedness property.

For the F15 and S16 semantics, we use the program (51) consisting of the rules
of (38) plus the constraint
$\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}a$. Note that
adding subjective constraints to a program do not affect the existence of
unfounded sets. Thus, this example also shows that the F15 and S16 semantics
do not satisfy this property either.

###  5.6 Cabalar, Fandinno & Fariñas del Cerro 2019

Motivated by the fact that all previous approaches did not satisfy the
foundedness property introduced above, Cabalar et al. (2019a) presented a new
semantics with this property in mind. Another goal in designing this semantics
was that it should precisely correspond to the G94-semantics when self-
supported beliefs are not a problem. This is the case for the class of
programs that do not have positive dependencies through subjective literals.
Those programs are called _epistemically tight_. It is worth mentioning that
the same ideas allow to obtain founded versions of the semantics mentioned
above as we also illustrate below.

Technically, this semantics is an extension of Pearce’s equilibrium logic with
Moore’s autoepistemic logic. As a result, its monotonic basis is based on a
combination of the intermediate logic HT and the modal logic KD45. In this
sense, its monotonic basis is similar to the one presented in Section 5.4, but
using modal logic KD45 instead of modal logic S5 used there.

A _C19-epistemic interpretation_ ${\bm{\mathsf{W}}=\\{\langle
H_{1},T_{1}\rangle,\dots,\langle H_{n},T_{n}\rangle\\}}$ is a non-empty set of
pairs of propositional interpretations. To each C19-epistemic interpretation,
we associate a corresponding epistemic interpretation
${\bm{\mathsf{W}}^{t}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptscriptstyle\mathrm{def}$\cr\kern
1.0pt\cr$=$\cr\kern-0.1pt\cr}}}\\{T_{1},\dots,T_{n}\\}}$. A _C19-belief
interpretation_ $\mathcal{I}$ is a pair
$\mathcal{I}=\langle\bm{\mathsf{W}},\langle H,T\rangle\rangle$, or simply
$\mathcal{I}=\langle\bm{\mathsf{W}},H,T\rangle$, where $\bm{\mathsf{W}}$ is a
C19-epistemic interpretation and $\langle H,T\rangle$ stands for the real
world, possibly not in $\bm{\mathsf{W}}$. A C19-belief interpretation
$\mathcal{I}=\langle\bm{\mathsf{W}},H,T\rangle$ satisfies a formula $\varphi$,
written $\mathcal{I}\models\varphi$, iff

  * •

$\mathcal{I}\models a$ iff $a\in H$, for any atom $a\in\text{\em At}$,

  * •

$\mathcal{I}\models\psi_{1}\wedge\psi_{2}$ iff $\mathcal{I}\models\psi_{1}$
and $\mathcal{I}\models\psi_{2}$,

  * •

$\mathcal{I}\models\psi_{1}\vee\psi_{2}$ iff $\mathcal{I}\models\psi_{1}$ or
$\mathcal{I}\models\psi_{2}$,

  * •

$\mathcal{I}\models\psi_{1}\to\psi_{2}$ iff both: (i)
$\mathcal{I}\not\models\psi_{1}$ or $\mathcal{I}\models\psi_{2}$; and (ii)
$\langle\bm{\mathsf{W}}^{t},T\rangle\not\models\psi_{1}$ or
$\langle\bm{\mathsf{W}}^{t},T\rangle\models\psi_{2}$,

  * •

$\mathcal{I}\models\operatorname{\mathbf{K}}\psi$ iff
$\langle\bm{\mathsf{W}},H_{i},T_{i}\rangle\models\psi$ for all $\langle
H_{i},T_{i}\rangle\in\bm{\mathsf{W}}$.

An interpretation $\langle\bm{\mathsf{W}},H,T\rangle$ is a _C19-belief model_
of a theory $\Gamma$ iff
$\langle\bm{\mathsf{W}},H_{i},T_{i}\rangle\models\varphi$ for all $\langle
H_{i},T_{i}\rangle\in\bm{\mathsf{W}}\cup\\{\langle H,T\rangle\\}$ and all
$\varphi\in\Gamma$ – additionally, when $\langle
H,T\rangle\in\bm{\mathsf{W}}$, we further say that $\bm{\mathsf{W}}$ is a
_C19-epistemic model_ of $\Gamma$, abbreviated as
$\bm{\mathsf{W}}\models\Gamma$.

###### Observation 3

If $\bm{\mathsf{W}}$ is a C19-epistemic model of some theory $\Gamma$, then
$\bm{\mathsf{W}}^{t}$ is an epistemic model of $\Gamma$.

######  Definition 5.8.

Given an epistemic interpretation $\mathbb{W}$ and a C19-epistemic
interpretation $\bm{\mathsf{W}}$, we write $\bm{\mathsf{W}}\prec\mathbb{W}$ if
the following two conditions hold:

  1. 1.

$\bm{\mathsf{W}}^{t}=\mathbb{W}$; and

  2. 2.

for every $T\in\mathbb{W}$, there is some $\langle
H,T\rangle\in\bm{\mathsf{W}}$, with $H\subseteq T$.

For a belief interpretation $\langle\mathbb{W},I\rangle$ and a C19-belief
interpretation $\langle\bm{\mathsf{W}},H,T\rangle$, we write
$\langle\mathbb{W},I\rangle\preceq\langle\bm{\mathsf{W}},H,T\rangle$ if
$\bm{\mathsf{W}}\preceq\mathbb{W}$ and $I=T$. We write
$\bm{\mathsf{W}}\prec\mathbb{W}$ if $\bm{\mathsf{W}}\preceq\mathbb{W}$ and one
of the following conditions hold:

  1. 1.

there is $\langle H^{\prime},T^{\prime}\rangle\in\bm{\mathsf{W}}$ with
$H^{\prime}\subset T^{\prime}$; or

  2. 2.

$H\subset T$.

######  Definition 5.9.

A belief interpretation $\langle\mathbb{W},I\rangle$ is said to be a
_C19-equilibrium model_ of some theory $\Gamma$, in symbols
$\langle\mathbb{W},I\rangle\models_{eq}$ iff its is a belief model of $\Gamma$
and there is no C19-belief model $\mathcal{I}^{\prime}$ of $\Gamma$ with
$\mathcal{I}^{\prime}\prec\langle\mathbb{W},I\rangle$.

As a final step, we impose a fixpoint condition to minimize the agent’s
knowledge as follows.

######  Definition 5.10 (C19-world view).

An epistemic interpretation $\mathbb{W}$ is called a _C19-world view_ of
$\Gamma$ if:

$\displaystyle\mathbb{W}\ \ =\ \ \\{\ I\ |\
\langle\mathbb{W},I\rangle\models_{eq}\Gamma\ \\}$

######  Theorem 5.11 (Main Theorem of the paper by cafafa19a).

Given any ground program $\Pi$, its C19-world views coincide with its founded
G94-world views.

This theorem does not only guarantee that all C19-world views are founded, but
that the C19-world views are precisely those G94-world views that are founded.
As a result, it is easy to see that a program consisting of rule

$\displaystyle p\leftarrow\operatorname{\mathbf{K}}p$ (6)

has $[\\{\,\\}]$ as its unique C19-world view as expected, because this is the
only G94-world view that is founded. Similarly, a program consisting of rules

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055ptp\leftarrow\operatorname{\mathbf{K}}q\hskip
56.9055ptq\leftarrow\operatorname{\mathbf{K}}p$ (38)

has a unique founded G94-world views, namely $[\\{p\\},\\{q\\}]$, which is
thus its only C19-world view. The same applies to the program consisting of
rules

$\displaystyle p\operatorname{\,\text{or}\,}q\hskip
56.9055ptp\leftarrow\operatorname{\mathbf{K}}q\hskip
56.9055ptq\leftarrow\operatorname{\mathbf{K}}p\hskip
56.9055pt\leftarrow\operatorname{\text{not}}\operatorname{\mathbf{K}}p$ (51)

which has the same unique C19-world view.

Given that Theorem 5.11 states that the C19-world views are the founded
G94-world views, we may expect that these two semantics coincide for programs
where self-supported beliefs are not an issue. As mentioned above, this class
of programs is called epistemically tight and consist of programs that do not
have positive dependencies through subjective literals. Formally, the positive
epistemic dependence relation among atoms in a program $\Pi$ is defined so
that $dep^{+}(a,b)$ is true iff there is any rule $r\in\Pi$ such that
$a\in\mathit{Head}(r)\cup\mathit{Body}_{obj}(r)$ and
$b\in\mathit{Body}^{+}_{sub}(r)$.

######  Definition 5.12 (Epistemically tight program).

We say that an epistemic program $\Pi$ is _epistemically tight_ if we can
assign an integer mapping $\lambda:\text{\em At}\longrightarrow\mathbb{N}$ to
each atom such that

  1. 1.

$\lambda(a)=\lambda(b)$ for any rule $r\in\Pi$ and atoms
$a,b\in(\mathit{Atoms}(r)\setminus\mathit{Body}_{sub}(r))$,

  2. 2.

$\lambda(a)>\lambda(b)$ for any pair of atoms $a,b$ satisfying $dep^{+}(a,b)$.

######  Theorem 5.13 (Theorem 8 in the paper by fandinno19a).

C19- and G94-world views coincide for epistemically tight programs.

This class of programs includes for instance the eligibility program
introduced in Example 1 (Section 4.2). It also includes the programs
corresponding to the rules $\eqref{prg:g11.no.epistemic.splitting}$,
$\eqref{prg:g11.no.epistemic.splitting.no.constraint}$ and
$\eqref{eq:leckah18b}$ discussed above.

Theorems 5.11 and 5.13 also provide means for using tools to compute G94-world
views as a means to compute C19-world views. If the program is epistemically
tight, we can just use a tool for the G94 semantics directly. Otherwise, we
can use a tool for the G94 semantics to compute a candidate and then check
whether this candidate is founded.

Interestingly, the G94 semantics can also be characterized as a particular
class of theories under the C19 semantics as illustrated next. Let
$\mathbf{KEM}$ be the set containing the following form of _exclude middle
axiom_

$\displaystyle\operatorname{\mathbf{K}}\,(\ell\vee\operatorname{\text{not}}\ell)$

for every explicit literal $\ell$.

######  Proposition 5.14 (Proposition 5 by cafafa20a).

The G94-world views of any theory $\Gamma$ coincide precisely with the
C19-world views of $\Gamma\cup\mathbf{KEM}$.

In light of these results, we can understand the C19 semantics as a founded
version of the G94 semantics. Interestingly, these results allow for providing
founded versions for all of the semantics presented above. Recall from Section
5.2 that the K15-world views of any program $\Pi$ can be characterized as the
G94-world views of program $\Pi^{K}$ (Corollary 1). Using this translation we
can obtain a founded version of the K15 semantics.

######  Definition 5.15.

An epistemic interpretation $\mathbb{W}$ is called a _FK15-world view_ of
$\Gamma$ if $\mathbb{W}$ is a C19-world view of $\Gamma^{K}$.

A founded version of the G11 semantics can be obtained in a similar way, by
providing a variation of the translation $\cdot^{K}$ that only affects
positive occurrences of the operator $\operatorname{\mathbf{K}}$. Furthermore,
since S16-world views can be defined in terms of K15-world views, we can
immediately get a a founded version of the S15 semantics by replacing in the
definition of S16-world views each occurrence of K15 by FK15. A founded
version of the F15 semantics is slightly more involved and we refer to the
paper by Fandinno (2019) for more details.

###  5.7 The state of the search

So far in this section, we have reviewed the major approaches that have
addressed the issue of the existence of self-supported beliefs. While doing
so, we have also reviewed how these approaches behave with respect to several
properties inspired by properties satisfied by the stable model semantics.
Table 2 is taken from the paper by Fandinno (2019) and summarizes the known
results for these semantics with respect to those properties.

|  G94 |  G11 |  F15 |  K15 |  S16 |  C19
---|---|---|---|---|---|---
Supra-S5 |  ✓ |  ✓ |  ✓ |  ✓ |  ✓ |  ✓
Supra-ASP |  ✓ |  ✓ |  ✓ |  ✓ |  ✓ |  ✓
Sub. constraint monotonicity |  ✓ |  ✓ |  |  |  |  ✓
Splitting |  ✓ |  |  |  |  |  ✓
Foundedness |  |  |  |  |  |  ✓
Table 2: Summary of properties in different semantics.

As we can see, C19 is the only one that satisfies foundedness and, as
illustrated in Section 5.6, we can use this semantics to construct founded
versions of all other semantics. In fact, C19 can be considered as the
“founded version” of G94.

Another interesting fact is that only G94 and C19 satisfy the epistemic
splitting property. Founded versions of the other semantics do not satisfy
epistemic splitting either. In fact, this property seems to be tightly
connected with the _non-reflexivity_ of these two semantics. We say that a
semantics $\mathcal{S}$ is _reflexive_ when the $\mathcal{S}$-world views of
$\Gamma$ and ${\Gamma\cup\\{p\leftarrow\operatorname{\mathbf{K}}p\mid
p\in\text{\em At}\\}}$ coincide for every possible epistemic theory $\Gamma$.
It is easy to see that G11, F15, K15 and S16 are all reflexive, while G94 and
C19 are not. As a result of this trade-off, we can find examples that appear
to have self-supported beliefs in all semantics. Take for instance, the
program consisting of the following rules:

$\displaystyle p$ $\displaystyle\leftarrow\operatorname{\mathbf{K}}p$ (6)
$\displaystyle p$ $\displaystyle\operatorname{\,\text{or}\,}q$ (52)
$\displaystyle s$ $\displaystyle\leftarrow\operatorname{\mathbf{K}}p$ (53)
$\displaystyle\leftarrow\operatorname{\text{not}}s$ (54)

This program is the result of adding rule (6) to (39) and has the unique world
view $[\\{p,s\\}]$ according to all semantics. As mentioned above, for
reflexive semantics, rule (6) is redundant and the world views of this program
coincide with the world views of (39). We already analyzed this program in
previous sections and showed that $[\\{p,s\\}]$ is its unique G11- and
K15-world view. As mentioned in Section 5.3, being a unique K15-world view
immediately implies that this is also the unique S16-world view. It also can
be checked that this is the unique F15-world view. Note that the first rule
supports that $p$ may be true in some answer sets, but does not support that
$p$ is true in all answer sets. Therefore, the body of (53) is not supported
and neither should be $s$. Thus, both $p$ and $s$ are unsupported beliefs.
Recall that the reason why these semantics produce this unintended world view
is related with their failure to satisfy the epistemic splitting property. In
fact, program (39) has no world view according to any semantics that satisfy
epistemic splitting, like G94 or C19. However, as a result of the non-
reflexivity of these semantics, adding (6) produces the world view
$[\\{p,s\\}]$. This also seems unjustified as the body of (6) still lacks
justification. More research is necessary to understand the behavior of this
kind of programs and whether these apparently unsupported beliefs can be
avoided.

##  6 Relation to autoepistemic logics

It is well-known that, for any ground program that includes a choice rule for
all its atoms, its stable models coincide with the classical models of the
program understood as a propositional theory. In this section, we show that
there is a similar relation between some of the approaches for epistemic
specifications and some autoepistemic logics. Recall that autoepistemic logics
are nonmonotonic logics for modeling the beliefs of ideally rational agents
who reflect on their own beliefs.

The first and most influential of these logics was the one introduced by Moore
(1985). The language of autoepistemic logic is that of ordinary propositional
logic, augmented by a modal operator $\operatorname{\mathbf{L}}$. Formulas of
the form $\operatorname{\mathbf{L}}\varphi$ can be read as “$\varphi$ is
believed.” In order to make the comparison with epistemic specifications
easier, we replace the modal operator $\operatorname{\mathbf{L}}$ by
$\operatorname{\mathbf{K}}$. With this notation at hand, we can say that a set
of formulas $E$ is a _stable expansion_ of a theory $\Gamma$ (whose only modal
operator is $\operatorname{\mathbf{K}}$) if $E$ is the set of all consequences
(in the sense of classical propositional logic) of theory

$\displaystyle\Gamma\cup\\{\operatorname{\mathbf{K}}\varphi\mid\varphi\in
E\\}\cup\\{\operatorname{\text{not}}\operatorname{\mathbf{K}}\varphi\mid\varphi\notin
E\\}$

We can easily extend this definition to arbitrary theories by assuming that
operators $\operatorname{\mathbf{M}}$ and $\operatorname{\mathbf{not}}$ are
shorthands as stated in Table 1.

Moore soon realized that autoepistemic logic can be characterized in terms of
the consequences of modal logic KD45 instead of classical propositional logic.
Later, Schwarz (1992) showed that it is also possible to characterize
autoepistemic logic as a particular class of minimal epistemic models. This
characterization can be rewritten in form of a fixpoint similar to Definition
5.10. We name those epistemic models as M85-world views by analogy with
epistemic specifications.

######  Definition 6.16 (M85-world view).

We say that an epistemic interpretation $\mathbb{W}$ is an _M85-world view_ of
some theory $\Gamma$ when it satisfies the following fixpoint condition:

$\displaystyle\mathbb{W}\quad=\quad\\{\,I\mid\langle\mathbb{W},I\rangle\models\Gamma\,\\}$

######  Proposition 6.17 (Proposition 4.1 in the paper by schwarz92).

Let $\Gamma$ be a theory, $\mathbb{W}$ be an epistemic interpretation and
$E=\\{\varphi\mid\mathbb{W}\models\varphi\\}$ be the set of formulas satisfied
by $\mathbb{W}$. Then, $\mathbb{W}$ is a M85-world view of $\Gamma$ iff $E$ is
a stable expansion of $\Gamma$.

Proposition 6.17 provides a semantic characterization of Moore’s autoepistemic
logic. This semantic characterization is similar to the definition of
C19-world views. In fact, the definition of C19-world views is obtained by
replacing the satisfaction in modal logic KD45 by equilibrium satisfaction.
That is, by replacing $\langle\mathbb{W},I\rangle\models\Gamma$ by
$\langle\mathbb{W},I\rangle\models_{eq}\Gamma$. Similarly, the G94 semantics
can also be characterized as a similar fixpoint where the equilibrium
condition is weakened (see Appendix A in fandinno19a). This allows us to show
that autoepistemic logic can be captured by a particular class of theories
under the G94 or C19 semantics. Let $\mathbf{EM}$ be the set containing the
_excluded middle axiom_

$\displaystyle\ell\vee\operatorname{\text{not}}\ell$

for every explicit literal $\ell$.

######  Proposition 6.18 (Theorem 1 in the paper by cafafa19a).

The M85-world views of any theory $\Gamma$ coincide precisely with the
G94-world views of $\Gamma\cup\mathbf{EM}$.

######  Proposition 6.19.

The M85-world views of any theory $\Gamma$ coincide precisely with the
C19-world views of $\Gamma\cup\mathbf{EM}$.

######  Proof 6.20.

iff $\mathbb{W}$ is a M85-world view of $\Gamma$
iff $\mathbb{W}$ is a G94-world view of $\Gamma\cup\mathbf{EM}$ (Proposition
6.18)
iff $\mathbb{W}$ is a C19-world view of
$\Gamma\cup\mathbf{EM}\cup\mathbf{KEM}$ (Proposition 5.14)
iff $\mathbb{W}$ is a C19-world view of $\Gamma\cup\mathbf{KEM}$.
For the last equivalence, just note that any belief model of $\mathbf{EM}$ is
also a belief model of $\mathbf{KEM}$.

As mentioned above, the stable models of any theory that includes the excluded
middle axiom for all atoms coincide with its models in classical propositional
logic. Propositions 6.18 and 6.19 show that a similar relation exists between
the G94 and C19 semantics for epistemic specifications and Moore’s
autoepistemic logic. In this sense, we can consider these semantics the
“stable” versions of Moore’s autoepistemic logic.

Besides Moore’s autoepistemic logic, several alternatives have been studied in
the literature Konolige (1988); Marek and Truszczyński (1989); Niemelä (1991);
Schwarz (1991); most of them also motivated by the existence of self-supported
beliefs in this logic. In particular, one of this alternatives, called
_reflexive autoepistemic logic_ Schwarz (1991), is closely related to the K15
semantics for epistemic specifications.

Formally, a set of formulas $E$ is a _reflexive expansion_ of a theory
$\Gamma$ (whose only modal operator is $\operatorname{\mathbf{K}}$) if $E$ is
the set of all consequences (in the sense of classical propositional logic) of
the theory

$\displaystyle\Gamma\cup\\{\varphi\leftrightarrow\operatorname{\mathbf{K}}\varphi\mid\varphi\in
E\\}\cup\\{\operatorname{\text{not}}\operatorname{\mathbf{K}}\varphi\mid\varphi\notin
E\\}$

Alternatively, reflexive expansions can be characterized as Moore’s stable
expansions of its reflexive embedding $(\,\cdot\,)^{B}$ (see Section 5.2).

######  Proposition 6.21.

A set of formulas $E$ is a reflexive expansion of some theory $\Gamma$ iff it
is a stable expansion of the theory $\Gamma^{B}$.

######  Proof 6.22.

Directly from Theorem 10.30 and 10.48 by Marek and Truszczynski (1993).

Using this result, we can semantically characterize reflexive autoepistemic
logic as follows.555Alternatively, S92-world views can be characterized using
the modal logic SW5 instead of the reflexive embedding (see schwarz92).

######  Definition 6.23 (S92-world view).

We say that an epistemic interpretation $\mathbb{W}$ is an _S92-world view_ of
some theory $\Gamma$ when it satisfies the following fixpoint condition:

$\displaystyle\mathbb{W}\quad=\quad\\{\,I\mid\langle\mathbb{W},I\rangle\models\Gamma^{B}\,\\}$

######  Corollary 6.24.

Let $\Gamma$ be a theory, $\mathbb{W}$ be an epistemic interpretation and
$E=\\{\varphi\mid\mathbb{W}\models\varphi\\}$ be the set of formulas satisfied
by $\mathbb{W}$. Then, $E$ is a reflexive expansion of $\Gamma$ iff
$\mathbb{W}$ is a S92-world view of $\Gamma$.

The following result shows that K15 can be considered the “stable” version of
reflexive autoepistemic logic.

######  Proposition 6.25.

The S92-world views of any theory $\Gamma$ coincide precisely with the
K15-world views of $\Gamma\cup\mathbf{EM}$.

iff $\mathbb{W}$ is a S92-world view of $\Gamma$
iff $\mathbb{W}$ is a M85-world view of $\Gamma^{B}$ (By definition)
iff $\mathbb{W}$ is a G94-world view of $(\Gamma\cup\mathbf{EM})^{B}$
(Proposition 6.18)
iff $\mathbb{W}$ is a K15-world view of $\Gamma\cup\mathbf{EM}$ (Proposition
1)

##  7 Systems for computing world views

Currently, there are several systems to compute the world views of a epistemic
logic program: _ESmodels_ Zhang and Zhao (2014), _Wviews_ Kelly (2007, 2018),
_ELPS_ Balai and Kahl (2014), _GISolver_ Zhang et al. (2015), _ELPsolve_
Leclerc and Kahl (2016), _EP-ASP_ Le and Son (2017), _PelpSolver_ Zhang and
Zhang (2017), _EHEX_ Strasser (2018), _selp_ Bichler et al. (2020), _eclingo_
Cabalar et al. (2020).

Solver | Year | Semantics |  Underlying ASP solver | Imp. Lang |  Available Form
---|---|---|---|---|---
ELMO | 1994 | G94 |  dlv | Prolog |  n/a (in thesis)
sismodels | 1994 | G94 |  claspD | C++ |  n/a
Wviews | 2007 | G94 |  clingo | C++ |  Windows binary
Esmodels | 2013 | G11 |  clingo | (unknown) |  Windows binary
ELPS | 2014 | K15 |  Java | clingo |  source + binary
GISolver | 2015 | K15 |  clingo | (unknown) |  Windows binary
ELPsolve | 2016 | K15/S16 |  clingo | C++ |  binary only
Wviews2 | 2017 | G94 |  Python | clingo |  Windows binary
EP-ASP | 2017 | K15/S16 |  clingo | Python + ASP |  Windows binary
PelpSolver | 2017 | S16 |  clingo | Java |  Windows binary
ELPsolve2 | 2017 | S16 |  clingo | C++ |  currently not for public release
EHEX | 2018 | S16 |  clingo | Python |  source
selp | 2018 | S16 |  clingo | Python |  source
eclingo | 2020 | G94 |  clingo | Python |  source
Table 3: List of solvers for computing the world views of epistemic logic
programs.

A recent survey can be found in the paper by Leclerc and Kahl (2018b). For the
sake of completeness, Table 3 briefly summarizes some of the characteristics
of these solvers discussed in this survey with the addition of the recently
presented eclingo. It is worth mentioning that Hecher et al. (2020) recently
presented a new dynamic programming algorithm for computing the world views of
an epistemic logic program. This algorithm bounds the number of calls
necessary to the underlying solver for Answer Set Prolog by using the
treewidth of the program. The authors have communicated to us that they are
currently working on an implementation of this algorithm.

##  8 Conclusions and Challenges

The paper presents a review of the development of the Theory of Epistemic
Specifications. The language was introduced in the early nineties with the
goal of expanding Answer Set Prolog with means of reasoning with incomplete
information in the presence of multiple answer sets. It belongs to the body of
work aimed at better understanding and automating common sense reasoning by
developing formal knowledge representation languages and reasoning algorithms
and learning how they can be used to take a simple story, encode it on a
machine in some way, and then test to see if the machine can correctly answer
questions that a human can answer. Judea Pearl refers to such work as an
attempt to pass what he calls Mini-Turing Test (Pearl and Mackenzie 2018).
Even though we are still very far from passing the test, Epistemic
Specifications help to make a small step in the right direction. Their use
allows us to expand the collection of stories one can successfully deal with.
Section 4 shows examples of such stories. Unfortunately the progress was
limited to stories whose formalization did not require recursion through modal
operators. If such recursion were required the original semantics produced
counter-intuitive results. For a long time this line of research has been put
on the back burner but in the last decade we have seen a renewed interest in
the subject and there has been a substantial progress in the understanding of
the language. We described various approaches to defining the semantics,
relationships between them, and their properties. In addition, our
understanding was deepened by discoveries of important connections between
epistemic specifications and (both monotonic and non-monotonic) modal logics.
Despite this progress we still have a number of important open problems to
solve.

We need to gain more experience in using epistemic specifications for
knowledge representation. This will allow us to learn if the expressive power
of the language is sufficient for its original purpose. In particular, it
remains to be seen if the language is fully suited for representing various
forms of the Closed World Assumption – one of its original goals. This is also
necessary for the development of methodologies for the use of epistemic
specifications.

More work is needed to further develop the mathematical theory of epistemic
specifications. Most formal results are only specified for the propositional
fragment of the language while the use of quantifiers for knowledge
representation seems essential. We also need to check whether the theory of
Answer Set Prolog modules can be adapted to work in epistemic specifications,
study various forms of equivalence between epistemic theories (some
preliminary work on strong and uniform equivalence has been reported in the
papers by famowo19a famowo19a,famowo19b; and sufahe20), find conditions for