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