=Paper=
{{Paper
|id=Vol-1949/CILCpaper11
|storemode=property
|title=An S4F-related Monotonic Modal Logic
|pdfUrl=https://ceur-ws.org/Vol-1949/CILCpaper11.pdf
|volume=Vol-1949
|authors=Ezgi Iraz Su
|dblpUrl=https://dblp.org/rec/conf/ictcs/Su17
}}
==An S4F-related Monotonic Modal Logic==
https://ceur-ws.org/Vol-1949/CILCpaper11.pdf
An S4F-related monotonic modal logic
Ezgi Iraz SU?
University of Lisbon, Department of Mathematics, CMAF-CIO, Lisbon, Portugal
eirsu@fc.ul.pt
Abstract. This paper introduces a novel monotonic modal logic, allowing us to
capture the nonmonotonic variant of the modal logic S4F: we add a second new
modal operator into the original language of S4F, and show that the resulting for-
malism is strong enough to characterise the logical consequence of (nonmono-
tonic) S4F, as well as its minimal model semantics. The latter underlies major
forms of nonmonotonic logic, among which are (reflexive) autoepistemic logic,
default logic, and nonmonotonic logic programming. The paper ends with a dis-
cussion of a general strategy, naturally embedding several nonmonotonic logics
of a similar floor structure on which a (maximal) cluster sits.
Keywords: nonmonotonic S4F, minimal model semantics, monotonic modal logic
1 Introduction
The use of monotonic modal logics for describing nonmonotonic inference has a long
tradition in Artificial Intelligence. There exists a considerable amount of research in
the literature [1,2,3,4,5,6,7,8], logically capturing important forms of nonmonotonic
reasoning. Theoretically, we obtain a clear and simple monotonic framework for study-
ing further language extensions and possible generalisations. From a practical point of
view, we can check nonmonotonic deduction with a validity proving procedure in a
corresponding monotonic setting.
The modal logic S4F (aka, S4.3.2) is obtained from S4 by adding the axiom schema
F : (ϕ ∧ M L ψ) → L (M ϕ ∨ ψ)
[9] in which L is the epistemic modal operator, and M is its dual, defined by ¬L¬. A first
and detailed investigation of this logic was given in [10]; yet in time, S4F has also found
interesting theoretical applications in Knowledge Representation [11,12,13,14,15,16,17].
S4F is characterised by the class of Kripke models (W, T , V) in which W = W1 ∪ W2
for some disjoint sets W1 and W2 such that W2 is nonempty. Moreover, xT y if and only
if y ∈ W2 or x ∈ W1 . V is the valuation function such that V(x) is a set of propositional
? I am grateful to Luis Fariñas del Cerro, Andreas Herzig, and Levan Uridia for motivation, and
the anonymous reviewers for their useful comments. This paper has been supported by the
institution “Fundação para a Ciência e a Tecnologia (FCT)”, and the research unit “Centro de
Matemática, Aplicações Fundamentais e Investigação Operacional (CMAF-CIO)” of the Uni-
versity of Lisbon, Portugal via the grant, identified by the number “UID/MAT/04561/2013”.
variables for every x ∈ W. A cluster is simply a trivial S5 model (C, T , V) such that xT y
for every x, y ∈ C. In terms of Kripke semantics, S5 is the modal logic, characterised
by models in which the accessibility relation is an equivalence relation: it is reflexive,
symmetric, and transitive. Now, we can alternatively identify an S4F model with the
ordered triple (C1 ,C2 , V) in which C1 and C2 are disjoint cluster structures, C2 , ∅, and
any world in C2 can be accessed from every world in C1 .
This paper follows a similar approach to [18] and [8]: the former captures the re-
flexive autoepistemic reasoning [19,20] of nonmonotonic SW5 [21,22,23]. The latter
successfully embeds equilibrium logic [24,25], which is a logical foundation for an-
swer set programming (ASP) [26,27,28], into a monotonic bimodal logic called MEM.
All these works are, in essence, parts of a project that aims to reexamine the logical and
mathematical foundations of nonmonotonic logics. The overall project will then culmi-
nate in a single monotonic modal framework, enabling us to obtain a unified perspective
of various forms of nonmonotonic reasoning.
As a reference to the analogy between all such works, we here keep the same sym-
bols T and S1 with [8,18] for the accessibility relations. Roughly speaking, [8,18] and
this paper all propose Kripke models, composed of a union of 2-floor (disjoint) struc-
tures. In general, while the relation T helps access from ‘bottom’ (first floor) to ‘top’
(second floor), the relation S works in the opposite direction. However, the structures of
bottom and top differ in all formalisms. In particular, the models here and in [18] are
respectively the extensions of the Kripke models of S4F and SW5 with the S-relation;
whereas MEM restricts top to a trivial cluster of a singleton, and forces all subsets
of the top valuation to appear inside the bottom structure to check the minimality
criterion of equilibrium models [24,25]. Similarly to [8,18], we also propose here a
modal language L[T],[S] with two (unary) modal operators, namely [T] and [S]. The for-
mer is a direct translation of L in the language of S4F (LS4F ) into L[T],[S] via a mapping
‘tr : LS4F −→ L[T],[S] ’. The relations T and S respectively interpret the modal operators
[T] and [S]. We call the resulting monotonic formalism MLF. We then add into MLF
the negatable axiom, resulting in MLF∗ : modal logic of nonmonotonic S4F. The negat-
able axiom ensures that the cluster C1 (bottom) of MLF frames is nonempty, so it
turns our frames into exactly 2-floor structures in MLF∗ : both floors are maximal clus-
ters w.r.t. the relation T . Essentially, this axiom enables us to refute any nontautology of
L[T],[S] as it allows us to have all possible valuations in an MLF∗ model. Thus, we show
that the formula hTi[T](ϕ ∧ [S]¬ϕ) characterises maximal ϕ-clusters in MLF∗ . This re-
sult paves the way to our final goal in which we capture nonmonotonic consequence
(abbreviated ‘ |≈S4F ’) of S4F in the monotonic modal logic MLF∗ :
ϕ |≈S4F ψ if and only if [T] tr(ϕ) ∧ [S]¬tr(ϕ) → [T]tr(ψ) is valid in MLF∗ .
The rest of the paper is organised as follows. Section 2 introduces the monotonic
modal logic MLF: we first define its bimodal language, and then propose two classes
of frames, namely K and F. They are respectively based on standard Kripke frames,
and the cluster-based component frames, which are in the form of a floor structure. We
axiomatise the validities of our logic, and finally prove that MLF is sound and complete
1 The symbols T and S of [8] respectively refer to ‘Top’ and ‘Subset’. However, the relation S
has a different character and meaning in this paper, which is similar to those of [18].
w.r.t. both semantics. In Section 3, we extend MLF with the negatable axiom, and call
the resulting logic MLF∗ . We introduce two kinds of model structures, K∗ and F∗ , and
end with the soundness and completeness results. Section 3.1 recalls minimal model
semantics of nonmonotonic S4F: we define the preference relation, and then give the
definition of a minimal model for S4F. Section 3.2 first captures minimal models of
S4F, and then embeds the consequence relation of S4F into MLF∗ . Section 4 discusses
a general approach, allowing us to capture major nonmonotonic logics. Section 5 makes
a brief overview of this paper, and mentions our future goals.
2 A monotonic modal logic related to nonmonotonic S4F
We here propose a new formalism called MLF, which is closely associated with S4F.
2.1 Language (L[T],[S] )
Throughout the paper we suppose P an infinite set of propositional variables, and Pϕ its
restriction to those of a formula ϕ. We also consider Prop as the set of all propositional
formulas of our language. The language L[T],[S] is formally defined by the grammar:
ϕ F p | ¬ϕ | ϕ → ϕ | [T]ϕ | [S]ϕ
where p ranges over P. L[T],[S] is therefore a bimodal language with the modalities [T]
def def def def
and [S]. As usual, > = ϕ → ϕ, ⊥ = ¬(ϕ → ϕ), ϕ ∨ ψ = ¬ϕ → ψ, ϕ ∧ ψ = ¬(ϕ → ¬ψ),
def
and ϕ ↔ ψ = (ϕ → ψ) ∧ (ψ → ϕ). Moreover, hTiϕ and hSiϕ respectively abbreviate
¬[T]¬ϕ and ¬[S]¬ϕ.
2.2 Kripke semantics for MLF
We now describe the class K of Kripke frames for MLF. A K-frame is a triple (W, T , S):
– W is a non-empty set of possible worlds.
– T , S ⊆ W × W are binary relations such that for every w, u, v ∈ W,
(w, w) ∈ T refl(T )
(w, u) ∈ T and (u, v) ∈ T ⇒ (w, v) ∈ T trans(T )
(w, u) ∈ T , (u, w) < T and (w, v) ∈ T ⇒ (v, u) ∈ T f(T )
(w, u) ∈ S ⇒ (u, u) ∈ S refl2 (S)
(w, u) ∈ S and (u, v) ∈ S ⇒ u = v wtriv2 (S)
(w, u) ∈ T ⇒ (u, w) ∈ T or (u, w) ∈ S msym(T , S)
(w, u) ∈ S ⇒ w = u or (u, w) ∈ T wmsym(S, T ).
The first three properties above characterise the frames of the modal logic S4F [9].
Thus, a K-frame is an extension of an S4F frame by a second relation S. Given a K-
frame F = (W, T , S), a K-model is a pair M = (F , V) in which V : W → 2P is the map,
assigning to each w ∈ W a valuation V(w). Then, given w ∈ W, a pointed K-model is a
pair Mw = (M, w), and similarly, a pointed K-frame is a pair Fw = (F , w).
Truth conditions The truth conditions are standard: (for p ∈ P)
M, w |=MLF p if p ∈ V(w);
M, w |=MLF ¬ϕ if M, w 6|=MLF ϕ;
M, w |=MLF ϕ → ψ if M, w 6|=MLF ϕ or M, w |=MLF ψ;
M, w |=MLF [T]ϕ if M, u |=MLF ϕ for every u such that wT u;
M, w |=MLF [S]ϕ if M, u |=MLF ϕ for every u such that wSu.
We say that ϕ is MLF satisfiable if M, w |=MLF ϕ for some K-model M and w in M.
Moreover, ϕ is MLF valid (for short, |=MLF ϕ) if M, w |=MLF ϕ for every w of every K-
model M. Then, ϕ is valid in M (M |=MLF ϕ) when M, w |=MLF ϕ for every w in M.
2.3 Cluster-based floor semantics for MLF
We here define the frames of a floor structure for MLF, and call their class F. The
underlying idea is due to the property ‘f(T )’ of K-frames, and in fact, F is only a
subclass of K. However, F-frames with some additional properties play an important
role in the completeness proof. We now start with the definition of a T -cluster2 [22,29].
Definition 1. Given a K-frame (W, T , S), let C be a subset of W. Then,
– C is a T -cluster if wT u for every w, u ∈ C;
– C is maximal if no proper superset of C in W is a T -cluster.
– C is a T -cone if for every w ∈ W, and every u ∈ C, uT w implies w ∈ C;
– C is final if wT u for every w ∈ W and every u ∈ C.
It follows from Definition 1 that the restriction of T to a T -cluster C (abbreviated T |C )
is a universal relation, viz. T |C = C × C. So, (C, T ) happens to be a trivial S5 frame.
Given a K-frame F = (W, T , S), the relation T partitions F into disjoint subframes
F 0 = (W 0 , T , S) in which W 0 = C1 ∪C2 for some maximal clusters C1 ,C2 ⊆ W 0 ⊆ W such
that C1 ∩C2 = ∅, and C2 , ∅ is a final cone in W 0 . Thus, T |W 0 = (W 0 ×C2 )∪(C1 ×C1 ). We
now define the operators T (·), S(·) : 2W −→ 2W , respectively assigning to every X ⊆ W,
T (X) = {u ∈ W : wT u for some w ∈ X};
S(X) = {u ∈ W : wSu for some w ∈ X}.
When X={w}, we simply write T (w) (resp. S(w)), denoting the set of all worlds that w
can access via T (resp. S). Note that T (·) and S(·) are homomorphisms under union:
T (X ∪ Y) = T (X) ∪ T (Y) and S(X ∪ Y) = S(X) ∪ S(Y).
We now formally define the above-mentioned partitions of a K-frame w.r.t. T .
Definition 2. Given a K-frame F = (W, T , S), let C = (C1 ,C2 ) be a pair of disjoint
subsets of W such that C2 , ∅. Then, C is called a component of F if:
1. C1 and C2 are maximal clusters;
2 Unless specified otherwise, any definition of this paper is given w.r.t. the relation T .
2. T ∩ (C1 × C2 ) = C1 × C2 .
So, a component C = (C1 ,C2 ) has a ‘two-layered’ structure: C1 is the first floor (‘F1-
cluster’), and C2 is the second floor (‘F2-cluster’). Clearly, C2 is the final cone of the
structure C. Note that C can also be transformed into a special K-frame
F C = C1 ∪ C2 , (C1 ∪ C2 ) × C2 ∪ (C1 × C1 ), (C2 × C1 ) ∪ ∆C1
(1)
where ∆C1 is the diagonal of C1 × C1 , i.e., ∆C1 = {(w, w) : w ∈ C1 }. Given any two dif-
ferent components C = (C1 ,C2 ) and C0 = (C10 ,C20 ) of a K-frame F , C1 ∪C2 and C10 ∪C20
are disjoint, and C and C0 are disconnected in the sense that there is no T -access (nor an
S-access) from one to the other. As a result, a K-frame F is composed of an arbitrary
union of components; however, when F contains a component in which the F1-cluster
is empty, and S , ∅ (and so, S is arbitrary), (1) is not sufficient to recover F . This
ambiguity in the transformation will be solved in the following section as the proposed
logic MLF∗ does not accept components whose F1-cluster is empty.
Definition 3. An F-frame is a pair C = (C1 ,C2 ), having a component structure.
We now define a function µ : F → K, assigning a K-frame µ(C) = F C (see (1)) to
each F-frame C. As two distinct components C and C0 give rise to two distinct K-frames
0
F C and F C , µ is 1-1, but not onto3 . Thus, F is indeed a (proper) subclass of K.
Proposition 1. Given a K-frame F = (W, T , S), let C = (C1 ,C2 ) be a component of F ,
and w ∈ C1 ∪ C2 , then
1. if w ∈ C1 , then T (w) = C1 ∪ C2 , and S(w) = {w};
2. if w ∈ C2 , then T (w) = C2 , and S(w) = C1 when C1 , ∅; otherwise S(w) is arbitrary.
The proof easily follows from the frame properties of K.
Corollary 1. For a K-frame F =(W, T , S), and a component C=(C1 ,C2 ) of F , we have:
1. T (C1 ∪ C2 ) = C1 ∪ C2 ;
2. S(C1 ∪ C2 ) ⊆ C1 ∪ C2 .
Corollary 2. Given a pointed K-frame Fw , let C = T (w)\C1 if w is in an F1-cluster C1 ;
else if w is in an F2-cluster C2 , let C = T (w). Take C 0 =S(C) \C. Then, CFw =(C 0 ,C) ∈ F.
Note that the component generated by w ∈ F is exactly the one in which w is placed.
So, any point from the same component forms itself. Using Corollary 2, we now define
another function ν, assigning to each pointed K-frame Fw an F-frame CFw . Clearly, ν
is not 1-1, but is onto. Finally, {ν(Fw ) : w ∈ W} identifies all the components in F . The
following proposition generalises this observation.
Proposition 2. Given an F-frame C = (C1 ,C2 ) and w ∈ C1 ∪C2 , we have ν(µ(C), w) = C.
3 Note that there is no F-frame being mapped to (i) a K-frame containing more than one com-
ponent structure in it, and (ii) a K-frame composed of only one component with a single
(nonempty) cluster structure in which S , ∅.
These transformations between frame structures of MLF enable us to define valuations
also on the components C ∈ F, resulting in an alternative semantics for MLF via F-
models. The new semantics can be viewed as a reformulation of the Kripke semantics:
given a K-model M = (F C , V) for some Kripke frame F C ∈ µ(F) and a valuation V, one
can transform F C to a component ν(FwC ) = C ∈ F for some w ∈ C1 ∪C2 (see Proposition
2). This discussion allows us to define pairs (C, V) in which C ∈ F, and V is the valua-
tion restricted to C. Such valuated components are called ‘F-models’, and they make it
possible to transfer K-satisfaction to F-satisfaction.
Truth conditions (the modal cases) for an F-model (C, V)=(C1 ,C2 , V) and w ∈ C1 ∪C2 ,
(C, V), w |=MLF [T]ψ if and only if
– if w ∈ C1 then (C, V), v |=MLF ψ for all v ∈ C1 ∪ C2 (i.e., (C, V) |=MLF ψ);
– if w ∈ C2 then (C, V), v |=MLF ψ for all v ∈ C2 .
(C, V), w |=MLF [S]ψ if and only if
– if w ∈ C1 then (C, V), w |=MLF ψ;
– if w ∈ C2 then (C, V), v |=MLF ψ for all v ∈ C1 if C1 , ∅; else ‘no strict conclusion’.
The next result reveals the relation between the Kripke and the floor sematics of MLF.
Proposition 3 (corollary of Proposition 2). For an F-model (C, V), w ∈ C, and ϕ ∈
L[T],[S] , (C, V), w |=MLF ϕ if and only if (F C , V), w |=MLF ϕ.
2.4 Axiomatisation of MLF
We here give an axiomatisation of MLF, and prove its completeness. Recall that K([T]),
T([T]), 4([T]) and F([T]) characterise the modal logic S4F [30]. The monotonic logic
defined by Table 1 is MLF. The schemas T2 ([S]) and WTriv2 ([S]) can be combined
K([T]) the modal logic K for [T]
K([S]) the modal logic K for [S]
T([T]) [T]ϕ → ϕ
4([T]) [T]ϕ → [T][T]ϕ
F([T]) (ϕ ∧ hTi[T]ψ) → [T](hTiϕ ∨ ψ)
T2 ([S]) [S]([S]ϕ → ϕ)
WTriv2 ([S]) [S](ϕ → [S]ϕ)
MB([T], [S]) ϕ → [T](hTiϕ ∨ hSiϕ)
WMB([S], [T]) ϕ → [S](ϕ ∨ hTiϕ)
Table 1. Axiomatisation of MLF
into the axiom Triv2 ([S]), i.e., [S]([S]ϕ ↔ ϕ), referring to the “triviality in the second
S-step”. Finally, MB([T], [S]) and WMB([S], [T]) are familiar from tense logics.
2.5 Soundness and completeness of MLF
The axiom schemas given in Table 1 precisely characterise the class K of MLF frames.
We only show that F([T]) describes the property f(T ) of K-frames, but the rest is similar.
– Let M=(W, T , S, V) be a K-model, satisfying f(T ). We want to show that F([T]) is
valid in M. Let w ∈ W be such that M, w |=MLF ϕ ∧ hTi[T]ψ (?). Then, it suffices to
prove that M, w |=MLF [T](hTiϕ ∨ ψ). For an arbitrary u ∈ W, assume that (w, u) ∈ T .
Case (1): let (u, w) ∈ T . The assumption (?) implies that M, w |=MLF ϕ. Then, it also
holds that M, u |=MLF hTiϕ; clearly, so does M, u |=MLF hTiϕ ∨ ψ.
Case (2): let (u, w) < T . Then, by the assumption (?), M, w |=MLF hTi[T]ψ. Thus,
there is v ∈ W such that (w, v) ∈ T and M, v |=MLF [T]ψ. As M satisfies f(T ), we get
(v, u) ∈ T . As M, v |=MLF [T]ψ, we have M, u |=MLF ψ; hence, M, u |=MLF hTiϕ ∨ ψ.
– Let F =(W, T , S) be a K-frame in which f(T ) fails. So, there exists w, u, v ∈ W
with (u, w) < T while (w, u) ∈ T and (w, v) ∈ T ; yet (v, u) < T . Thanks to the last
2 claims, we have w,v (otherwise (v, u) < T would contradict (w, u) ∈ T ). Due to
the first 2 claims, w , u (otherwise, (w, u)=(u, w), and (u, w) ∈ T ). We now take a
valuation V satisfying: M, w |=MLF ϕ (N), but M, x 6|=MLF ϕ for any x , w; similarly,
M, u 6|=MLF ψ (H), but M, y |=MLF ψ for every y , u. Since (v, u) < T , and thanks to
the choice of V, M, v |=MLF [T]ψ. As (w, v) ∈ T , and also by using (N), we have
M, w |=MLF ϕ ∧ hTi[T]ψ. On the other hand, M, u |=MLF [T]¬ϕ since (u, w) < T and w
is the only point satisfying ϕ. Then, (H) further implies that M, u |=MLF [T]¬ϕ ∧ ¬ψ.
Since (w, u) ∈ T , we also get M, w |=MLF hTi([T]¬ϕ ∧ ¬ψ). So, we are done.
Corollary 3. MLF is sound w.r.t. the class K of frames.
Here, we only need to show that the inference rules of MLF are validity-preserving.
Theorem 1. MLF is complete w.r.t. the class of K-frames.
Proof. We use the method of canonical models (see [29]), so we first define the canon-
ical model Mc = (W c , T c , Sc , V c ) in which
– W c is the set of maximally consistent sets of MLF.
– T c and Sc are the accessibility relations on W c with:
ΓT c Γ 0 if and only if {ψ : [T]ψ ∈ Γ} ⊆ Γ 0 ;
ΓSc Γ 0 if and only if {ψ : [S]ψ ∈ Γ} ⊆ Γ 0 .
– V c is the valuation s.t. V c (Γ) = Γ ∩ P, for every Γ ∈ W c .
By induction on ϕ, we prove a truth lemma saying: “Γ |=MLF ϕ iff ϕ ∈ Γ” for every
ϕ ∈ L[T],[S] . Then, it remains to show that Mc satisfies all constraints of K, and so is
a legal K-model of MLF. We here give the proof only for wtriv2 (S) and wmsym(S, T ).
I The schema WTriv2 ([S]) guarantees that Mc satisfies wtriv2 (S): let Γ1 Sc Γ2 (?) and
Γ2 Sc Γ3 (??). Assume for a contradiction that Γ2 , Γ3 . Thus, there exists ϕ ∈ Γ2 with
¬ϕ ∈ Γ3 , implying that hSi¬ϕ ∈ Γ2 by the hypothesis (??). Since Γ2 is maximally
consistent, ϕ ∧ hSi¬ϕ ∈ Γ2 . So, using the hypothesis (?), we get hSi(ϕ ∧ hSi¬ϕ) ∈ Γ1 .
However, since Γ1 is maximally consistent, any instance of WTriv2 ([S]) is in Γ1 . Thus,
[S](ϕ→[S]ϕ) ∈ Γ1 , and it contradicts the consistency of Γ1 .
I The schema WMB([S], [T]) ensures that wmsym(S, T ) holds in Mc : suppose that
ΓSc Γ 0 (?) for Γ, Γ 0 ∈ W c . W.l.o.g., let Γ , Γ 0 . Then, there exists ψ ∈ Γ 0 with ¬ψ ∈ Γ.
We need to show that Γ 0 T c Γ. So, let ϕ be such that [T]ϕ ∈ Γ 0 . As Γ 0 is maximally
consistent, we have both ϕ ∨ ψ ∈ Γ 0 and [T]ϕ ∨ [T]ψ ∈ Γ 0 . We know that [T]ϕ ∨ [T]ψ →
[T](ϕ ∨ ψ) is a theorem of MLF, so it is in Γ 0 . Then, by Modus Ponens (MP), we
get [T](ϕ ∨ ψ) ∈ Γ 0 , further implying (ϕ ∨ ψ) ∧ [T](ϕ∨ ψ) ∈ Γ 0 since we already have
(ϕ ∨ ψ) ∈ Γ 0 . The assumption (?) gives us that hSi ϕ ∨ ψ ∧ [T] ϕ ∨ ψ ∈ Γ. Since
Γ is maximally consistent, any instance of WMB([S], [T]) is in Γ; in particular, so is
hSi (ϕ ∨ ψ) ∧ [T](ϕ ∨ ψ) → (ϕ ∨ ψ). Finally, again by MP, we have ϕ ∨ ψ ∈ Γ. Since
¬ψ ∈ Γ, it follows that ϕ ∈ Γ.
Soundness and completeness of MLF w.r.t. F. Since any component C ∈ F can be
converted to a K-frame µ(C), soundness follows from Corollary 3 and Proposition 2. As
to completeness, for a non-theorem ϕ ∈ L[T],[S] , ¬ϕ is consistent. Let Γ¬ϕ be a maximally
consistent set in the canonical model Mc such that ¬ϕ ∈ Γ¬ϕ . As the canonical frame
Mc = (W c , T c , Sc ) is a member of the class K, Proposition 1 and Proposition 2 allow
us to define the component Cc = (C1c ,C2c ) with Γ¬ϕ ∈ C1c ∪ C2c . Moreover, by Corollary
1, C1c ∪ C2c is closed under the operators T c (·) and Sc (·). Therefore, modal satisfaction
is preserved between Mc and Cc . As a result, Cc , Γ¬ϕ 6|=MLF ϕ (i.e., Cc , Γ¬ϕ |=MLF ¬ϕ).
3 Where we capture nonmonotonic S4F: Modal logic MLF∗
We here propose an extension of MLF with a new axiom schema
Neg([S], [T]): hTi[T]ϕ → hTihSi¬ϕ
where ϕ ∈ Prop is non-tautological. We call this schema ‘negatable axiom’ and the
resulting formalism MLF∗ . MLF∗ -models are of 2 kinds, namely K∗ and F∗ . They are
obtained respectively from the classes K and F by adding a ‘model’ constraint:
neg(S, T ): for every P ⊆ P, there exists a world w such that P = V(w).
In other words, MLF∗ -models can falsify any nontheorem of our logic, i.e., for every
such ϕ, there exists a world w such that w |=MLF∗ ¬ϕ. Every F∗ -model (C1 ,C2 , V) now has
an exactly ‘two-floor’ form: C1 , ∅, and C1 includes a world w, at which a propositional
nontheorem ϕ, valid in C2 , is refuted. A K∗ -model is indeed an arbitrary combination
of F∗ -models. Below we show that Neg([S], [T]) precisely corresponds to neg(S, T ).
Proposition 4. Given a K-model M = (W, T , S, V) in MLF,
Neg([S], [T]) is valid in M if and only if M is a K∗ -model.
Proof. Let M = (W, T , S, V) be a K-model of MLF.
(=⇒): Assume that M is not a K∗ -model. Then, there exists a nontautological propo-
sitional formula ϕ ∈ Prop such that M |=MLF ϕ. Clearly, [T]ϕ, [S]ϕ and [T][S]ϕ are all
valid in M, but then so is hTi[T]ϕ (thanks to the reflexivity of T ). This implies that
hTi[T]ϕ ∧ [T][S]ϕ is also valid in M. Thus, Neg([S], [T]) is not valid in M.
(⇐=): Let M be a K∗ -model (•). Let ϕ ∈ Prop be a nontheorem. Take β = hTi[T]ϕ →
hTihSi¬ϕ. We need to show that M |=MLF∗ β. Let w ∈ W be such that M, w |=MLF∗ hTi[T]ϕ.
We first consider the F-model C = (C1 ,C2 , V), generated by w as in Corollary 2. By con-
struction, ϕ is valid in C2 , and (•) implies an existence of u ∈ C1 such that u refutes ϕ. By
the frame properties of F, there exists v ∈ C2 satisfying vSu and M, v |=MLF∗ hSi¬ϕ. Re-
gardless of the floor to which w belongs, wT v, and v ∈ C2 . Thus, M, w |=MLF∗ hTihSi¬ϕ.
Proposition 5. Given an F-model (C, V) = (C1 ,C2 , V) in MLF,
Neg([S], [T]) is valid in (C, V) if and only if (C, V) is an F∗ -model.
Neg([S], [T]) has an elegant representation. However, as it makes the reasoning clear in
the demanding proofs of this section, we find it handier to use the equivalent version
Neg’([S], [T]): hTi[T]ϕ → hTihSi(¬ϕ ∧ Q)
of Neg([S], [T]) in which ϕ ∈ Prop is a nontheorem, and Q is a conjunction of a finite
set of literals (i.e., p or ¬p, for p ∈ P) such that the set {¬ϕ, Q} is consistent.
Proposition 6. For a K∗ -model M=(W, T , S, V) and w ∈ W,
M, w |=MLF∗ Neg([S], [T]) if and only if M, w |=MLF∗ Neg’([S], [T]).
Proof. The right-to-left direction is straightforward: take Q = ∅ and the result follows.
For the opposite direction, we first assume that M, w |=MLF∗ Neg([S], [T]) (N). Let ϕ ∈
Prop be a nontheorem of MLF∗ viz. M, w |=MLF∗ hTi[T]ϕ (H). Let Q be a conjunction
of finite literals such that ¬ϕ ∧ Q is consistent. Then, ϕ ∨ ¬Q ∈ Prop is a nontheorem
of MLF∗ . Moreover, from the assumption (H), we also get M, w |=MLF∗ hTi[T](ϕ ∨ ¬Q).
Lastly, by the hypothesis (N), we have M, w |=MLF∗ hTihSi(¬ϕ ∧ Q).
We finally transform a valuated cluster (C, V) into an F∗ -model. We first construct a set
C1 = {xϕ : for every ϕ ∈ Prop such that ¬ϕ 0 ⊥, (C, V) |=MLF ϕ and xϕ < C}
into which we put a point xϕ < C for every nontheorem ϕ that is valid in C. So, C ∩C1 =
∅. Then, we extend the universal relation T on C to T = C1 ∪ C × C ∪ (C1 × C1 ) on
0
C ∪ C1 . The valuation V defined over C is also extended to V 0 : C1 ∪ C −→ P satisfying:
V 0 |C = V, and V 0 (xϕ ) is designed to falsify ϕ. Hence, by definition, (C1 ,C, V 0 ) ∈ F∗ .
Soundness and completeness of MLF∗ We have seen that MLF is sound w.r.t. F, so
Proposition 5 implies that MLF∗ is sound w.r.t. F∗ . Since any K∗ -model is a combi-
nation of F∗ -models, we can generalise this result to K∗ . We here show that MLF∗ is
complete w.r.t. F∗ : first we take a canonical model Mc = (W c , T c , Sc , V c ) of MLF∗ (see
Theorem 1 for the details). Then, we define a valuated component (Cc , V c ) = (C1c ,C2c , V c )
for C1c ,C2c ⊆ W c as in Section 2.5. We want to show that (Cc , V c ) is an F∗ -model. So, it
is enough to prove that Neg([S], [T]) ensures the property neg(S, T ).
First recall that every F-frame C corresponds to a K-frame µ(C) = F C , and by
Proposition 2, ν µ(C), w = C for w ∈ C1 ∪ C2 . Thus, such µ(Cc ), V c is a submodel of
Mc since it is a K∗ -frame. For nontautological ϕ ∈ Prop, let us assume Γ |=MLF∗ ϕ (i.e.,
ϕ ∈ Γ) for every Γ ∈ C2c (so, ϕ is consistent). This implies that (Cc , V c ), Γ |=MLF∗ [T]ϕ
(i.e., [T]ϕ ∈ Γ), for every Γ ∈ C2c . Using the fact that µ(Cc ) is part of the canonical
model Mc , we have T c |C c ∪C c ⊃ (C1c ∪ C2c ) × C2c . Thus, (Cc , V c ), Γ |=MLF∗ hTi[T]ϕ for
1 2
every Γ ∈ C1c ∪C2c . As any instance of Neg([S], [T]) is valid in (Cc , V c ), hTihSi¬ϕ ∈ Γ for
every Γ ∈ C1c ∪ C2c . In other words, (Cc , V c ) |=MLF∗ hTihSi¬ϕ. Thus, there exists Γ 0 ∈ W c
such that ΓT c Γ 0 and Γ 0 |=MLF∗ hSi¬ϕ (i.e., hSi¬ϕ ∈ Γ 0 ). As T (C ∪ A) = C ∪ A in F,
we have Γ 0 ∈ C1c ∪ C2c . Moreover, there also exists Γ 00 ∈ W c such that Γ 0 Sc Γ 00 and
Γ 00 |=MLF∗ ¬ϕ. By Corollary 1, S(C1c ∪ C2c ) ⊆ C1c ∪ C2c , yet from our initial hypothesis,
we obtain Γ 00 ∈ C1c . To sum up, Γ 00 is a maximally consistent set in Cc such that
(Cc , V c ), Γ 00 6|=MLF∗ ϕ.
3.1 Minimal model semantics for nonmonotonic S4F
This section recalls the minimal model semantics for nonmonotonic S4F [22]. We first
define a preference relation between S4F models, enabling us to check minimisation.
Definition 4. An S4F model N = (N, R, U) is preferred over a valuated cluster (C, V) if
– N = C ∪ C1 for some (nonempty) set C1 of possible worlds such that C ∩ C1 = ∅;
– R = N × C ∪ (C1 × C1 );
– The valuations V and U agree on C (i.e., V = U|C );
– There exists ϕ ∈ Prop such that C |= ϕ and N 6|= ϕ.
We abbreviate it by N (C, V). A valuated cluster (C, V) is then a minimal model of a
theory (finite set of formulas) Γ in S4F if
– (C, V), x |= Γ for every x ∈ C (i.e., (C, V) |= Γ);
– N 6|= Γ for every N such that N (C, V).
Finally, a formula ϕ is a logical consequence of a theory Γ in S4F (abbreviated Γ |≈S4F ϕ)
if ϕ is valid in every minimal model of Γ. For example, q |≈S4F ¬p ∨ q, yet ¬p ∨ q |0S4F q.
3.2 Embedding nonmonotonic S4F into MLF∗
We here embed nonmonotonic S4F into MLF∗ . With this aim, we first translate the
language of S4F (LS4F ) into L[T],[S] via a mapping ‘tr’: we simply and only replace
L ∈ L[T],[S] by [T]. The following proposition proves that this translation is correct, and
clarifies how to characterise minimal models of S4F in MLF∗ .
Proposition 7. Given an F∗ -model (C, V) = (C1 ,C, V), and α ∈ LS4F , we have:
1. (C, V), w |=MLF∗ tr(α), for every w ∈ C if and only if (C, V|C ) |= α.
2. (C, V) |=MLF∗hTi[T] tr(α)∧[S]¬tr(α) if and only if (C, V|C ) is a minimal model of α.
Proof. The proof of the first item is by induction on α. As to the second item, for the
proof of the ‘only if ’ part, we first assume (C, V) |=MLF∗ hTi[T](tr(α) ∧ [S]¬tr(α)) ().
(1) From (), we obtain that (C, V), u |=MLF∗ tr(α) (N), and (C, V), u |=MLF∗ [S]¬tr(α) (H)
for every u ∈ C (consider: for w ∈ C1 , () implies that there is u ∈ C1 ∪ C such that wT u
and (C, V), u |=MLF∗ [T](tr(α) ∧ [S]¬tr(α)). So, u ∈ C; otherwise it yields a contradiction).
Then, using Proposition 7.1 and (N), we get (C, V|C ) |= α. So, the first condition holds.
(2) By definition, it remains to show that N 6|= α for every S4F model N such that
N (C, V|C ). Let N = (N, R, U) be a preferred model over the valuated cluster (C, V|C )
satisfying: N = C ∪C 0 for some (cluster) C 0 such that C ∩C 0 = ∅, R = N ×C ∪(C 0 ×C 0 ),
and U|C = V|C . By Definition 4, we also know that there exists ψ ∈ Prop such that
(C, V|C ) |= ψ (•), but N 6|= ψ. Therefore, there exists r ∈ C 0 viz. N, r 6|= ψ (i.e., N, r |= ¬ψ).
(3) As (C, V) is an F∗ -model, Neg([S], [T]) is valid in it; due to Proposition 6, so is
Neg’([S], [T]). Hence, (C, V) |= hTi[T]ϕ → hTihSi(¬ϕ ∧ Q) for a non-theorem ϕ ∈ Prop
of LMLF∗ , and a conjunction of a finite set of literals Q such that {¬ϕ, Q} is consistent.
(4) By (•) in the item (2) and also using Lemma 7.1, we get (C, V), u |=MLF∗ tr(ψ) for
every u ∈ C. Since (C, V) is an F∗ -model, we also have (C, V), u |=MLF∗ [T]tr(ψ); even
(C, V), u |=MLF∗ hTi[T]tr(ψ) for every u ∈ C (♣). V Moreover, we know that tr(ψ) is not
a tautology; otherwise N, r |= ψ. Let Q0 = p∈ Pα ∩U(r)
p ∧ V
q∈ Pα \U(r)
¬q . It is
clear that N, r |= Q0 , but we also know that N, r |= ¬ψ, so we have N, r |= ¬ψ ∧ Q0 .
We so conclude that {¬ψ, Q0 } is consistent; then so is {¬tr(ψ), Q0 }. As (C, V) is an F∗ -
model, an instance of the negatable axiom, namely hTi[T]tr(ψ) → hTihSi(¬tr(ψ) ∧ Q0 ),
is valid in (C, V). So, (♣) implies that (C, V), u |=MLF∗ hTihSi(¬tr(ψ) ∧ Q0 ) for every u ∈ C.
This means that there exists a point xψ ∈ C1 such that (C, V), xψ |=MLF∗ ¬tr(ψ) ∧ Q0 , i.e.,
(C, V), xψ |=MLF∗ ¬tr(ψ) and (C, V), xψ |=MLF∗ Q0 . As a result, V(xψ ) ∩ Ptr(α) = U(r) ∩ Pα .
(5) Note that r and xψ agree on Pα . By (H), we also have (C, V), x |=MLF∗ ¬tr(α) for every
x ∈ C1 ; in particular, (C, V), xψ |=MLF∗ ¬tr(α). To summarise the observation above:
1. The pointed model {xψ },C, V|(C∪{xψ }) , xψ in MLF∗ , and the pointed model (N, r)
in S4F have the similar structure: both contain the same maximal valuated cluster
(C, V|C ) and one additional reflexive point that can have access to all points of C;
2. Pα = Ptr(α) and V(xψ ) ∩ Ptr(α) = U(r) ∩ Pα ;
3. Both α and tr(α) are the exact copies of each other, except that one contains L
wherever the other contains [T] (note that tr(α) contains neither [S] nor hSi).
Then, it follows that N, r 6|= α, which further implies that N 6|= α. By definition, (C, V|C )
is a minimal model for α. The other part of the proof is similar.
We are now ready to show how we capture the logical consequence of S4F in MLF∗ .
Theorem 2. For α, β ∈ LS4F , α |≈S4F β iff |=MLF∗ [T](tr(α) ∧ [S]¬tr(α)) → [T]tr(β).
Proof. We first take ζ = [T](tr(α) ∧ [S]¬tr(α)) → [T]tr(β).
(=⇒): Assume that α |≈S4F β in S4F (N). Let (C, V) = (C1 ,C2 , V) be an F∗ -model. Then
(C2 , V|C2 ) is a valuated cluster over C2 . We need to show that (C, V) |=MLF∗ ζ. “For every
w ∈ C1 , (C, V), w |=MLF∗ ζ” trivially holds: by the frame constraints w.r.t. T in MLF∗ ,
(C, V), w 6|=MLF∗ [T](tr(α) ∧ [S]¬tr(α)) for any w ∈ C1 (otherwise, (C, V) |=MLF∗ tr(α), but
also (C, V) |=MLF∗ ¬tr(α), yielding a contradiction). Let x ∈ C2 be such that (C, V), x |=MLF∗
[T](tr(α) ∧ [S]¬tr(α)). We know that T |C2 is a universal relation, so “for all x ∈ C2 ,
(C, V), x |=MLF∗ hTi[T](tr(α) ∧ [S]¬tr(α))” trivially follows. Then, by Proposition 7.2, we
conclude that (C2 , V|C2 ) is a minimal model for α. Then, as α |≈S4F β by the hypothesis
(N), β is valid in (C2 , V|C2 ), i.e., (C2 , V|C2 ) |= β. Thus, Proposition 7.1 gives us that
(C, V), z |=MLF∗ tr(β) for every z ∈ C2 . Since C2 is a cluster which is a final cone, we also
have (C, V), z |=MLF∗ [T]tr(β) for every z ∈ C; in particular, (C, V), x |=MLF∗ [T]tr(β).
(⇐=): Assume that ζ is valid in MLF∗ (H). We need to prove that α |≈S4F β. Let (C, V) be
a minimal model of α. Then, we take an S4F model N = (C ∪ C 0 ), R, U preferred over
(C, V). viz. N (C, V). Thus, N 6|= α (). Now, let us construct (C, V) = (C1 ,C2 , V) as fol-
lows: take C2 as the maximal α-cluster C (i.e., exactly the same cluster C as in (C, V)),
and C1 = {r : N, r 6|= α}. Simply, restrict R and U to C1 ∪C2 , respectively resulting in T
and V. Finally, arrange S in a way that would satisfy all the frame constraints of MLF.
Thus, (C, V) is clearly an F∗ -model. By the minimal model definition, (C, V) |= α. Then,
Proposition 7.1 and () imply that (C, V), x |=MLF∗ tr(α) for every x ∈ C2 , and for every y ∈
C1 , (C, V), y |=MLF∗ ¬tr(α). As (C, V) is an F∗ -model, we have (C, V), x |=MLF∗ [S]¬tr(α)
for every x ∈ C2 . As a result, (C, V), x |=MLF∗ tr(α) ∧ [S]¬tr(α) for every x ∈ C2 . Since C2
is a cluster which is a final cone, we further have (C, V), x |=MLF∗ [T](tr(α) ∧ [S]¬tr(α))
for each x ∈ C2 . From (H), it also follows that (C, V), x |=MLF∗ [T]tr(β) for every x ∈ C2 .
Clearly, tr(β) is also valid in C2 . Finally, Proposition 7.1 implies that (C, V) |= β in S4F.
Corollary 4. For α ∈ LS4F , α has a minimal model if and only if [T](tr(α) ∧ [S]¬tr(α))
is satisfiable in MLF∗ . (hint: take β = ⊥ in Theorem 2.)
4 Relation to other nonmonotonic formalisms
In this section, we briefly discuss a general strategy, unifying some major nonmono-
tonic reasonings among which are autoepistemic logic (AEL) [31], reflexive autoepis-
temic logic (RAEL) [23], equilibrium logic (and so ASP), and nonmonotonic S4F. The
emphasis is on the 2-floor semantics; the second floor charaterises the minimal model
of a formula, and the first floor checks the minimality criterion. This approach can be
generalised to other formalisms such as default logic [32] and MBNF [33] as there ex-
ists a good amount of research in the literature, studying such relations [34,35,36,15].
In particular, nonmonotonic S4F and default logic has a strong connection as it is ex-
plained and analysed in [14,15]. So, the MLF∗ encoding of nonmonotonic S4F leads
the potential encoding of default logic.
AEL and RAEL [21,23] are the nonmonotonic variants [22] of respectively the
modal logics KD45 and SW5 [9,29]. We have recently proposed two new monotonic
modal logics called MAE∗ and MRAE∗ , respectively capturing AEL and RAEL. They
are obtained from MLF∗ by replacing only the axioms characterising S4F (i.e., S, 4,
F) by ones, characterising respectively KD45 and SW5 (i.e., groups of axioms D, 4, 5
and T, 4, W5). The models of MAE∗ , MRAE∗ , and MLF∗ are all composed of a union
of 2-floor structures: in each, the second floor is a maximal cluster which is a final
cone of the 2-floor part of the model; where they differ is the structure of the first floor.
While a first floor in MLF∗ is a maximal cluster, that of MAE∗ contains irreflexive and
isolated worlds w.r.t. the T -relation (in a sense that, any two different worlds of the
first floor are not related to each other by the accessibility relation T ). Moreover, the
MRAE∗ models are nothing, but the reflexive closures of the MAE∗ models w.r.t. the
relation T . Interestingly, the same mechanism applied to S4F performs successfully
for KD45 and SW5 as well when everything else remains the same: the implication
[T] tr(α) ∧ [S]¬tr(α) → [T]tr(β), capturing nonmonotonic consequence of S4F, and
the formula hTi[T] tr(α) ∧ [S]¬tr(α) characterising minimal model semantics in S4F
perfectly work for the nonmonotonic variants of KD45 and SW5 as well.
Our research has also a large overlap with [8], embedding equilibrium logic (and so,
ASP) into a monotonic bimodal logic called MEM. The models of MEM are roughly
described in the introduction. The main result of this paper is also given via a similar
implication: the validity of tr(α) ∧ [S]¬tr(α) → tr(β) in MEM captures the nonmono-
tonic consequence, α |≈ β, of equilibrium logic. However, it is easy to check that the
formula [T] tr(α) ∧ [S]¬tr(α) → [T]tr(β) of this paper also gives the same result. This
analogy between all these works enables us to classify MEM under the same approach.
Still, we need to provide a stronger result that would help reinforce the relations be-
tween MEM and MLF∗ . For instance, [14] proves that the well-known Gödel’s trans-
lation into the modal logic S4 is still valid for translating the logic of here-and-there (a
3-valued monotonic logic on which equilibrium logic is built) [37,25] into the modal
logic S4F. A natural question that may arise is whether a similar translation can be used
to encode MEM into MLF∗ , which is the subject of a future work.
5 Conclusion and further research
In this paper, we design a novel monotonic modal logic, namely MLF∗ , that captures
nonmonotonic S4F. We demonstrate this embedding by translating the language of S4F
into that of MLF∗ . This way, we see that MLF∗ is able to characterise the existence of
a minimal model as well as logical consequence in nonmonotonic S4F.
Our work provides an alternative to Levesque’s monotonic bimodal logic of only
knowing [38,4,5,6], by which he captures four kinds of nonmonotonic logic, including
autoepistemic logic: his language has two modal operators, namely B and N. B is similar
to [T]. N is characterised by the complement of the relation, interpreting B. Levesque’s
frame constraints on the accessibility relation differ from ours, and he identifies the
nonmonotonic consequence ‘α |≈ β’ with the implication
B tr(α) ∧ N ¬tr(α) → B tr(β).
Levesque attacked the same problem with an emphasis on the only knowing notion.
However, his reasoning does not attempt to unify, and does not provide a general mech-
anism either. In particular, he applied his approach to neither SW5 nor S4F.
As a future work, we will implement this general methodology to capture mini-
mal model reasoning, underlying many other nonmonotonic formalisms. This paper,
together with other works on KD45, SW5, and ASP [8] stand a very strong initiative
by their possible straightforward implementations to different kinds of nonmonotonic
formalisms of similar floor-based semantics. Such research will then enable us to com-
pare various forms of nonmonotonic formalisms in a single monotonic modal setting.
References
1. Chen, J.: The logic of only knowing as a unified framework for non-monotonic reasoning.
Fundamenta Informaticae 21(3) (1994) 205–220
2. Chen, J.: Relating only knowing to minimal belief and negation as failure. Journal of Exper-
imental and Theoretical Artificial Intelligence 6(4) (1994) 409–429
3. Chen, J.: The generalized logic of only knowing (GOL) that covers the notion of epistemic
specifications. Journal of Logic and Computation 7(2) (1997) 159–174
4. Lakemeyer, G., Levesque, H.J.: Only-knowing: taking it beyond autoepistemic reasoning. In
Veloso, M.M., Kambhampati, S., eds.: Proceedings of the 20th National Conference on Arti-
ficial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference,
AAAI Press (2005) 633–638
5. Lakemeyer, G., Levesque, H.J.: Towards an axiom system for default logic. In: Proceedings
of the Twenty-First National Conference on Artificial Intelligence and the 18th Innovative
Applications of Artificial Intelligence Conference, AAAI Press (2006) 263–268
6. Lakemeyer, G., Levesque, H.J.: Only-knowing meets nonmonotonic modal logic. In Brewka,
G., Eiter, T., McIlraith, S.A., eds.: Proceedings of the Thirteenth International Conference on
Principles of Knowledge Representation and Reasoning, AAAI Press (2012) 350–357
7. Fariñas del Cerro, L., Herzig, A., Su, E.I.: Combining equilibrium logic and dynamic logic.
In Cabalar, P., Son, T.C., eds.: Proceedings of the Twelfth International Conference on Logic
Programming and Nonmonotonic Reasoning. Volume 8148 of Lecture Notes in Computer
Science., Springer (2013) 304–316
8. Fariñas del Cerro, L., Herzig, A., Su, E.I.: Capturing equilibrium models in modal logic.
Journal of Applied Logic 12(2) (2014) 192–207
9. Hughes, G.E., Cresswell, M.J.: A new introduction to modal logic. Psychology Press (1996)
10. Segerberg, K.: An essay in classical modal logic. Filosofiska studier. Filosofiska föreningen
och Filosofiska institutionen vid Uppsala universitet (1971)
11. Truszczyński, M.: Embedding default logic into modal nonmonotonic logics. In: Proceed-
ings of the First International Workshop on Logic Programming and Nonmonotonic Reason-
ing. (1991) 151–165
12. Schwarz, G.F., Truszczyński, M.: Modal logic S4F and the minimal knowledge paradigm. In
Moses, Y., ed.: Proceedings of the Fourth Conference on Theoretical Aspects of Reasoning
about Knowledge, Morgan Kaufmann Publishers Inc., Morgan Kaufmann (1992) 184–198
13. Schwarz, G., Truszczyński, M.: Minimal knowledge problem: a new approach. Artificial
Intelligence 67(1) (1994) 113–141
14. Cabalar, P., Lorenzo, D.: New insights on the intuitionistic interpretation of default logic.
In de Mántaras, R.L., Saitta, L., eds.: Proceedings of the Sixteenth European Conference on
Artificial Intelligence, IOS Press (2004) 798–802
15. Truszczyński, M.: The modal logic S4F, the default logic, and the logic here-and-there.
In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence. (2007)
508–514
16. Pearce, D., Uridia, L.: A logic related to minimal knowledge. In Esteva, M., Fernndez, A.,
Giret, A., eds.: Proceedings of the 2nd Workshop on Agreement Technologies (WAT-2009),
Sevilla, Spain, November 9, 2009. Volume 635. (2009)
17. Pearce, D., Uridia, L.: An approach to minimal belief via objective belief. In: Proceedings of
the 22nd International Joint Conference on Artificial Intelligence. Volume 22., AAAI Press
(2011) 1045–1050
18. Su, E.I.: A monotonic view on reflexive autoepistemic reasoning. In Balduccini, M., Jan-
hunen, T., eds.: Proceedings of the 14th International Conference on Logic Programming and
Nonmonotonic Reasoning, LPNMR 2017, Espoo, Finland, July 3-6, 2017. Volume 10377 of
Lecture Notes in Computer Science., Springer, Springer (2017) 85–100
19. Konolige, K.: Autoepistemic logic. In Gabbay, D.M., Hogger, C.J., Robinson, J.A., eds.:
Handbook of Logic in Artificial Intelligence and Logic Programming. Volume 3., New York,
NY, USA, Oxford University Press, Inc. (1994) 217–295
20. Marek, V. Wiktor, T.M.: Reflexive autoepistemic logic and logic programming. In: Pro-
ceedings of the Second International Workshop on Logic Programming and Non-Monotonic
Reasoning, MIT Press (1993) 115–131
21. Schwarz, G.F.: Autoepistemic logic of knowledge. In: Proceedings of the First International
Workshop on Logic Programming and Nonmonotonic Reasoning, MIT Press (1991) 260–
274
22. Schwarz, G.F.: Minimal model semantics for nonmonotonic modal logics. In: Proceedings
of the Seventh Annual Symposium on Logic in Computer Science, IEEE Computer Society
Press (1992) 34–43
23. Schwarz, G.F.: Reflexive autoepistemic logic. Fundamenta Informaticae 17(1-2) (1992)
157–173
24. Pearce, D.: A new logical characterisation of stable models and answer sets. In Dix, J.,
Pereira, L.M., Przymusinski, T.C., eds.: Non-Monotonic Extensions of Logic Programming,
NMELP ’96, Bad Honnef, Germany, September 5-6, 1996, Selected Papers. Volume 1216 of
Lecture Notes in Computer Science., Springer (1996) 57–70
25. Pearce, D.: Equilibrium logic. Annals of Mathematics and Artificial Intelligence 47(1-2)
(2006) 3–41
26. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In Kowal-
ski, R.A., Bowen, K.A., eds.: Proceedings of the Fifth International Conference on Logic
Programming, MIT Press (1988) 1070–1080
27. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases.
New Generation Computing 9(3/4) (1991) 365–386
28. Baral, C.: Knowledge representation, reasoning and declarative problem solving. Cambridge
University Press, New York, NY, USA (2003)
29. Blackburn, P., de Rijke, M., Venema, Y.: Modal logic. Volume 53. Cambridge University
Press, Cambridge Tracts in Theoretical Computer Science (2002)
30. Marek, V.W., Truszczyński, M.: Nonmonotonic logic: context-dependent reasoning.
Springer (1993)
31. Moore, R.C.: Autoepistemic logic revisited. Artificial Intelligence 59(1-2) (1993) 27–30
32. Reiter, R.: A logic for default reasoning. Artificial Intelligence 13(1-2) (1980) 81–132
33. Lifschitz, V.: Minimal belief and negation as failure. Artificial Intelligence 70(1-2) (1994)
53–72
34. Truszczyński, M.: Modal interpretations of default logic. In Mylopoulos, J., Reiter, R., eds.:
Proceedings of the 12th International Joint Conference on Artificial Intelligence, Morgan
Kaufmann (1991) 393–398
35. Lifschitz, V., Schwarz, G.: Extended logic programs as autoepistemic theories. In Pereira,
L.M., Nerode, A., eds.: Proceedings of the Second International Workshop on Logic Pro-
gramming and Non-monotonic Reasoning, MIT Press (1993) 101–114
36. Schwarz, G.: On embedding default logic into Moore’s autoepistemic logic. Artificial Intel-
ligence 80(1-2) (1996) 349–359
37. Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzungsber. preuss. Akad.
Wiss. 42-71 (1930) 158–169
38. Levesque, H.J.: All I know: a study in autoepistemic logic. Artificial intelligence 42(2-3)
(1990) 263–309