Founded World Views with Autoepistemic Equilibrium Logic

TL;DR

This paper introduces a formal property called foundedness for epistemic logic programs, proposes a new semantics combining Autoepistemic and Equilibrium Logic, and shows it accurately captures the intended world views without self-support.

Contribution

It extends unfounded set concepts to epistemic logic, defines foundedness, and proposes a new semantics that ensures only founded world views are derived.

Findings

The new semantics captures all founded G91 world views.

Previous approaches violate foundedness, leading to self-supported world views.

Formalizes the notion of foundedness in epistemic logic programming.

Abstract

Defined by Gelfond in 1991 (G91), epistemic specifications (or programs) are an extension of logic programming under stable models semantics that introducessubjective literals. A subjective literal al-lows checking whether some regular literal is true in all (or in some of) the stable models of the program, being those models collected in a setcalledworld view. One epistemic program may yield several world views but, under the original G91 semantics, some of them resulted from self-supported derivations. During the last eight years, several alternative approaches have been proposed to get rid of these self-supported worldviews. Unfortunately, their success could only be measured by studying their behaviour on a set of common examples in the literature, since no formal property of "self-supportedness" had been defined. To fill this gap, we extend in this paper the idea of unfounded set from standard logic programming to the epistemic case. We define when a world view is founded with respect to some program and propose the foundedness property for any semantics whose world views are always founded. Using counterexamples, we explain that the previous approaches violate foundedness, and proceed to propose a new semantics based on a combination of Moore's Autoepistemic Logic and Pearce's Equilibrium Logic. The main result proves that this new semantics precisely captures the set of founded G91 world views.

Equations

$$a\leftarrow \neg Kb$$

$$b\leftarrow \neg Ka$$

$$a\leftarrow Ka$$

$$\phi ::=\perp \mid a\mid {\phi }_1\wedge {\phi }_2\mid {\phi }_1\vee {\phi }_2\mid {\phi }_1\to {\phi }_2\mid K\phi \text{ for any atom }a\in \mathcal{A}\mathcal{T}.$$

$$a_1\vee \dots \vee a_n\leftarrow B_1\wedge \dots \wedge B_m$$

$$a\vee ba\leftarrow Kbb\leftarrow Ka$$

$$a\vee bc\leftarrow Ka\perp \leftarrow \neg c$$

$$\mathbb{W}=\{T|(\mathbb{W},T)\in \mathrm{WEQ}[\Gamma ]\}$$

$$\mathbb{W}=\{T|\mathbb{W}\cup \{T\}\subseteq \mathrm{EQ}[{\Gamma }^{\mathbb{W}}]\}$$

$$\displaystyle\mathbb{S}\ \ \mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr$\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=$\cr\kern-0.1pt\cr}}}\ \ \big{\{}\ \langle X,I\rangle\ \ \big{|}\ \ \langle H,I\rangle\in\mathbb{W}^{\prime}\text{ with }X=I\setminus H\text{ and }X\neq\emptyset\ \big{\}}$$

$$\mathbb{W}=\{T|(\mathbb{W},T)\in \mathrm{EQB}[\Gamma \cup \{\perp \leftarrow \phi \}]\}$$

$$\mathbb{W}=\{T|(\mathbb{W},T)\in \mathrm{EQB}[\Gamma ]\}$$

Full text

1 Introduction

The language of epistemic specifications, proposed by Gelfond in 1991 [4], extends disjunctive logic programs (under the stable model [6] semantics) with modal constructs called subjective literals. Using these constructs, it is possible to check whether a regular literal $l$ is true in every stable model (written $\operatorname{\mathbf{K}}l$) or in some stable model (written $\operatorname{\mathbf{M}}l$) of the program. For instance, the rule:

[TABLE]

means that $a$ must hold if we cannot prove that all the stable models contain $b$. Subjective literals have been incorporated as an extension of the Answer Set Programming (ASP) paradigm [14, 18] in different solvers and implementations – see [12] for a recent survey. The definition of a “satisfactory” semantics for epistemic specifications has proved to be a non-trivial enterprise, as shown by the list of different attempts proposed so far [2, 4, 5, 9, 23, 24, 25]. The main difficulty arises because subjective literals query the set of stable models but, at the same time, occur in rules that determine those stable models. As an example, the program consisting of:

[TABLE]

and (1) has now two rules defining atoms $a$ and $b$ in terms of the presence of those same atoms in all the stable models. To solve this kind of cyclic interdependence, the original semantics by Gelfond [4] (G91) considered different alternative world views or sets of stable models. In the case of program (1)-(2), G91 yields two alternative world views111For the sake of readability, sets of propositional interpretations are embraced with $[\ ]$ rather than $\{\ \}$., $[\{a\}]$ and $[\{b\}]$, each one containing a single stable model, and this is also the behaviour obtained in the remaining approaches developed later on. The feature that made G91 unconvincing, though, was the generation of self-supported world views. A prototypical example for this effect is the epistemic program consisting of the single rule:

[TABLE]

whose world views under G91 are $[\emptyset]$ and $[\{a\}]$. The latter is considered as counter-intuitive by all authors222This includes Gelfond himself, who proposed a new variant in [5] motivated by this same example and further modified this variant later on in [9]. because it relies on a self-supported derivation: $a$ is derived from $\operatorname{\mathbf{K}}a$ by rule (3), but the only way to obtain $\operatorname{\mathbf{K}}a$ is rule (3) itself. Although the rejection of world views of this kind seems natural, the truth is that all approaches in the literature have concentrated on studying the effects on individual examples, rather than capturing the absence of self-supportedness as a formal property. To achieve such a goal, we would need to establish some kind of derivability condition in a very similar fashion as done with unfounded sets [3] for standard logic programs. To understand the similarity, think about the (tautological) rule $a\leftarrow a$. The classical models of this rule are $\emptyset$ and $\{a\}$, but the latter cannot be a stable model because $a$ is not derivable applying the rule. Intuitively, an unfounded set is a collection of atoms that is not derivable from a given program and a fixed set of assumptions, as happens to $\{a\}$ in the last example. As proved by [13], the stable models of any disjuntive logic program are precisely its classical models that are founded, that is, that do not admit any unfounded set. As we can see, the situation in (3) is pretty similar to $a\leftarrow a$ but, this time, involves derivability through subjective literals. An immediate option is, therefore, extending the definition of unfounded sets for the case of epistemic programs – this constitutes, indeed, the first contribution of this paper.

Once the property of founded world views is explicitly stated, the paper proposes a new semantics for epistemic specifications, called Founded Autoepistemic Equilibrium Logic (FAEEL), that fulfills that requirement. In the spirit of [2, 25], our proposal actually constitutes a full modal non-monotonic logic where $\operatorname{\mathbf{K}}$ becomes the usual necessity operator applicable to arbitrary formulas. Formally, FAEEL is a combination of Pearce’s Equilibrium Logic [20], a well-known logical characterisation of stable models, with Moore’s Autoepistemic Logic (AEL) [17], one of the most representative approaches among modal non-monotonic logics. The reason for choosing Equilibrium Logic is quite obvious, as it has proved its utility for characterising other extensions of ASP, including the already mentioned epistemic approaches in [2, 25]. As for the choice of AEL, it shares with epistemic specifications the common idea of agent’s introspection where $\operatorname{\mathbf{K}}\varphi$ means that $\varphi$ is one of the agent’s beliefs. The only difference is that those beliefs are just classical models in the case of AEL whereas epistemic specifications deal with stable models instead. Interestingly, the problem of self-supported models has also been extensively studied in AEL [11, 15, 19, 21], where the formula $\operatorname{\mathbf{K}}a\to a$, analogous to (3), also yields an unfounded world view333Technically, AEL is defined in terms of theory expansions but each one can be characterised by a canonical S5-model with the same form of a world view [16, 22].

$[\{a\}]$. Our solution consists in combining the monotonic bases of AEL and Equilibrium Logic (the modal logic KD45 and the intermediate logic of Here-and-There (HT) [8], respectively), but defining a two-step models selection criterion that simultaneously keeps the agent’s beliefs as stable models and avoids unfounded world views from the use of the modal operator $\operatorname{\mathbf{K}}$. As expected, we prove that FAEEL guarantees the property of founded world views, among other features. Our main result, however, goes further and asserts that the FAEEL world views of an epistemic program are precisely the set of founded G91 world views. We reach, in this way, an analogous situation to the case of standard logic programming, where stable models are the set of founded classical models of the program.

The rest of the paper is organised as follows. Section 2 and 3 respectively revisit the background knowledge about equilibrium logic and epistemic specifications necessary for the rest of the paper. Section 4 introduces the foundedness property for epistemic logic programs. In Section 5, we introduce FAEEL and show that its world views precisely coincide with the set of founded G91 world views. Finally, Section 6 concludes the paper.

2 Background

We begin recalling the basic definitions of equilibrium logic and its relation to stable models. We start from the syntax of propositional logic, with formulas built from combinations of atoms in a set $\mathcal{AT}$ with operators $\wedge,\vee,\bot$ and $\to$ in the usual way. We define the derived operators \varphi\leftrightarrow\psi\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}(\varphi\to\psi)\wedge(\psi\to\varphi),  (\varphi\leftarrow\psi)\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}(\psi\to\varphi),  \neg\varphi\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}(\varphi\to\bot) and  \top\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}\neg\bot.

A propositional interpretation $T$ is a set of atoms $T\subseteq\mathcal{AT}$. We write $T\models\varphi$ to represent that $T$ classically satisfies formula $\varphi$. An HT-interpretation is a pair $\langle H,T\rangle$ (respectively called “here” and “there”) of propositional interpretations such that $H\subseteq T\subseteq\mathcal{AT}$; it is said to be total when $H=T$. We write $\langle H,T\rangle\models\varphi$ to represent that $\langle H,T\rangle$ satisfies a formula $\varphi$ under the recursive conditions:

• •

$\langle H,T\rangle\not\models\bot$

• •

$\langle H,T\rangle\models p$ iff $p\in H$

• •

$\langle H,T\rangle\models\varphi\wedge\psi$ iff $\langle H,T\rangle\models\varphi$ and $\langle H,T\rangle\models\psi$

• •

$\langle H,T\rangle\models\varphi\vee\psi$ iff $\langle H,T\rangle\models\varphi$ or $\langle H,T\rangle\models\psi$

• •

$\langle H,T\rangle\models\varphi\to\psi$ iff both (i) $T\models\varphi\to\psi$ and (ii) $\langle H,T\rangle\not\models\varphi$ or $\langle H,T\rangle\models\psi$

As usual, we say that $\langle H,T\rangle$ is a model of a theory $\Gamma$, in symbols $\langle H,T\rangle\models\Gamma$, iff $\langle H,T\rangle\models\varphi$ for all $\varphi\in\Gamma$. It is easy to see that $\langle T,T\rangle\models\Gamma$ iff $T\models\Gamma$ classically. For this reason, we will identify $\langle T,T\rangle$ simply as $T$ and will use ‘$\models$’ indistinctly. By $\text{\rm CL}[\Gamma]$ we denote the set of all classical models of $\Gamma$. Interpretation $\langle T,T\rangle=T$ is a stable (or equilibrium) model of a theory $\Gamma$ iff $T\models\Gamma$ and there is no $H\subset T$ such that $\langle H,T\rangle\models\Gamma$. We write $\text{\rm SM}[\Gamma]$ to stand for the set of all stable models of $\Gamma$. Note that $\text{\rm SM}[\Gamma]\subseteq\text{\rm CL}[\Gamma]$ by definition.

3 G91 semantics for epistemic theories

In this section we provide a straightforward generalisation of G91 allowing its application to arbitrary modal theories. Formulas are extended with the necessity operator $\operatorname{\mathbf{K}}$ according to the following grammar:

[TABLE]

An (epistemic) theory is a set of formulas as defined above. In our context, the epistemic reading of $\operatorname{\mathbf{K}}\psi$ is that “$\psi$ is one of the agent’s beliefs.” Thus, a formula $\varphi$ is said to be subjective if all its atom occurrences (having at least one) are in the scope of $\operatorname{\mathbf{K}}$. Analogously, $\varphi$ is said to be objective if $\operatorname{\mathbf{K}}$ does not occur in $\varphi$. For instance, $\neg\!\operatorname{\mathbf{K}}a\vee\operatorname{\mathbf{K}}b$ is subjective, $\neg a\vee b$ is objective and $\neg a\vee\operatorname{\mathbf{K}}b$ none of the two.

To represent the agent’s beliefs we will use a set $\mathbb{W}$ of propositional interpretations. We call belief set to each element $I\in\mathbb{W}$ and belief view to the whole set $\mathbb{W}$. The difference between belief and knowledge is that the former may not hold in the real world. Thus, satisfaction of formulas will be defined with respect to an interpretation $I\subseteq\mathcal{AT}$, possibly $I\not\in\mathbb{W}$, that accounts for the real world: the pair $({\mathbb{W},I})$ is called belief interpretation (or interpretation in modal logic KD45). Modal satisfaction is also written $({\mathbb{W},I})\models\varphi$ (ambiguity is removed by the interpretation on the left) and follows the conditions:

• •

$({\mathbb{W},I})\not\models\bot$,

• •

$({\mathbb{W},I})\models a$ iff $a\in I$, for any atom $a\in\mathcal{AT}$,

• •

$({\mathbb{W},I})\models\psi_{1}\wedge\psi_{2}$ iff $({\mathbb{W},I})\models\psi_{1}$ and $({\mathbb{W},I})\models\psi_{2}$,

• •

$({\mathbb{W},I})\models\psi_{1}\vee\psi_{2}$ iff $({\mathbb{W},I})\models\psi_{1}$ or $({\mathbb{W},I})\models\psi_{2}$,

• •

$({\mathbb{W},I})\models\psi_{1}\to\psi_{2}$ iff $({\mathbb{W},I})\not\models\psi_{1}$ or $({\mathbb{W},I})\models\psi_{2}$, and

• •

$({\mathbb{W},I})\models\operatorname{\mathbf{K}}\psi$ iff $({\mathbb{W},J})\models\psi$ for all $J\in\mathbb{W}$.

Notice that implication here is classical, that is, $\varphi\to\psi$ is equivalent to $\neg\varphi\vee\psi$ in this context. A belief interpretation $({\mathbb{W},I})$ is a belief model of $\Gamma$ iff $({\mathbb{W},J})\models\varphi$ for all $\varphi\in\Gamma$ and all $J\in\mathbb{W}\cup\{I\}$ – additionally, when $I\in\mathbb{W}$, we further say that $\mathbb{W}$ is an epistemic model of $\Gamma$ and abbreviate this as $\mathbb{W}\models\Gamma$. Belief models defined in this way correspond to modal logic KD45 whereas epistemic models correspond to S5.

Example 1

Take the theory $\Gamma_{\ref{f:loop1}}=\{\neg\!\operatorname{\mathbf{K}}b\to a\}$ corresponding to rule (1). An epistemic model $\mathbb{W}\models\Gamma_{\ref{f:loop1}}$ must satisfy: $\langle\mathbb{W},J\rangle\models\operatorname{\mathbf{K}}b$ or $\langle\mathbb{W},J\rangle\models a$, for all $J\in\mathbb{W}$. We get three epistemic models from $\operatorname{\mathbf{K}}b$, $[\{b\}]$, $[\{a,b\}]$, and $[\{b\},\{a,b\}]$ and the rest of cases must force $a$ true, so we also get $[\{a\}]$ and $[\{a\},\{a,b\}]$. In other words, $\Gamma_{\ref{f:loop1}}$ has the same epistemic models than $\operatorname{\mathbf{K}}b\vee\operatorname{\mathbf{K}}a$.   $\Box$

Note that rule (1) alone did not seem to provide any reason for believing $b$, but we got three epistemic models above satisfying $\operatorname{\mathbf{K}}b$. Thus, we will be interested only in some epistemic models (we will call world views) that minimize the agent’s beliefs in some sense. To define such a minimisation we rely on the following syntactic transformation provided by [24].

Definition 1** (Subjective reduct)**

The subjective reduct of a theory $\Gamma$ with respect to a belief view $\mathbb{W}$, also written $\Gamma^{\mathbb{W}}$, is obtained by replacing each maximal subformula of the form $\operatorname{\mathbf{K}}\varphi$ by: $\top$, if $\mathbb{W}\models\operatorname{\mathbf{K}}\varphi$; by $\bot$, otherwise. Notice that $\Gamma^{\mathbb{W}}$ is a classical, non-modal theory.  $\Box$

Finally, we impose a fixpoint condition where, depending on whether each belief set $I\in\mathbb{W}$ is required to be a stable model of the reduct or just a classical model, we get G91 or AEL semantics, respectively.

Definition 2** (AEL and G91 world views)**

A belief view $\mathbb{W}$ is called an AEL-world view of a theory $\Gamma$ iff $\mathbb{W}=\text{\rm CL}[\Gamma^{\mathbb{W}}]$, and is called a G91-world view of $\Gamma$ iff $\mathbb{W}=\text{\rm SM}[\Gamma^{\mathbb{W}}]$.  $\Box$

Example 2** (Example 1 revisited)**

Take any $\mathbb{W}$ such that $\mathbb{W}\models\operatorname{\mathbf{K}}b$. Then, $\Gamma_{\ref{f:loop1}}^{\mathbb{W}}=\{\bot\to a\}$ with $\text{\rm CL}[\Gamma_{\ref{f:loop1}}^{\mathbb{W}}]=[\emptyset,\{a\},\{b\},\{a,b\}]$ and $\text{\rm SM}[\Gamma_{\ref{f:loop1}}^{\mathbb{W}}]=[\emptyset]$. None of the two satisfy $\operatorname{\mathbf{K}}b$ so $\mathbb{W}$ cannot be fixpoint for G91 or AEL. If $\mathbb{W}\not\models\operatorname{\mathbf{K}}b$ instead, we get $\Gamma_{\ref{f:loop1}}^{\mathbb{W}}=\{\top\to a\}$, whose classical models are $\{a\}$ and $\{a,b\}$, but only the former is stable. As a result, $\mathbb{W}=[\{a\},\{a,b\}]$ is the unique AEL world view and $\mathbb{W}=[\{a\}]$ the unique G91 world view.   $\Box$

Example 3

Take now the theory $\Gamma_{\ref{f:self}}=\{\operatorname{\mathbf{K}}a\to a\}$ corresponding to rule (3). If $\mathbb{W}\models\operatorname{\mathbf{K}}a$ we get $\Gamma_{\ref{f:self}}^{\mathbb{W}}=\{\top\to a\}$ and $\text{\rm CL}[\Gamma_{\ref{f:self}}^{\mathbb{W}}]=\text{\rm SM}[\Gamma_{\ref{f:self}}^{\mathbb{W}}]=\{a\}$ so $\mathbb{W}=[\{a\}]$ is an AEL and G91 world view. If $\mathbb{W}\not\models\operatorname{\mathbf{K}}a$, the reduct becomes $\Gamma_{\ref{f:self}}^{\mathbb{W}}=\{\bot\to a\}$, a classical tautology with unique stable model $\emptyset$. As a result, $\mathbb{W}=[\emptyset,\{a\}]$ is the other AEL world view, while $\mathbb{W}=[\emptyset]$ is the a second G91 world view.   $\Box$

As we can see, the difference between AEL and G91 is that we use classical $\text{\rm CL}[\Gamma^{\mathbb{W}}]$ instead of stable $\text{\rm SM}[\Gamma^{\mathbb{W}}]$ models, respectively. It is well known that adding the excluded middle axiom $a\vee\neg a$ for all atoms makes equilibrium logic collapse into classical logic. This leads us to the following result.

Theorem 1

$\mathbb{W}$* is an AEL world view of some theory $\Gamma$ iff $\mathbb{W}$ is a G91-world view of $\Gamma\cup\{a\vee\neg a\mid a\in\mathcal{AT}\}$.  $\Box$*

4 Founded world views of epistemic specifications

As we explained in the introduction, world view $[\{a\}]$ of $\{\operatorname{\mathbf{K}}a\to a\}$ is considered to be “self-supported” in the literature but, unfortunately, there is no formal definition for such a concept, to the best of our knowledge. To cover this lack, we proceed to extend here the idea of unfounded sets from disjunctive logic programs to the epistemic case. For this purpose, we focus next on the original language of epistemic specifications [4] (a fragment of epistemic theories closer to logic programs) on which most approaches have been actually defined.

Let us start by introducing some terminology. An objective literal is either an atom $a\in\mathcal{AT}$, its negation $\neg a$ or its double negation $\neg\neg a$. A subjective literal is any of the formulas444We focus here on the study of the operator $\operatorname{\mathbf{K}}$, but epistemic specifications also allow a second operator $\operatorname{\mathbf{M}}l$ whose relation to $\operatorname{\mathbf{K}}$ is also under debate and, for this reason, we leave it future work. $\operatorname{\mathbf{K}}l$, $\neg\!\operatorname{\mathbf{K}}l$ or $\neg\neg\!\operatorname{\mathbf{K}}l$ where $l$ an objective literal. A literal is either an objective or a subjective literal, and is called negative if it contains negation and positive otherwise. A rule is a formula of the form

[TABLE]

with $n\geq 0$, $m\geq 0$ and $m+n>0$, where each $a_{i}$ is an atom and each $B_{j}$ is a literal. For any rule $r$ like (4), we define its body as \mathit{Body}(r)\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}B_{1}\wedge\dotsc\wedge B_{m} and its head \mathit{Head}(r)\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scriptscriptstyle\mathrm{def}$\cr\kern 1.0pt\cr$=\cr\kern-0.1pt\cr}}}a_{1}\vee\dotsc\vee a_{n}, which we sometimes use as the set of atoms $\{a_{1},\dotsc,a_{n}\}$. When $n=0$, $\mathit{Head}(r)=\bot$ and the rule is a constraint, whereas if $m=0$ then $\mathit{Body}(r)=\top$ and the rule is a fact. The set $\mathit{Body}^{+}_{ob}(r)$ collects all atoms occurring in positive objective literals in the body while $\mathit{Body}^{+}_{sub}(r)$ collects all atoms occurring in positive subjective literals. An epistemic specification or program is a set of rules. As with formulas, a program without occurrences of $\operatorname{\mathbf{K}}$ is said to be objective (it corresponds to a standard disjunctive logic program with double negation).

Definition 3** (Unfounded set)**

Let $\Pi$ be a program and $\mathbb{W}$ a belief view. 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}$, we have that $X$ and $I$ are sets of atoms and there is no rule $r\in\Pi$ with $\mathit{Head}(r)\cap X\neq\emptyset$ satisfying:

$({\mathbb{W},I})\models\mathit{Body}(r)$** 2. 2.

$\mathit{Body}^{+}_{ob}(r)\cap X=\emptyset$** 3. 3.

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

$\mathit{Body}^{+}_{sub}(r)\cap Y=\emptyset$* with $Y=\bigcup\{\ X^{\prime}\ |\ \langle X^{\prime},I^{\prime}\rangle\in\mathbb{S}\ \}$.  $\Box$*

The definition works in a similar way to standard unfounded sets [13, Definition 3.1]. In fact, the latter corresponds to the first three conditions above, except that we use $({\mathbb{W},I})$ to check $\mathit{Body}(r)$, as it may contain now subjective literals. Intuitively, each $I$ represents some potential belief set (or stable model) and $X$ is some set of atoms without a “justifying” rule, that is, there is no $r\in\Pi$ allowing a positive 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 in our definition is the addition of condition 4: to consider $r$ a justifying rule, we additionally require not using 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 4** (Founded world view)**

Let $\Pi$ be a program and $\mathbb{W}$ be a belief view. We say that $\mathbb{W}$ is unfounded if there is some unfounded-set $\mathbb{S}$ s.t., for every $\langle X,I\rangle\in\mathbb{S}$, we have $I\in\mathbb{W}$ and $X\cap I\neq\emptyset$. $\mathbb{W}$ is called founded otherwise.  $\Box$

When $\Pi$ is an objective program, each pair $\langle X,I\rangle$ corresponds to a standard unfounded set $X$ of some potential stable model $I$ in the traditional sense of [13].

Example 4

Given the single disjunctive rule $a\vee b$ suppose we check the (expected) world view $\mathbb{W}=[\{a\},\{b\}]$. For $I=\{a\}$ and $X=\{a\}$, rule $a\vee b$ satisfies the four conditions and justifies $a$. The same happens for $I=\{b\}=X$. So, $\mathbb{W}$ is founded. However, suppose we try with $\mathbb{W}^{\prime}=[\{a,b\}]$ instead. For $I=\{a,b\}$ we can form $X=\{a\}$ and $X^{\prime}=\{b\}$ and in both cases, the only rule in the program, $a\vee b$, violates condition 3. As a result, $\mathbb{W}^{\prime}$ is unfounded due to the set $\mathbb{S}^{\prime}=\{\langle\{b\},\{a,b\}\rangle,\langle\{a\},\{a,b\}\rangle\}$.  $\Box$

To illustrate how condition 4 works, let us continue with Example 3.

Example 5** (Example 3 continued)**

Theory $\Gamma_{\ref{f:self}}=\{\operatorname{\mathbf{K}}a\to a\}$ is also a program. Given belief set $\mathbb{W}=[\{a\}]$ we can observe that $\mathbb{S}=[\langle\{a\},\{a\}\rangle]$ makes $\mathbb{W}$ unfounded because the unique rule in $\Gamma_{\ref{f:self}}$ does not fulfill condition 4: we cannot derive $a$ from a rule that contains $a\in\mathit{Body}^{+}_{sub}(r)$. On the other hand, the other G91 world view, $\mathbb{W}=[\emptyset]$, is trivially founded.  $\Box$

Since Definition 4 only depends on some epistemic program and its selected world views, we can raise it to a general property for any epistemic semantics.

Property 1** (Foundedness)**

A semantics satisfies foundedness when all the world views it assigns to any program $\Pi$ are founded.   $\Box$

Approaches proposed after G91 do remove unfounded world views in the examples studied in the literature, but unfortunately, this does not mean that they generally satisfy foundedness. Let us consider a common counterexample.

Example 6

Take the epistemic logic program:

[TABLE]

whose G91-world views are $\mathbb{W}=[\{a\},\{b\}]$ and $\mathbb{W}^{\prime}=[\{a,b\}]$. These are, indeed, the two cases we analysed in Example 4. $\mathbb{W}$ is again founded because $a\vee b$ keeps justifying both possible $\langle X,I\rangle$ pairs, that is, $[\langle\{a\},\{a\}\rangle]$ and $[\langle\{b\},\{b\}\rangle]$. However, for $\mathbb{W}^{\prime}$ we still 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 as before, but also condition 4 for the other two rules.  $\Box$

Note how $\mathbb{S}^{\prime}$ allows us to spot the root of the derivability problem: to justify $a$ in $\langle\{a\},\{a,b\}\rangle$ we cannot use $a\leftarrow\operatorname{\mathbf{K}}b$ because $b$ is part of the unfounded structure $X$ in the other pair $\langle\{b\},\{a,b\}\rangle$, and vice versa. Since the variants by Gelfond in [5] (G11) and Kahl et al. [9] (K15) also assign the unfounded world view $\mathbb{W}^{\prime}$ to $\Pi_{\ref{theory:larger.set.of.worlds}}$ (in fact, they coincide with G91 for this program), we can conclude that G11 and K15 do not satisfy foundedness either.

A more elaborated strategy is adopted by the recent approaches by Fariñas et al.  [2] (F15) and Shen and Eiter [23] (S17), that treat the previous world views as candidate solutions555In [2], these candidate world views are called epistemic equilibrium models while selected world views receive the name of autoepistemic equilibrium models., but select the ones with minimal knowledge in a second step. This allows removing the unfounded world view $[\{a,b\}]$ in Example 6, because the other solution $[\{a\},\{b\}]$ provides less knowledge. Unfortunately, this strategy does not suffice to guarantee foundedness, since other formulas (such as constraints) may remove the founded world view, as explained below.

Example 7** (Example 6 continued)**

Take the program $\Pi_{2}=\Pi_{\ref{theory:larger.set.of.worlds}}\cup\{\bot\leftarrow\neg\!\operatorname{\mathbf{K}}a\}$. The constraint rules out $\mathbb{W}=[\{a\},\{b\}]$ because the latter satisfies $\neg\!\operatorname{\mathbf{K}}a$. In G91, G11, F15 and S17, only world view $\mathbb{W}^{\prime}=[\{a,b\}]$ is left, so knowledge minimisation has no effect. However, $\mathbb{W}^{\prime}$ is still unfounded in $\Pi_{\ref{theory:larger.set.of.worlds2}}$ since constraints do not affect that feature (their empty head never justifies any atom).  $\Box$

As a conclusion, semantics F15 and S17 do not satisfy foundedness either.

5 Founded Autoepistemic Equilibrium Logic

We present now the semantics proposed in this paper, introducing Founded Autoepistemic Equilibrium Logic (FAEEL). The basic idea is an elaboration of the belief (or KD45) interpretation $({\mathbb{W},I})$ already seen but replacing belief sets by HT pairs. Thus, we extend now the idea of belief view $\mathbb{W}$ to a non-empty set of HT-interpretations $\mathbb{W}=\{\langle H_{1},T_{1}\rangle,\dots,\langle H_{n},T_{n}\rangle\}$ and say that $\mathbb{W}$ is total when $H_{i}=T_{i}$ for all of them, coinciding with the form of belief views $\mathbb{W}=\{T_{1},\dots,T_{n}\}$ we had so far. Similarly, a belief interpretation is now redefined as $({\mathbb{W},\langle H,T\rangle})$, or simply $({\mathbb{W},H,T})$, where $\mathbb{W}$ is a belief view and $\langle H,T\rangle$ stands for the real world, possibly not in $\mathbb{W}$. Next, we redefine the satisfaction relation from a combination of modal logic KD45 and HT. A belief interpretation $\mathcal{I}= ({\mathbb{W},H,T})$ satisfies a formula $\varphi$, written $\mathcal{I}\models\varphi$, iff:

• •

$\mathcal{I}\not\models\bot$,

• •

$\mathcal{I}\models a$ iff $a\in H$, for any atom $a\in\mathcal{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) $({\mathbb{W}^{t},T})\not\models\psi_{1}$ or $({\mathbb{W}^{t},T})\models\psi_{2}$, where $\mathbb{W}^{t}=\{T_{i}\mid\langle H_{i},T_{i}\rangle\in\mathbb{W}\}$.

• •

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

For total belief interpretations, this new satisfaction relation collapses to the one in Section 3 (that is, KD45). Interpretation $({\mathbb{W},H,T})$ is a belief model of $\Gamma$ iff $({\mathbb{W},H_{i},T_{i}})\models\varphi$ for all $\langle H_{i},T_{i}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$ and all $\varphi\in\Gamma$ – additionally, when $\langle H,T\rangle\in\mathbb{W}$, we further say that $\mathbb{W}$ is an epistemic model of $\Gamma$, abbreviated as $\mathbb{W}\models\Gamma$.

Proposition 1** (Persistence)**

$({\mathbb{W},H,T})\models\varphi$* implies $({\mathbb{W}^{t},T})\models\varphi$.  $\Box$*

A belief model just captures collections of HT models which need not be in equilibrium. To make the agent’s beliefs correspond to stable models we impose a particular minimisation criterion on belief models.

Definition 5

We define the partial order $\mathcal{I}^{\prime}\preceq\mathcal{I}$ for belief interpretations $\mathcal{I}^{\prime}=({\mathbb{W}^{\prime},H^{\prime},T^{\prime}})$ and $\mathcal{I}=({\mathbb{W},H,T})$ when the following three conditions hold:

$T^{\prime}=T$* and $H^{\prime}\subseteq H$, and* 2. 2.

for every $\langle H_{i},T_{i}\rangle\in\mathbb{W}$, there is some $\langle H^{\prime}_{i},T_{i}\rangle\in\mathbb{W}^{\prime}$, with $H^{\prime}_{i}\subseteq H_{i}$. 3. 3.

*for every $\langle H^{\prime}_{i},T_{i}\rangle\in\mathbb{W}^{\prime}$, there is some $\langle H_{i},T_{i}\rangle\in\mathbb{W}$, with $H^{\prime}_{i}\subseteq H_{i}$.  *$\Box$

As usual, $\mathcal{I}^{\prime}\prec\mathcal{I}$ means $\mathcal{I}^{\prime}\preceq\mathcal{I}$ and $\mathcal{I}^{\prime}\neq\mathcal{I}$. The intuition for $\mathcal{I}^{\prime}\preceq\mathcal{I}$ is that $\mathcal{I}^{\prime}$ contains less information than $\mathcal{I}$ for each fixed $T_{i}$ component. As a result, $\mathcal{I}^{\prime}\models\varphi$ implies $\mathcal{I}\models\varphi$ for any formula $\varphi$ without implications other than $\neg\psi=\psi\to\bot$.

Definition 6

A total belief interpretation $\mathcal{I}=({\mathbb{W},T})$ is said to be an equilibrium belief model of some theory $\Gamma$ iff $\mathcal{I}$ is a belief model of $\Gamma$ and there is no other belief model $\mathcal{I}^{\prime}$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$.  $\Box$

By ${\rm{EQB}}[\Gamma]$ we denote the set of equilibrium belief models of $\Gamma$. As a final step, we impose a fixpoint condition to minimise the agent’s knowledge as follows.

Definition 7

A belief view $\mathbb{W}$ is called an equilibrium world view of $\Gamma$ iff: {IEEEeqnarray}c+x* W  =   $\{\ T\ |\ ({\mathbb{W},T})\in{\rm{EQB}}[\Gamma]\ \}$ &  $\Box$*

Example 8** (Example 5 continued)**

Back to $\Gamma_{\ref{f:self}}=\{\operatorname{\mathbf{K}}a\to a\}$, remember its unique founded G91-world view was $[\emptyset]$. It is easy to see that $\mathcal{I}=({[\emptyset],\emptyset})\in{\rm{EQB}}[\Gamma_{\ref{f:self}}]$ because $({[\emptyset],\emptyset})\models\Gamma_{\ref{f:self}}$ and no smaller belief model can be obtained. Moreover, $[\emptyset]$ is an equilibrium world view of $\Gamma_{\ref{f:self}}$ since no other $T\not\in[\emptyset]$ satisfies $({[\emptyset],T})\in{\rm{EQB}}[\Gamma_{\ref{f:self}}]$. The only possibility is $({[\emptyset],\{a\}})$ but it fails because there is a smaller belief model $({[\emptyset],\emptyset,\{a\}})$ satisfying $\operatorname{\mathbf{K}}a\to a$. As for the other potential world view $[\{a\}]$, it is not in equilibrium: we already have $\mathcal{I}^{\prime}=({[\{a\}],\{a\}})\not\in{\rm{EQB}}[\Gamma_{\ref{f:self}}]$ because the smaller interpretation $\mathcal{I}^{\prime\prime}=({[\langle\emptyset,\{a\}\rangle],\{a\},\{a\}})$ also satisfies $\Gamma_{\ref{f:self}}$. In particular, note that $\mathcal{I}^{\prime\prime}\not\models\operatorname{\mathbf{K}}a$ and, thus, clearly satisfies $\operatorname{\mathbf{K}}a\to a$.   $\Box$

The logic induced by equilibrium world views is called Founded Autoepistemic Equilibrium Logic (FAEEL). A first important property is:

Theorem 2

FAEEL satisfies foundedness.  $\Box$

A second interesting feature is that equilibrium world views are also G91-world views though the converse may not be the case (as we just saw in Example 8). This holds, not only for programs, but in general for any theory:

Theorem 3

For any theory $\Gamma$, its equilibrium world views are also G91-world views of $\Gamma$.  $\Box$

In other words, FAEEL is strictly stronger than G91, something that, as we see next, is not the case in other approaches in the literature.

Example 9

The following program:

[TABLE]

has no G91-world views, but according to G11, K15, F15 and S17 has world view $[\{a,c\}]$. This example was also used in [1] to show that these semantics do not satisfy another property, called there epistemic splitting.  $\Box$

Example 10** (Example 6 continued)**

Take again program $\Pi_{\ref{theory:larger.set.of.worlds}}$ whose G91-world views were $\mathbb{W}=[\{a\},\{b\}]$ and $\mathbb{W}^{\prime}=[\{a,b\}]$. Since $\mathbb{W}^{\prime}$ is unfounded, it cannot be an equilibrium world view (Theorem 2), leaving $\mathbb{W}$ as the only candidate (Theorem 3). Let us check that this is in fact an equilibrium world view. First, note that $\mathcal{I}=({[\{a\},\{b\}],\{a\}})\in{\rm{EQB}}[\Pi_{\ref{theory:larger.set.of.worlds}}]$ because there is no model $\mathcal{I}^{\prime}$ of $\Pi_{\ref{theory:larger.set.of.worlds}}$ such that $\mathcal{I}^{\prime}\preceq\mathcal{I}$. In fact, it is easy to see that $({[\langle H_{1},\{a\}\rangle,\langle H_{2},\{b\}\rangle],H_{3},\{a\}})$ is not a model of the rule $a\vee b$ if $H_{i}=\emptyset$ for any $i\in\{1,2,3\}$. Symmetrically, we have that $\mathcal{I}^{\prime}=({[\{a\},\{b\}],\{b\}})\in{\rm{EQB}}[\Pi_{\ref{theory:larger.set.of.worlds}}]$ too. Finally, we have to check that no other $T\not\in[\{a\},\{b\}]$ can form an equilibrium belief model. For the case $T=\emptyset$, it is easy to check that $({[\{a\},\{b\}],\emptyset})$ does not satisfy $a\vee b$. For $T=\{a,b\}$, we have that $\mathcal{I}^{\prime\prime}=({[\{a\},\{b\}],\{a,b\}})\not\in{\rm{EQB}}[\Pi_{\ref{theory:larger.set.of.worlds}}]$ because, for instance, the smaller $\mathcal{I}^{\prime\prime\prime}=({[\{a\},\{b\}],\{a\},\{a,b\}})$ is a model of $\Pi_{\ref{theory:larger.set.of.worlds}}$.   $\Box$

Theorems 2 and 3 assert that any equilibrium world view is a founded G91-world view. The natural question is whether the opposite also holds. In Examples 8, 9 and 10 we did not find any counterexample, and this is in fact a general property, as stated below.

Main Theorem

Given any program $\Pi$, its equilibrium world views coincide with its founded G91-world views.  $\Box$

An interesting observation is that in all the original examples of epistemic specifications [4, 7] used by Gelfond to introduce G91, modal operators occurred in the scope of negation. Negated beliefs never incur unfoundedness, so this feature could not be spotted using this family of examples. In fact, under this syntactic restriction, FAEEL and G91 coincide.

Proposition 2

For any theory where all occurrences of $\operatorname{\mathbf{K}}$ are in the scope of negation, we have that the equilibrium world views and the G91-world views coincide.  $\Box$

Proposition 2 also holds for semantics [24, 25] that are conservative extensions of G91, as well as for G11. Apart from foundedness, [1] recently proposed other four properties for semantics of epistemic specifications. We analyse here three of them, omitting the so-called epistemic splitting due to lack of space.

supra-ASP holds when, for any objective theory $\Gamma$, either $\Gamma$ has a unique world view $\mathbb{W}=\text{\rm SM}[\Gamma]\neq\emptyset$ or $\text{\rm SM}[\Gamma]=\emptyset$ and $\Gamma$ has no world view. 2. 2.

supra-S5 holds when every world view $\mathbb{W}$ of a theory $\Gamma$ is also an S5-model of $\Gamma$ (that is, $\mathbb{W}\models\Gamma$). 3. 3.

subjective constraint monotonicity holds when, for any theory $\Gamma$ and any subjective constraint $\bot\leftarrow\varphi$, we have that $\mathbb{W}$ is a world view of $\Gamma\cup\{\bot\leftarrow\varphi\}$ iff both $\mathbb{W}$ is a world view of $\Gamma$ and $\mathbb{W}$ is not an S5-model of $\varphi$.

Proposition 3

FAEEL satisfies supra-ASP, supra-S5 and subjective constraint monotonicity.  $\Box$

All semantics discussed in this paper satisfy the above first two properties but most of them fail for subjective constraint monotonicity, as first discussed in [10]. In fact, a variation of Example 9 can be used to show that K15, F15 and S17 do not satisfy this property.

Example 11** (Example 9 continued)**

Suppose we remove the constraint (last rule) from $\Pi_{\ref{prg:nog91}}$ getting the program $\Pi_{\ref{prg:nog91b}}=\{a\vee b\,,\,c\leftarrow\operatorname{\mathbf{K}}a\}$. All semantics, including G91 and FAEEL, agree that $\Pi_{\ref{prg:nog91b}}$ has a unique world view $[\{a\},\{b\}]$. Suppose we add now a subjective constraint $\Pi_{5}=\Pi_{\ref{prg:nog91b}}\cup\{\bot\leftarrow\neg\!\operatorname{\mathbf{K}}c\}$. This addition leaves G91 and FAEEL without world views (due to subjective constraint monotonicity) the same happens for G11, but not for K15, F15 and S17, which provide a new world view $[\{a,c\}]$ not obtained before adding the subjective constraint.  $\Box$

Tables 1 and 2 show a list of examples taken from Table 4 in [2] and their world views according to different semantics.

6 Conclusions

In order to characterise self-supported world-views, already present in Gelfond’s 1991 semantics [4] (G91), we have extended the definition of unfounded sets from standard logic programs to epistemic specifications. As a result, we proposed the foundedness property for epistemic semantics, which is not satisfied by other approaches in the literature. Our main contribution has been the definition of a new semantics, based on the so-called Founded Autoepistemic Equilibrium Logic (FAEEL), that satisfies foundedness. This semantics actually covers the syntax of any arbitrary modal theory and is a combination of Equilibrium Logic and Autoepistemic Logic. As a main result, we were able to prove that, for the syntax of epistemic specifications, FAEEL world views coincide with the set of G91 world views that are founded. We showed how this semantics behaves on a set of common examples in the literature and proved that it satisfies other three basic properties: all world views are S5 models (supra-S5); standard programs have (at most) a unique world view containing all the stable models (supra-ASP); and subjective constraints just remove world views (monotonicity). FAEEL also satisfies the property of epistemic splitting as proposed in [1], but we leave the proof and discussion for future work, together with a formal comparison with other approaches.

Appendix A Proof of Proposition 1

• Proof of Proposition 1.

Just note that, for atomic $a$, we have that $\langle\mathbb{W},H,T\rangle\models a$ iff $a\in H\subseteq T$ which implies that $\langle\mathbb{W}^{t},T\rangle\models a$. The rest of the proof follows by induction in the structure of $\varphi$.      $\Box$

Appendix B Proof of Theorem 2

The proof of Theorem 2 rely on the definition of S5-equilibrium models. We first show that S5-equilibrium models are unfounded-free and then that autoepistemic world views are S5-equilibrium models. Then, we obtain that autoepistemic world views are unfounded-free as a corollary. We start by defining S5-interpretations $\mathbb{W}$ as sets of HT-interpretations. An S5-interpretations $\mathbb{W}$ is said to be total iff it satisfies that every HT-interpretation $\langle H,T\rangle\in\mathbb{W}$ is total, that is, $H=T$. We say that an S5-interpretations $\mathbb{W}$ is a $\text{S5}_{\text{\tiny HT}}$-model of a formula $\varphi$ iff $\langle\mathbb{W},H,T\rangle\models\varphi$ for every $\langle H,T\rangle\in\mathbb{W}$.

Definition 8

Given S5-interpretations $\mathbb{W}_{1}$ and $\mathbb{W}_{2}$, we write $\mathbb{W}_{1}\preceq\mathbb{W}_{2}$ iff the following two condition hold:

for every $\langle H_{2},T\rangle\in\mathbb{W}_{2}$, there is some $\langle H_{1},T\rangle\in\mathbb{W}_{1}$, with $H_{1}\subseteq H_{2}$. 2. 2.

for every $\langle H_{1},T\rangle\in\mathbb{W}_{1}$, there is some $\langle H_{2},T\rangle\in\mathbb{W}_{2}$, with $H_{1}\subseteq H_{2}$.

As usual, we write $\mathbb{W}_{1}\prec\mathbb{W}_{2}$ iff $\mathbb{W}_{1}\preceq\mathbb{W}_{2}$ and $\mathbb{W}_{1}\neq\mathbb{W}_{2}$.  $\Box$

Definition 9

A total S5-interpretation $\mathbb{W}$ is said to be a S5-equilibrium model of some theory $\Gamma$ iff $\mathbb{W}$ is a $\text{S5}_{\text{\tiny HT}}$-model of $\Gamma$ and there is no other $\text{S5}_{\text{\tiny HT}}$-model $\mathbb{W}^{\prime}$ of $\Gamma$ such that $\mathbb{W}^{\prime}\prec\mathbb{W}$.  $\Box$

S5-equilibrium model are similar to epistemic equilibrium model in the sense of [2], being the major difference that, in our approach, different evaluations in the here world can be used to minimise the same evaluation in the there world. As a result, we conjeture that every S5-equilibrium model is also an epistemic equilibrium model in the sense of [2]. On the other hand, the converse does not hold in general. For instance, if we take the program $\Pi_{\ref{theory:larger.set.of.worlds}}$ from Example 6, we have that $[\{a\},\{b\}]$ is an epistemic equilibrium model in the sense of [2], but not an S5-equilibrium model in our approach. This shows that epistemic equilibrium model in the sense of [2] are not unfounded-free (in the same way that world views or autoepistemic equilibrium model in this approach are not unfounded-free). The following result shows that S5-equilibrium model are, in fact, unfounded-free.

Theorem 4

Any S5-equilibrium model of any program $\Pi$ is unfounded-free.  $\Box$

Proof B.5**.**

Let $\mathbb{W}$ be some S5-equilibrium model of some program $\Pi$ and suppose, for the sake of contradiction, that it is not unfounded-free. Then, there is a unfounded-set $\mathbb{S}$ for $\Pi$ with respect to $\mathbb{W}$ such that, for every $\langle X,I\rangle\in\mathbb{S}$, we have $I\in\mathbb{W}$ and $X\cap I\neq\emptyset$. Let {IEEEeqnarray}l ?C? C l C l W’ &= $\{\ \langle I,I\rangle\ |\ \langle I,I\rangle\in\mathbb{W}\text{ and no }\langle X,I\rangle\notin\mathbb{S}\ \}$

∪ $\{\ \langle I\setminus X,I\rangle\ |\ \langle I,I\rangle\in\mathbb{W}\text{ and }\langle X,I\rangle\in\mathbb{S}\ \}$

Since $\mathbb{S}$ is non-empty and $X\cap I\neq\emptyset$ for all $\langle X,I\rangle\in\mathbb{S}$, we have that $\mathbb{W}^{\prime}\prec\mathbb{W}$ and, since $\mathbb{W}$ is an S5-equilibrium model of $\Pi$, it must be that $\mathbb{W}^{\prime}$ is not an $\text{S5}_{\text{\tiny HT}}$-model of $\Pi$. Hence, there is some rule $r\in\Pi$ such that $\mathbb{W}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $r$ while $\mathbb{W}^{\prime}$ is not. Besides, the latter implies that there is some $\langle H,T\rangle\in\mathbb{W}^{\prime}$ such that $\langle\mathbb{W}^{\prime},H,T\rangle\not\models r$ and, thus, that one of following conditions must hold:*

$\langle\mathbb{W}^{\prime},H,T\rangle\models\bigwedge\mathit{Body}(r)$* and $\langle\mathbb{W}^{\prime},H,T\rangle\not\models\bigvee\mathit{Head}(r)$, or* 2. 2.

$\langle\mathbb{W},T,T\rangle\models\bigwedge\mathit{Body}(r)$* and $\langle\mathbb{W},T,T\rangle\not\models\bigvee\mathit{Head}(r)$.*

Note that the latter is a contradiction with the fact that $\mathbb{W}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $r$ and, thus, the former must hold. Furthermore, $\langle\mathbb{W}^{\prime},H,T\rangle\models\bigwedge\mathit{Body}(r)$ implies $\langle\mathbb{W},T\rangle\models\bigwedge\mathit{Body}(r)$ and, since $\mathbb{W}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $r$, that $\langle\mathbb{W},T\rangle\models\bigvee\mathit{Head}(r)$. Hence, $\mathit{Head}(r)\cap H=\emptyset$ and there is an atom $a\in\mathit{Head}(r)$ such that $a\in T\setminus H$. By construction, this implies that, since $\langle X,T\rangle\in\mathbb{S}$ with $X=T\setminus H$ and, thus, one of the following conditions must hold:

$({W,T})\not\models\bigwedge\mathit{Body}(r)$, 2. 2.

$\mathit{Body}^{+}_{ob}(r)\cap X\neq\emptyset$, or 3. 3.

$(\mathit{Head}(r)\setminus X)\cap T\neq\emptyset$, or 4. 4.

$\mathit{Body}^{+}_{sub}(r)\cap Y\neq\emptyset$.

*The first condition cannot hold because we have that $\langle\mathbb{W},T\rangle\models\bigwedge\mathit{Body}(r)$. Furthermore, $X=T\setminus H$, we have that

$(\mathit{Head}(r)\setminus X)\cap T\neq\emptyset$ holds

iff $(\mathit{Head}(r)\setminus(T\setminus H))\cap T\neq\emptyset$

iff $(\mathit{Head}(r)\cap\overline{(T\cap\overline{H}))}\cap T\neq\emptyset$

iff $(\mathit{Head}(r)\cap(\overline{T}\cup H))\cap T\neq\emptyset$

iff $\mathit{Head}(r)\cap\overline{T}\cap T\neq\emptyset$ or $\mathit{Head}(r)\cap H\cap T\neq\emptyset$

iff $\mathit{Head}(r)\cap H\neq\emptyset$

which does not hold. Hence, the forth condition cannot hold either.*

Assume now that $b\in\mathit{Body}^{+}_{ob}(r)\cap X\neq\emptyset$. Then, $\langle\mathbb{W}^{\prime},H,T\rangle\not\models b$ and, thus, we have that $\langle\mathbb{W}^{\prime},H,T\rangle\not\models\bigwedge\mathit{Body}(r)$ which is a contradiction with 1. Therefore, it must be that $\mathit{Body}^{+}_{sub}(r)\cap Y\neq\emptyset$ holds. Pick some atom $b\in\mathit{Body}^{+}_{sub}(r)\cap Y$. But then, there is some $\langle X^{\prime},T^{\prime}\rangle\in\mathbb{S}$ such that $b\in X^{\prime}$ and $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}$ with $X^{\prime}=T^{\prime}\setminus H^{\prime}$. This implies that $\langle\mathbb{W}^{\prime},H^{\prime},T^{\prime}\rangle\not\models b$ and, thus, that $\langle\mathbb{W}^{\prime},H,T\rangle\not\models\operatorname{\mathbf{K}}b$ which is a contradiction with the fact that $\langle\mathbb{W}^{\prime},H,T\rangle\models\bigwedge\mathit{Body}(r)$. Consequently, $\mathbb{W}$ must be unfounded-free.∎

Observation 1

Let $\Gamma$ be a theory and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be a model of $\Gamma$. Then, $\mathbb{W}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $\Gamma$.∎

Proposition B.6**.**

Let $\Gamma$ be a theory and $\mathbb{W}$ be an S5-interpretation such that $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$. Then, $\mathbb{W}$ is an S5-equilibrium model of $\Gamma$.

Proof B.7**.**

First note that, since $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$, it follows that $\langle\mathbb{W},T\rangle$ is a model of $\Gamma$ for every $T\in\mathbb{W}$ and, thus, that $\langle\mathbb{W},T\rangle\models\varphi$ for every formula $\varphi\in\Gamma$. In its turn, this implies that $\mathbb{W}$ is an S5-model of $\Gamma$. Suppose now, for the sake of contradiction, that $\mathbb{W}$ is not an S5-equilibrium model of $\Gamma$ and, thus, that there is some $\text{S5}_{\text{\tiny HT}}$-model $\mathbb{W}^{\prime}$ of $\Gamma$ such that $\mathbb{W}^{\prime}\prec\mathbb{W}$. Hence, there is $\langle H,T\rangle\in\mathbb{W}^{\prime}$ such that $H\subset T$. Furthermore, since $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$ it follows that $\langle\mathbb{W}^{\prime},H,T\rangle$ is not a model of $\Gamma$. Hence, there is a formula $\varphi\in\Gamma$ and $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}^{\prime}\cup\{\langle H,T\rangle\}=\mathbb{W}^{\prime}$ such that $\langle\mathbb{W}^{\prime},H^{\prime},T^{\prime}\rangle\not\models\varphi$. This implies that $\mathbb{W}^{\prime}$ is not an $\text{S5}_{\text{\tiny HT}}$-model of $\varphi$ which is a contradiction with the fact that $\mathbb{W}^{\prime}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $\Gamma$. Consequently, $\mathbb{W}$ must be an S5-equilibrium model of $\Gamma$.∎

Note that, in general, the converse of Proposition B.6 does not hold. For instance, $[\{a\}]$ is the unique S5-equilibrium model of the the theory $\{\operatorname{\mathbf{K}}a\}$ while $({[\{a\}],\{a\}})$ is not a equilibrium model of it.

Corollary B.8**.**

Let $\mathbb{W}$ be an autoepistemic world view of some theory $\Gamma$. Then, it satisfies the following two conditions:

$\mathbb{W}$* is an S5-equilibrium model, and* 2. 2.

there is no propositional interpretation $T$ such that model $\langle\mathbb{W},T\rangle$ is an equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$.∎

Note that, in general, the converse of Corollary B.8 does not hold. For instance, theory $\{\operatorname{\mathbf{K}}a,\neg\neg a\}$ has no autoepistemic world view while we have that $[\{a\}]$ is an S5-equilibrium model and $({[\{a\}],\emptyset})$ is not a equilibrium model of it. To see that $[\{a\}]$ is not autoepistemic world view, note that $({[\{a\}],\{a\}})$ is not a equilibrium model of $\{\operatorname{\mathbf{K}}a,\neg\neg a\}$.

• Proof of Theorem 2.

From Corollary B.8, we have that $\mathbb{W}$ is an S5-equilibrium model and, from Theorem 4, this implies that $\mathbb{W}$ is unfounded-free.    ∎

Appendix C Proof of Theorem 3

The proof of Theorem 3 rely on the definition of weak autoepistemic world views. We first show that every autoepistemic world view is also a weak autoepistemic world view and then that weak autoepistemic world views coincide with G91-world views. Then, we obtain that autoepistemic world views are G91-world views as a corollary. Let us start by defining semi-total interpretations. We say that an interpretation $\langle\mathbb{W},H,T\rangle$ is semi-total iff every HT-interpretation $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}$ is total, that is, $H^{\prime}=T^{\prime}$. It is easy to see that, every total interpretation is semi-total but not vice-versa.

Definition C.9**.**

A total interpretation $\mathcal{I}$ is said to be a weak equilibrium model of some theory $\Gamma$ iff $\mathcal{I}$ is a model of $\Gamma$ and there is no other semi-total model $\mathcal{I}^{\prime}$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$.∎

Note that every equilibrium model is also a weak equilibrium model, but not vice-versa. For instance, $({[\{a\}],\{a\}})$ is a weak equilibrium model of $\{a\leftarrow\operatorname{\mathbf{K}}a\}$ but not a equilibrium model.

Definition C.10**.**

A S5-interpretation $\mathbb{W}$ is called a weak autoepistemic world view of $\Gamma$ iff it satisfies the following two conditions:

$({\mathbb{W},T})$* is a weak equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$, and* 2. 2.

there not exists any propositional interpretation $T$ such that $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$.∎

Proposition C.11**.**

Every autoepistemic world view is also a weak autoepistemic world view.∎

Proof C.12**.**

Since every equilibrium model is also a weak equilibrium model, it only remains to be shown that if $\mathbb{W}$ is an autoepistemic world view then

1. there not exists any propositional interpretation $T$ such that $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$.

Suppose, for the sake of contradiction, that there is some propositional interpretation $T$ such that $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$. Since $\mathbb{W}$ is an autoepistemic world view, this implies that $\langle\mathbb{W},T\rangle$ is not a equilibrium model of $\Gamma$ and, thus, that there is some non-semi-total model $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H,T\rangle$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$. Hence, there is some $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}^{\prime}$ such that $H^{\prime}\subset T^{\prime}$. Let $\mathcal{I}^{\prime\prime}=\langle\mathbb{W}^{\prime},H^{\prime},T^{\prime}\rangle$. Then, we have that $\mathcal{I}^{\prime\prime}\prec\langle\mathbb{W},T^{\prime}\rangle$ and, since $\mathbb{W}$ is an autoepistemic world view of $\Gamma$ and $T\in\mathbb{W}$, we have that $\langle\mathbb{W},T^{\prime}\rangle$ is a equilibrium model of $\Gamma$. These two facts together imply that $\mathcal{I}^{\prime\prime}$ is not a model of $\Gamma$. Hence, there is a formula $\varphi\in\Gamma$ such that $\mathcal{I}^{\prime\prime}$ is not a model of $\varphi$ and, thus, there is $\langle H^{\prime\prime},T^{\prime\prime}\rangle\in\mathbb{W}^{\prime}\cup\{\langle H^{\prime},T^{\prime}\rangle\}$ such that $\langle\mathbb{W}^{\prime},H^{\prime\prime},T^{\prime\prime}\rangle\not\models\varphi$. On the other hand, since $\mathcal{I}^{\prime}$ is a model of $\Gamma$ , it follows that $\langle\mathbb{W}^{\prime},H^{\prime\prime\prime},T^{\prime\prime\prime}\rangle\not\models\varphi$ for every $\langle H^{\prime\prime\prime},T^{\prime\prime\prime}\rangle\in\mathbb{W}^{\prime}\cup\{\langle H,T\rangle\}$. Hence, it follows that $H^{\prime\prime}=H^{\prime}$ and $T^{\prime\prime}=T^{\prime}$ and that $\langle\mathbb{W}^{\prime},H^{\prime},T^{\prime}\rangle\not\models\varphi$. However, since $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}^{\prime}$, this implies that $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H,T\rangle\not\models\varphi$, which is a contradiction with the fact that $\mathcal{I}^{\prime}$ is a model of $\Gamma$. Consequently, $\mathbb{W}$ is a weak autoepistemic world view.∎

Lemma C.13**.**

Let $\Gamma$ be a formula and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be a semi-total interpretation. Then, $\mathcal{I}$ is a model of $\varphi$ iff $\mathcal{I}$ is a model of $\varphi^{\mathbb{W}}$.∎

Proof C.14**.**

Assume that $\varphi=\operatorname{\mathbf{K}}\psi$. Then, we have that $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\varphi$ if and only if $\langle\mathbb{W},T^{\prime\prime},T^{\prime\prime}\rangle\models\psi$ for every $\langle T^{\prime\prime},T^{\prime\prime}\rangle\in\mathbb{W}$ iff $\mathbb{W}$ is a S5-model of $\varphi$ iff $\varphi^{\mathbb{W}}=\top$ iff $\mathcal{I}\models\varphi^{\mathbb{W}}$. Then, by induction in the structure of $\varphi$, we get that $\mathcal{I}\models\varphi$ iff $\mathcal{I}\models\varphi^{\mathbb{W}}$. Finally, we have that $\mathcal{I}$ is a model of $\varphi$ iff $\mathcal{I}\models\varphi$ and $\langle\mathbb{W},T^{\prime},T^{\prime}\rangle\models\varphi$ for every $\langle T^{\prime},T^{\prime}\rangle\in\mathbb{W}$ iff $\mathcal{I}\models\varphi^{\mathbb{W}}$ and $\langle\mathbb{W},T^{\prime},T^{\prime}\rangle\models\varphi^{\mathbb{W}}$ for every $\langle T^{\prime},T^{\prime}\rangle\in\mathbb{W}$ iff $\mathcal{I}$ is a model of $\varphi^{\mathbb{W}}$.

Lemma C.15**.**

Let $\Gamma$ be a propositional theory and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be some interpretation. Then, $\mathcal{I}$ is a model of $\Gamma$ iff $\langle H^{\prime},T^{\prime}\rangle$ is a HT-model of $\Gamma$ for every HT-interpretation $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$.∎

Proof C.16**.**

By definition, we have that $\mathcal{I}$ is a model of $\Gamma$ iff $\mathcal{I}$ is a model of $\varphi$ for all $\varphi\in\Gamma$. Furthermore, $\mathcal{I}$ is a model of $\varphi$ iff $\mathcal{I}\models\varphi$ and $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\varphi$ for every $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}$ iff $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\varphi$ for every HT-interpretation $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$. Finally, since $\varphi$ is a propositional formula, we have that $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\varphi$ iff $\langle H^{\prime},T^{\prime}\rangle\models\varphi$. Hence, $\mathcal{I}$ is a model of $\Gamma$ iff $\langle H^{\prime},T^{\prime}\rangle$ is a HT-model of $\Gamma$ for every HT-interpretation $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$.∎

Lemma C.17**.**

Let $\Gamma$ be a propositional theory and $\mathcal{I}=\langle\mathbb{W},T\rangle$ be some total interpretation. Then, $\mathcal{I}$ is a equilibrium model of $\Gamma$ iff $T^{\prime}$ is an equilibrium model of $\Gamma$ for every $T^{\prime}\in\mathbb{W}\cup\{T\}$.∎

Proof C.18**.**

First note that, since $\Gamma$ is propositional, $\mathcal{I}$ is a model of $\Gamma$ iff $T^{\prime}$ is an model of $\Gamma$ for every $T^{\prime}\in\mathbb{W}\cup\{T\}$. Hence, we have that $\mathcal{I}$ is a equilibrium model of $\Gamma$ iff there is not model $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H,T\rangle$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$.

Suppose, for the sake of contradiction, that there is some $T^{\prime}\in\mathbb{W}\cup\{T\}$ which is not an equilibrium model of $\Gamma$. Then, there is $\langle H^{\prime},T^{\prime}\rangle\models\Gamma$ such that $H^{\prime}\subset T^{\prime}$. Let $\mathcal{I}^{\prime}=\langle\mathbb{W},H^{\prime},T^{\prime}\rangle$ if $T^{\prime}=T$ and $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},T^{\prime},T^{\prime}\rangle$ with $\mathbb{W}^{\prime}=\{\langle H^{\prime},T^{\prime}\rangle\}\cup\mathbb{W}$ otherwise. Then, $\mathcal{I}^{\prime}\prec\mathcal{I}$ and, from Lemma C.17, we have that $\mathcal{I}^{\prime}$ is a model of $\Gamma$ which is a contradiction. Hence, $T^{\prime}$ must be an equilibrium model of $\Gamma$ for every $T^{\prime}\in\mathbb{W}\cup\{T\}$. The other way around. Assume that $T^{\prime}$ is an equilibrium model of $\Gamma$ for every $T^{\prime}\in\mathbb{W}\cup\{T\}$ and suppose, for the sake of contradiction, that $\mathcal{I}$ is not a equilibrium model of $\Gamma$. Then, there is some model $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H,T\rangle$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$. Then, from Lemma C.17, we have that $\langle H^{\prime},T^{\prime}\rangle\models\Gamma$ for every $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$. This implies that $T^{\prime}$ is not an equilibrium model of $\Gamma$ which is a contradiction. Consequently, $\mathcal{I}$ must be a equilibrium model of $\Gamma$.∎

Theorem C.19**.**

Given a theory $\Gamma$ and some S5-interpretation $\mathbb{W}$, we have that $\mathbb{W}$ is a weak autoepistemic world view of $\Gamma$ iff $\mathbb{W}$ is a G91-world view of $\Gamma$.∎

Proof C.20**.**

It is easy to see Definition C.10 can be rewritten as the following fixpoint equation:

[TABLE]

where ${\rm{WEQ}}[\Gamma]$ denotes the set of all weak equilibrium models of $\Gamma$. Furthermore, from Lemmas C.13 and C.17, we have that $\langle\mathbb{W},T\rangle\in{\rm{WEQ}}[\Gamma]$ iff $\langle\mathbb{W},T\rangle\in{\rm{WEQ}}[\Gamma^{\mathbb{W}}]$ iff $\mathbb{W}\cup\{T\}\subseteq{\rm{EQ}}[\Gamma^{\mathbb{W}}]$ and, therefore, the above can be rewriting as

[TABLE]

which holds iff $\mathbb{W}={\rm{EQ}}[\Gamma^{\mathbb{W}}]$. That is, iff $\mathbb{W}$ is a G91-world view of $\Gamma$.∎

Note that weak autoepistemic world views are very similar to epistemic views as defined in [25] and, in fact, we conjecture that they coincide for any theory without nested implications. On the other hand, the following example shows that this does not hold in general:

Example C.21**.**

Consider the singleton theory $\Gamma=\{\neg\neg a\wedge\operatorname{\mathbf{K}}\varphi\to a\}$ with $\varphi$ the following formula $\varphi=\neg\neg a\to a$. Then, $\mathbb{W}=[\emptyset,\{a\}]$ is both a G91 and autoepistemic world view of $\Gamma$, but not an epistemic view. To see that $\mathbb{W}$ is both a G91-world view of $\Gamma$, note that $\Gamma^{\mathbb{W}}=\{\neg\neg a\wedge\top\to a\}\equiv\{\neg\neg a\to a\}$ which has two stable models: $\emptyset$ and $\{a\}$. Hence, $\mathbb{W}$ is a G91-world view of $\Gamma$. Furthermore, from Theorem C.19 this implies that $\mathbb{W}$ is also an autoepistemic world view. On the other hand, $\mathbb{W}$ is not an epistemic view because $\langle\mathbb{W},\emptyset,\{a\}\rangle$ is a model of $\Gamma$ in the sense of [25]. Note that $\langle\mathbb{W},\emptyset,\{a\}\rangle\not\models\varphi$ and that both $\emptyset$ and $\{a\}$ belong to $\mathbb{W}$. This implies that $\langle\mathbb{W},\emptyset,\{a\}\rangle\not\models\operatorname{\mathbf{K}}\varphi$ and, thus, that $\langle\mathbb{W},\emptyset,\{a\}\rangle$ is a model of $\Gamma$. On the other hand, in our logic $\langle\mathbb{W},\emptyset,\{a\}\rangle\not\models\varphi$ does not imply $\langle\mathbb{W},\emptyset,\{a\}\rangle\not\models\operatorname{\mathbf{K}}\varphi$. In fact $\langle\mathbb{W},\emptyset,\{a\}\rangle\models\operatorname{\mathbf{K}}\varphi$ holds because both $\langle\mathbb{W},\emptyset,\emptyset\rangle\models\varphi$ and $\langle\mathbb{W},\{a\},\{a\}\rangle\models\varphi$ hold. ∎

This example shows that epistemic views [25] are different from G91-world views as defined in [24] and from ours weak autoepistemic world views.

• Proof of Theorem 3.

From Proposition C.11, we have that every autoepistemic world view is also a weak autoepistemic world view and, from Theorem C.19, this implies that every autoepistemic world view is also a G91-world view.    ∎

Appendix D Proof of the Main Theorem

First note that, by taking together Theorems 2 and 3, we immediately obtain the following result:

Corollary D.22**.**

Any autoepistemic world view $\mathbb{W}$ of any program $\Pi$ is also an unfounded-free G91-world view.∎

The converse of Corollary D.22 is proved in two steps. We first prove that every unfounded-free S5-model is also an S5-equilibrium model and then that every S5-equilibrium model which is also a weak autoepistemic world view is an autoepistemic world view. As a Corollary, we obtain that every unfounded-free G91-world view is also an autoepistemic world view.

Theorem D.23**.**

Given any program $\Pi$ and some S5-interpretation $\mathbb{W}$, we have that $\mathbb{W}$ is an S5-equilibrium model iff $\mathbb{W}$ is an unfounded-free S5-model.∎

Proof D.24**.**

First note that from Theorem 4, we have that any S5-equilibrium model of any program $\Pi$ is unfounded-free. Suppose now, for the sake of contradiction, that $\mathbb{W}$ is an S5-model of $\Pi$ but not an S5-equilibrium model. Then, there is some $\text{S5}_{\text{\tiny HT}}$-model $\mathbb{W}^{\prime}$ of $\Pi$ such that $\mathbb{W}^{\prime}\prec\mathbb{W}$. Let us define

[TABLE]

Then, is clear that, for every $\langle X,I\rangle\in\mathbb{S}$ we have $I\in\mathbb{W}^{\prime}$ and $X\cap I\neq\emptyset$. Hence, since $\mathbb{W}$ is unfounded-free, it follows that $\mathbb{S}$ cannot be an unfounded-witness for $\Pi$ w.r.t. $\mathbb{W}^{\prime}$. Besides, since $\mathbb{W}^{\prime}\prec\mathbb{W}$, we have that $\mathbb{S}\neq\emptyset$ and, thus, there must be some $\langle X,I\rangle\in\mathbb{S}$, atom $a\in X$ and rule $r\in\Pi$ with $a\in\mathit{Head}(r)$ satisfying all the following conditions:

$({\mathbb{W},I})\models\bigwedge\mathit{Body}(r)$, and 2. 2.

$\mathit{Body}^{+}_{ob}(r)\cap X=\emptyset$, and 3. 3.

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

$\mathit{Body}^{+}_{sub}(r)\cap Y=\emptyset$, and

Furthermore, since $\mathbb{W}^{\prime}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $\Pi$, we have that $({\mathbb{W}^{\prime},H,I})\models r$ for every $r\in\Pi$ and with $H=I\setminus X$ and that one of the following must hold:

$({\mathbb{W},I})\not\models\bigwedge\mathit{Body}(r)$, or 2. 6.

$({\mathbb{W}^{\prime},H,I})\models\bigvee\mathit{Head}(r)$, or 3. 7.

$({\mathbb{W}^{\prime},H,I})\not\models\bigwedge\mathit{Body}(r)$* and $({\mathbb{W},I})\models\bigvee\mathit{Head}(r)$.*

*Clearly, (5) is in contradiction with (1) and, thus, either (6) or (7) must hold. Note also that (3) implies that $\mathit{Head}(r)\cap H=\emptyset$ and, thus, (6) cannot hold either. In more detail, we have that

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

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

iff $(\mathit{Head}(r)\cap\overline{(I\cap\overline{H}))}\cap I=\emptyset$

iff $(\mathit{Head}(r)\cap(\overline{I}\cup H))\cap I=\emptyset$

iff $\mathit{Head}(r)\cap\overline{I}\cap I=\emptyset$ and $\mathit{Head}(r)\cap H\cap I=\emptyset$

iff $\mathit{Head}(r)\cap H\cap I=\emptyset$

iff $\mathit{Head}(r)\cap H=\emptyset$

iff $({\mathbb{W}^{\prime},H,I})\not\models\bigvee\mathit{Head}(r)$ Hence, (7) must hold and, thus, there is some literal $L\in\mathit{Body}^{+}(r)$ such that $({\mathbb{W}^{\prime},H,I})\not\models L$. If $L\in\mathit{Body}^{obj}(r)$, then, we have that $L\notin H$. Besides, from condition 1, we have that $L\in I$ and, thus, $L\in I\setminus H=X$ which is a contradiction with condition 2. Otherwise, $L\in\mathit{Body}^{sub}(r)$ and we have that there is $\langle H^{\prime},I^{\prime}\rangle\in\mathbb{W}^{\prime}$ such that $a\notin H^{\prime}$ with $L=\operatorname{\mathbf{K}}a$. But then, $\langle X^{\prime},I^{\prime}\rangle\in\mathbb{S}$ with $X^{\prime}=I^{\prime}\setminus H^{\prime}$ and, thus, $a\in Y$ which is a contradiction with condition 4. Consequently, $\mathbb{W}$ is an S5-equilibrium model.∎*

Lemma D.25**.**

Let $\Gamma$ be a theory, $\mathbb{W}$ be an S5-equilibrium model of $\Gamma$ and $T\in\mathbb{W}$ be a propositional interpretation. If $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$, then $\langle\mathbb{W},T\rangle$ is also a equilibrium model of $\Gamma$.

Proof D.26**.**

Suppose that $\langle\mathbb{W},T\rangle$ is not a equilibrium model of $\Gamma$. Since $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$, we have that $({\mathbb{W},T})$ is model of $\Gamma$ and, thus, there must be some non-semi-total model $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H,T\rangle$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec({\mathbb{W},T})$. Hence, there is $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}^{\prime}$ with $H\subset T$. This implies that $\mathbb{W}^{\prime}\prec\mathbb{W}$ and, since $\mathbb{W}$ is an S5-equilibrium model of $\Gamma$, that $\mathbb{W}$ is not a $\text{S5}_{\text{\tiny HT}}$-model of $\Gamma$. Hence, $\mathbb{W}^{\prime}$ is not a $\text{S5}_{\text{\tiny HT}}$-model of $\Gamma$. This implies that there is some formula $\varphi\in\Gamma$ and HT-interpretation $\langle H^{\prime\prime},T^{\prime\prime}\rangle\in\mathbb{W}^{\prime}$ such that $\langle\mathbb{W}^{\prime},H^{\prime\prime},T^{\prime\prime}\rangle\not\models\varphi$. In its turn, this implies that $\mathcal{I}^{\prime}$ is not a model of $\Gamma$ which is a contradiction. Consequently, $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$.∎

Proposition D.27**.**

Given a theory $\Gamma$ and an S5-interpretation $\mathbb{W}$, we have that $\mathbb{W}$ is an autoepistemic world view iff $\mathbb{W}$ is both an S5-equilibrium model and a weak autoepistemic world view of $\Gamma$.∎

Proof D.28**.**

First note that from Corollary B.8 and Proposition C.11, we have that every autoepistemic world view is both an S5-equilibrium model and a weak autoepistemic world view of $\Gamma$. The other way around. Since $\mathbb{W}$ is a weak autoepistemic equilibrium model of $\Gamma$, we have that $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$ which, from Lemma LABEL:lem:epistemic:prop:decomposition, implies that $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$. Hence, it only remains to be shown that the following condition hold:

1. there is no propositional interpretation $T$ such that model $\langle\mathbb{W},T\rangle$ is an equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$.

Suppose, for the sake of contradiction, that there is some propositional interpretation $T$ such that model $\langle\mathbb{W},T\rangle$ is an equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$. First, this implies that $\langle\mathbb{W},T\rangle$ is an D45-model of $\Gamma$. Then, since $\mathbb{W}$ is a weak autoepistemic equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$, it follows that $\langle\mathbb{W},T\rangle$ cannot be a weak equilibrium model of $\Gamma$ and, thus, there is some semi-total model $\mathcal{J}$ is a model of $\Gamma$ such that $\mathcal{J}\prec\langle\mathbb{W},T\rangle$. But every semi-total model is also a model, so this is a contradiction with the fact that $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$. Consequently, $\mathbb{W}$ must be an autoepistemic world view of $\Gamma$.∎

Corollary D.29**.**

Given any program $\Pi$ and some S5-interpretation $\mathbb{W}$, we have that $\mathbb{W}$ is an autoepistemic world view of $\Pi$ iff $\mathbb{W}$ is an unfounded-free weak autoepistemic world view.∎

Proof D.30**.**

From Proposition D.27 and Theorem D.23, we have that $\mathbb{W}$ is an autoepistemic world view iff $\mathbb{W}$ is both an S5-equilibrium model and a weak autoepistemic world view iff $\mathbb{W}$ is an unfounded-free S5-model and a weak autoepistemic world view. Finally, it is easy to see that every weak autoepistemic world view is also an S5-model and, thus, we get that any S5-interpretation is an autoepistemic world view iff is an unfounded-free weak autoepistemic world view.∎

• Proof of the Main Theorem.

Let $\mathbb{W}$ be any S5-interpretation. Then, from Corollary D.29, we have that $\mathbb{W}$ is an autoepistemic world view iff $\mathbb{W}$ is an unfounded-free weak autoepistemic world view. Furthermore, from Theorem C.19, we have that $\mathbb{W}$ is a weak autoepistemic world view iff $\mathbb{W}$ is a G91-world view. Taking these two facts together, we get that $\mathbb{W}$ is an autoepistemic world view iff $\mathbb{W}$ is an unfounded-free G91-world view.    ∎

Appendix E Proofs of Propositions 2 and 3

Proposition E.31**.**

Let $\varphi$ be a formula and let $\langle\mathbb{W},H,T\rangle$ be an interpretation. Then, $\langle\mathbb{W},H,T\rangle\models\neg\varphi$ iff $\langle\mathbb{W}^{t},T,T\rangle\not\models\varphi$ iff $\langle\mathbb{W}^{t},T,T\rangle\models\neg\varphi$.∎

Proof E.32**.**

By definition, we have that $\langle\mathbb{W}^{t},T,T\rangle\models\neg\varphi$ iff $\langle\mathbb{W}^{t},T,T\rangle\models\varphi\to\bot$ iff $\langle\mathbb{W}^{t},T,T\rangle\not\models\varphi$. Furthermore, by definition, we have that $\langle\mathbb{W},H,T\rangle\models\neg\varphi$ iff both $\langle\mathbb{W},H,T\rangle\not\models\varphi$ and $\langle\mathbb{W},T,T\rangle\not\models\varphi$. Finally, since Proposition LABEL:prop:pers, we have that $\langle\mathbb{W},H,T\rangle\models\varphi$ implies $\langle\mathbb{W},T,T\rangle\models\varphi$ we get that $\langle\mathbb{W},H,T\rangle\models\neg\varphi$ iff $\langle\mathbb{W},T,T\rangle\not\models\varphi$.∎

Lemma E.33**.**

Let $\varphi$ be a formula where all occurrences of $\operatorname{\mathbf{K}}$ are in the scope of negation and let $\langle\mathbb{W},H,T\rangle$ be an interpretation. Then, $\langle\mathbb{W},H,T\rangle\models\varphi$ iff $\langle\mathbb{W}^{t},H,T\rangle\models\varphi$.∎

Proof E.34**.**

In case that $\varphi\in\mathcal{AT}$ is an atom, we have that $\langle\mathbb{W},H,T\rangle\models\varphi$ iff $\varphi\in H$ iff $\langle\mathbb{W}^{t},H,T\rangle\models\varphi$. In case $\varphi=\neg\psi$, from Proposition E.31, we have that $\langle\mathbb{W},H,T\rangle\models\varphi$ iff $\langle\mathbb{W}^{t},T,T\rangle\models\varphi$ iff $\langle\mathbb{W}^{t},H,T\rangle\models\varphi$. Otherwise, the proof follows by induction in the structure of the formula.∎

Lemma E.35**.**

Let $\Gamma$ be a formula where all occurrences of $\operatorname{\mathbf{K}}$ are in the scope of negation and let $\mathbb{W}$ be a weak autoepistemic world view. Then, $\mathbb{W}$ is also an autoepistemic world view.∎

Proof E.36**.**

Since $\mathbb{W}$ be a weak autoepistemic world view we have that

$({\mathbb{W},T})$* is a weak equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$, and* 2. 2.

there not exists any propositional interpretation $T$ such that $\langle\mathbb{W},T\rangle$ is a weak equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$.

First note that condition 2 immediately implies that there not exists any propositional interpretation $T$ such that $\langle\mathbb{W},T\rangle$ is a equilibrium model of $\Gamma$ and $T\notin\mathbb{W}$. Suppose now, for the sake of contradiction, that

1. there is $T\in\mathbb{W}$ such that $({\mathbb{W},T})$ is a not equilibrium model of $\Gamma$.

Hence, there is a non-semi-total model $\mathcal{I}=({\mathbb{W}^{\prime},H,T})$ of $\Gamma$ s.t. $\mathcal{I}\prec({\mathbb{W},T})$. Furthermore, since $\mathcal{I}$ is a model of $\Gamma$, we have that $({\mathbb{W}^{\prime},H^{\prime},T^{\prime}})\models\varphi$ all $\varphi\in\Gamma$ and all $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$ which, from Lemma E.33 and the fact that all occurrences of $\operatorname{\mathbf{K}}$ in $\varphi$ are in the scope of negation, implies that $({\mathbb{W},H^{\prime},T^{\prime}})\models\varphi$ holds for all $\varphi\in\Gamma$ and all $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$. Note that, since $\mathcal{I}\prec({\mathbb{W},T})$, there is $\langle H^{\prime\prime},T^{\prime\prime}\rangle\in\mathbb{W}^{\prime}\cup\{\langle H,T\rangle\}$ with $H^{\prime\prime}\subset T^{\prime\prime}$ and we have that $({\mathbb{W},H^{\prime\prime},T^{\prime\prime}})$ is a semi-total model of $\Gamma$ and that $({\mathbb{W},H^{\prime\prime},T^{\prime\prime}})\prec({\mathbb{W},T^{\prime\prime}})$. Note also that $\langle H^{\prime\prime},T^{\prime\prime}\rangle\in\mathbb{W}^{\prime}$ implies $T^{\prime\prime}\in\mathbb{W}$ and, thus, the above is a contradiction with condition 1. Hence, we have that $({\mathbb{W},T})$ is a equilibrium model of $\Gamma$ for every $T\in\mathbb{W}$. Consequently, $\mathbb{W}$ is an autoepistemic world view.∎

• Proof of Proposition 2.

From Proposition C.11, we have that every autoepistemic world view $\mathbb{W}$ of any theory $\Gamma$ is also a weak autoepistemic world view. Furthermore, since all occurrences of $\operatorname{\mathbf{K}}$ in $\Gamma$ are in the scope of negation, from Lemma E.35, the converse also holds.    ∎

Lemma E.37**.**

Let $\varphi$ be a formula in which every atom is in the scope of the modal operator $\operatorname{\mathbf{K}}$ and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be some interpretation. Then, $\mathcal{I}\models\varphi$ iff $\mathbb{W}^{t}$ is an S5-model of $\varphi$.

Proof E.38**.**

In case $\varphi=\operatorname{\mathbf{K}}\psi$, we have that $\mathcal{I}\models\varphi$ iff $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\psi$ for all $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}$ iff $\mathbb{W}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $\varphi$. The rest of the proof follows by induction on the structure of $\varphi$.∎

Lemma E.39**.**

Let $\varphi$ be a formula in which every atom is in the scope of the modal operator $\operatorname{\mathbf{K}}$ and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be some interpretation. Then, $\mathcal{I}$ is a model of $\bot\leftarrow\varphi$ iff $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$.

Proof E.40**.**

*By definition, we have that $\mathcal{I}$ is a model of $\bot\leftarrow\varphi$

iff $\langle\mathbb{W},H^{\prime},T^{\prime}\rangle\models\bot\leftarrow\varphi$ for all $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$

iff $\langle\mathbb{W}^{t},T^{\prime},T^{\prime}\rangle\not\models\varphi$ for all $\langle H^{\prime},T^{\prime}\rangle\in\mathbb{W}\cup\{\langle H,T\rangle\}$

iff $\mathbb{W}^{t}$ is not an $\text{S5}_{\text{\tiny HT}}$-model of $\varphi$ (Lemma E.37)

iff $\mathbb{W}^{t}$ is an $\text{S5}_{\text{\tiny HT}}$-model of $\bot\leftarrow\varphi$

iff $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$.∎*

Lemma E.41**.**

Let $\Gamma$ be a theory and $\varphi$ be a formula in which every atom is in the scope of the modal operator $\operatorname{\mathbf{K}}$ and $\mathcal{I}=\langle\mathbb{W},H,T\rangle$ be some interpretation. Then, $\mathcal{I}$ is a equilibrium model of $\Gamma\cup\{\bot\leftarrow\varphi\}$ iff $\mathcal{I}$ is a equilibrium model of $\Gamma$ and $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$.

Proof E.42**.**

Assume first that $\mathcal{I}$ is a equilibrium model of $\Gamma\cup\{\bot\leftarrow\varphi\}$. Then, $\mathcal{I}$ is a model of $\Gamma$ and a model of $\bot\leftarrow\varphi$. From Lemma E.39, the latter implies that $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$. Suppose, for the sake of contradiction, that $\mathcal{I}$ is a equilibrium model of $\Gamma$ and, thus, that there is some model $\mathcal{I}^{\prime}=\langle\mathbb{W}^{\prime},H^{\prime},T^{\prime}\rangle$ of $\Gamma$ such that $\mathcal{I}^{\prime}\prec\mathcal{I}$. Then, $\mathcal{I}^{\prime}\prec\mathcal{I}$ implies that $(\mathbb{W}^{\prime})^{t}=\mathbb{W}$ and, thus, from Lemma E.39 and the fact that $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$, it follows that $\mathcal{J}$ is a model of $\bot\leftarrow\varphi$ which is a contradiction with the fact that $\mathcal{I}$ is a equilibrium model of $\Gamma\cup\{\bot\leftarrow\varphi\}$.

The other way around. Assume that $\mathcal{I}$ is a equilibrium model of $\Gamma$ and $\mathbb{W}^{t}$ is an S5-model of $\bot\leftarrow\varphi$. From Lemma E.39, we have that $\mathcal{I}$ is a model of $\bot\leftarrow\varphi$ and, thus, a equilibrium model of $\Gamma\cup\{\bot\leftarrow\varphi\}$.∎

• Proof of Proposition 3.

For Property LABEL:property:supraASP, note that since we are dealing with propositional theories there is no occurrence of $\operatorname{\mathbf{K}}$ and, thus, we can apply Proposition 2 and Theorem C.19 to see that the autoepistemic and G91 world views coincide. Then, just note that, since there is no occurrence of $\operatorname{\mathbf{K}}$, we have that $\Gamma^{\mathbb{W}}=\Gamma$ and, thus $\mathbb{W}$ is an autoepistemic world view of $\Gamma$ iff $\mathbb{W}$ is a G91-world view of $\Gamma$ iff $\mathbb{W}=\text{\rm SM}[\Gamma^{\mathbb{W}}]=\text{\rm SM}[\Gamma]$.

For Property LABEL:property:supraS5, from Corollary B.8, it follows that every autoepistemic world view $\mathbb{W}$ is also an S5-equilibrium model and it is easy to check that every S5-equilibrium model is also an S5-model.

For Property LABEL:property:constraint.monotonicity, we have that $\mathbb{W}$ is an autoepistemic world view of $\Gamma\cup\{\bot\leftarrow\varphi\}$ iff the following equality holds:

[TABLE]

Furthermore, from Lemma E.41 and the fact that every atom in $\varphi$ is in the scope of the modal operator $\operatorname{\mathbf{K}}$, it follows that $({\mathbb{W},T})\in{\rm{EQB}}[\Gamma\cup\{\bot\leftarrow\varphi\}]$ iff $({\mathbb{W},T})\in{\rm{EQB}}[\Gamma]$ and $\mathbb{W}$ is S5-model of $\bot\leftarrow\varphi$. Hence, we have that $\mathbb{W}$ is an autoepistemic world view of $\Gamma\cup\{\bot\leftarrow\varphi\}$ iff the following equality holds:

[TABLE]

and $\mathbb{W}$ is S5-model of $\bot\leftarrow\varphi$.    ∎