Adding Standpoint Modalities to Non-Monotonic S4F: Preliminary Results Piotr Gorczyca1,*,† , Hannes Strass1,† 1 Computational Logic Group, Institute of Artificial Intelligence, Faculty of Computer Science, TU Dresden, Germany Abstract Standpoint logics allow to represent multiple heterogeneous viewpoints in a unifying framework based on modal logic. We propose to combine standpoint modalities with the single modality of the non-monotonic modal logic S4F, thus defining standpoint S4F. The resulting language allows to express semantic commitments based on default reasoning. We define syntax and semantics of the logic, study the computational complexity of reasoning problems in the fragment of simple theories, and showcase standpoint S4F by exemplifying two concrete instantiations of the general language – standpoint default logic and standpoint argumentation frameworks. Keywords Standpoint Logic, Modal Logic S4F, Default Logic 1. Introduction that the overall formalism becomes non-monotonic with respect to its logical conclusions. Standpoint logic is a modal logic-based formalism for repres- Several non-monotonic formalisms that could be em- enting multiple diverse (and potentially conflicting) view- ployed for default reasoning within standpoints come to points within a single framework. Its main appeal derives mind, and obvious criteria for selection among the can- from its conceptual simplicity and its attractive properties: didates are not immediate. We choose to employ the non- In the presence of conflicting information, standpoint logic monotonic modal logic S4F [3, 4], which is a very general sacrifices neither consistency nor logical conclusions about formalism that subsumes several other NMR languages, de- the shared understanding of common vocabulary [1]. The cidedly allowing the possibility for later specialisation via underlying idea is to start from a base logic (originally pro- restricting to proper fragments. The usefulness of non- positional logic [1]) and to enhance it with two modalities monotonic S4F for knowledge representation and especially pertaining to what holds according to certain standpoints. non-monotonic reasoning has been aptly demonstrated by There, a standpoint is a specific point of view that an agent Schwarz and Truszczyński [4] (among others), but seems to or other entity may have, and that may have a bearing on be underappreciated in the literature to this day. In our case, how the entity understands and employs a given logical employing S4F as base language for standpoint logic entails, vocabulary (that may at the same time be used by other as easy corollary, for example standpoint default logic, a entities with a potentially different understanding). The standpoint variant of Reiter’s default logic [5], where de- two modalities are, respectively: faults and definite knowledge can be annotated with stand- point modalities. In Example 1, the annotated defaults are • □s 𝜑, expressing: of the standard form, namely 𝜙 : 𝜓1 , . . . , 𝜓𝑛 /𝜓, where (as “it is unequivocal [from the point of view s] that 𝜑”; usual) if the prerequisite 𝜙 is believed to be true and the justifications 𝜓1 , . . . , 𝜓𝑛 are consistent with one’s current • ♢s 𝜑, expressing: beliefs, the consequence 𝜓 can be concluded. “it is conceivable [from the point of view s] that 𝜑”. Example 1. Coffee is consumed differently in different Standpoint logic escapes global inconsistency by keeping parts of the world – what is considered to be a “typical conflicting pieces of knowledge separate, yet avoids duplic- coffee” varies among countries. Usually (*) it is consumed ation of vocabulary and in this way conveniently keeps hot, however in Vietnam ( ) iced coffee is a more common portions of common understanding readily available. It choice. Apart from the temperature, in Italy ( ), one of has its history and roots within the philosophical theory the most popular coffee drinks – espresso – is much higher of supervaluationism [2], stating that semantic variability in caffeine than the typically filtered coffee popular in the “can be explained by the fact that natural language can be US ( ). The above considerations could be formalised interpreted in many different yet equally acceptable ways, using standpoint defaults as follows: commonly referred to as precisifications” [1]. [︁ ]︁ [︁ ]︁ In our work, such semantic commitments can be made, as □* coffee : hot/hot , □ coffee : iced /iced , is often done, on the basis of incomplete knowledge using a [︁ coffee : espresso/espresso , ]︁ □ form of default reasoning. Consequently, in our work each [︁ ]︁ precisification embodies a consistent (but possibly partial) □ coffee : low _caffeine/low _caffeine ♢ viewpoint on what can be known, potentially using non- monotonic reasoning (NMR) to arrive there. This entails Several monotonic logics have been “standpointified” so far: Apart from propositional logic in the original work of Gómez 22nd International Workshop on Nonmonotonic Reasoning, November 2–4, Álvarez and Rudolph [1], also first-order logic and vari- 2024, Hanoi, Vietnam ous fragments thereof [6] as well as the description logics * Corresponding author. † 𝒮ℛ𝒪ℐ𝒬 [6], ℰℒ+ [7, 8], and 𝒮ℋℐ𝒬 [9], and the temporal These authors contributed equally. logic LTL [10]. We add the first non-monotonic logic to the $ piotr.gorczyca@tu-dresden.de (P. Gorczyca); hannes.strass@tu-dresden.de (H. Strass) realm of standpoint logics, that is, the first standpoint logic  0000-0002-6613-6061 (P. Gorczyca); 0000-0001-6180-6452 (H. Strass) where the points of view embodied by standpoints can be © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribu- tion 4.0 International (CC BY 4.0). obtained by reasoning in a non-monotonic fashion. CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings More specifically, in this paper, we introduce the syntax (𝑊, {𝑅s }s∈𝒮 , 𝑣), where the worlds 𝑊 are given by the and semantics of standpoint S4F. We analyse the computa- precisifications Π, the evaluation function 𝑣 is given by 𝛾, tional complexity of its associated reasoning problems and and the reachability relation among worlds for a standpoint show that reasoning does not become harder (than in the name (i.e., modality) s ∈ 𝒮 is simply 𝑅s = Π × 𝜎(s). base logic) through the addition of standpoint modalities. Finally, we demonstrate some of the more concrete stand- 2.2. Modal Logic S4F point formalisms we obtain as corollaries, more specific- ally standpoint default logic and standpoint argumentation S4F is a propositional modal logic with a single modality frameworks. We conclude with a discussion of future work. K, read as “knows”. It was studied in depth by Seger- berg [3]; we base our study on the works of Schwarz and Truszczyński [11, 12, 13, 4]. We again start from a proposi- 2. Background tional vocabulary 𝒜. The syntax of the modal logic S4F ℒK is given by All languages we henceforth consider build on propositional logic, denoted ℒ, and built from a set 𝒜 of atoms according 𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | K𝜙 to 𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 where 𝑝 ∈ 𝒜. Its model-theoretic semantics is given by interpretations 𝐼 ⊆ 𝒜 containing with 𝑝 ∈ 𝒜. For formulas 𝜙 ∈ ℒK without occurrences of exactly the true atoms, and we denote satisfaction of a for- K, we write 𝜙 ∈ ℒ and call them objective formulas. mula 𝜙 by an interpretation 𝐼 by 𝐼 ⊩ 𝜙, and entailment of Truszczyński [14] introduced a useful fragment of S4F, a formula 𝜙 by a set 𝑇 of formulas by 𝑇 |= 𝜙. The provab- so-called modal defaults. There, the base case of formula ility relation for propositional logic is denoted by ⊢ (where induction is not a propositional atom as above, but of the 𝑇 ⊢ 𝜙 means that from 𝑇 , we can derive 𝜙) and assumed form K𝜓 for 𝜓 ∈ ℒ a formula of propositional logic. More to be given by some standard proof system that is sound formally, a modal default is built via and complete (that is, where 𝑇 ⊢ 𝜙 iff 𝑇 |= 𝜙). 𝜙 ::= K𝜓 | ¬𝜙 | 𝜙 ∧ 𝜙 | K𝜙 2.1. Standpoint Logic with 𝜓 ∈ ℒ. The fragment of modal defaults is still ex- Standpoint Logic was introduced by Gómez Álvarez and pressive enough for our desired applications in knowledge Rudolph [1] as a modal logic-based formalism for repres- representation and reasoning, so we will mostly restrict our enting multiple (potentially contradictory) perspectives in attention to modal defaults later on. a single framework. Building upon propositional logic, in The semantics of S4F is given by S4F structures, tuples addition to a set 𝒜 of propositional atoms, it uses a set 𝒮 ℳ = (𝑉, 𝑊, 𝜉) where 𝑉 and 𝑊 are disjoint sets of worlds of standpoint names, where a standpoint represents a point with 𝑊 ̸= ∅, and 𝜉 : 𝑉 ∪ 𝑊 → 2𝒜 assigns to each world 𝑤 of view an agent or other entity can take, and * ∈ 𝒮 is a propositional interpretation 𝜉(𝑤) ⊆ 𝒜. The satisfaction a designated special standpoint, the universal standpoint. relation ℳ, 𝑤 ⊩ 𝜙 for 𝑤 ∈ 𝑉 ∪ 𝑊 is defined by induction: Formally, the syntax of propositional standpoint logic ℒS is given by ℳ, 𝑤 ⊩ 𝑝 :⇐⇒ 𝑝 ∈ 𝜉(𝑤) 𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | □s 𝜙 ℳ, 𝑤 ⊩ ¬𝜙 :⇐⇒ ℳ, 𝑤 ̸⊩ 𝜙 where 𝑝 ∈ 𝒜, and s ∈ 𝒮 is a standpoint name. We allow the ℳ, 𝑤 ⊩ 𝜙1 ∧ 𝜙2 :⇐⇒ ℳ, 𝑤 ⊩ 𝜙1 and ℳ, 𝑤 ⊩ 𝜙2 notational shorthands 𝜙 ∨ 𝜓, 𝜙 → 𝜓, and ♢s 𝜙 := ¬□s ¬𝜙. ℳ, 𝑤 ⊩ K𝜙 :⇐⇒ The semantics of standpoint logic is given by standpoint ® ℳ, 𝑣 ⊩ 𝜙 for all 𝑣 ∈ 𝑉 ∪ 𝑊, if 𝑤 ∈ 𝑉, structures 𝒩 = (Π, 𝜎, 𝛾), where Π is a non-empty set of precisifications, 𝜎 : 𝒮 → 2Π assigns a set of precisifica- ℳ, 𝑣 ⊩ 𝜙 for all 𝑣 ∈ 𝑊, otherwise. tions to each standpoint name (with 𝜎(*) = Π fixed), and A pointed S4F structure ℳ, 𝑤 is a model of a formula 𝜙 𝛾 : Π → 2𝒜 assigns a propositional interpretation to each iff ℳ, 𝑤 ⊩ 𝜙; ℳ, 𝑤 is a model of a theory 𝑇 ⊆ ℒK iff precisification. The relation 𝒩 , 𝜋 ⊩ 𝜙, indicating that the ℳ, 𝑤 ⊩ 𝜙 for all 𝜙 ∈ 𝑇 . A formula 𝜙 ∈ ℒK is satisfiable structure 𝒩 = (Π, 𝜎, 𝛾) satisfies formula 𝜙 (at point 𝜋), is iff there exists an S4F structure ℳ = (𝑉, 𝑊, 𝜉) and a world defined by induction: 𝑤 ∈ 𝑉 ∪ 𝑊 such that (𝑉, 𝑊, 𝜉) , 𝑤 ⊩ 𝜙 (likewise for 𝒩,𝜋 ⊩ 𝑝 :⇐⇒ 𝑝 ∈ 𝛾(𝜋) theories 𝑇 ). An S4F structure (𝑉, 𝑊, 𝜉) is a model of a formula 𝜙 ∈ ℒK (theory 𝑇 ⊆ ℒK ), written (𝑉, 𝑊, 𝜉) ⊩ 𝜙 𝒩 , 𝜋 ⊩ ¬𝜙 :⇐⇒ 𝒩 , 𝜋 ̸⊩ 𝜙 (ℳ ⊩ 𝑇 ) iff for all 𝑤 ∈ 𝑉 ∪ 𝑊 , we have (𝑉, 𝑊, 𝜉) , 𝑤 ⊩ 𝜙 𝒩 , 𝜋 ⊩ 𝜙1 ∧ 𝜙2 :⇐⇒ 𝒩 , 𝜋 ⊩ 𝜙1 and 𝒩 , 𝜋 ⊩ 𝜙2 (for each 𝜙 ∈ 𝑇 ). A formula 𝜙 ∈ ℒK is entailed by a theory 𝒩 , 𝜋 ⊩ □s 𝜙 :⇐⇒ 𝒩 , 𝜋 ′ ⊩ 𝜙 for all 𝜋 ′ ∈ 𝜎(s) 𝑇 , written 𝑇 |=S4F 𝜙, iff every model of 𝑇 is a model of 𝜙. S4F structures can also be seen as a restricted form of As usual, a standpoint structure (Π, 𝜎, 𝛾) is a model for a ordinary Kripke structures (𝑉 ∪ 𝑊, 𝑅, 𝜉) with reachabil- formula 𝜙 iff (Π, 𝜎, 𝛾) ⊩ 𝜙; a formula 𝜙 ∈ ℒS is satisfiable ity relation 𝑅 := (𝑉 × 𝑉 ) ∪ (𝑉 × 𝑊 ) ∪ (𝑊 × 𝑊 ). Intu- iff there exist (Π, 𝜎, 𝛾) and 𝜋 ∈ Π with (Π, 𝜎, 𝛾) , 𝜋 ⊩ 𝜙.1 itively, an S4F structure consists of two clusters of fully inter- Standpoint structures can be regarded as a restric- connected worlds, the inner worlds 𝑊 and outer worlds 𝑉 . ted form of ordinary (multi-modal) Kripke structures The outer worlds 𝑉 can reach all (inner and outer) worlds, while the inner worlds 𝑊 can only reach all inner worlds. 1 Original standpoint logic [1] also offered sharpening statements, ex- The entailment relation |=S4F has a proof-theoretic char- pressions of the form s ⪯ u indicating that every precisification acterisation ⊢S4F based on necessitation and axiom schemata subscribing to s must also subscribe to u as realised by their formal K, T, 4, and F,2 with 𝐹 being (𝜙 ∧ MK𝜓) → M(K𝜙 ∨ 𝜓), semantics 𝜎(s) ⊆ 𝜎(u). We disregard sharpening statements in this 2 work for clarity of exposition; they could be added without difficulty. This also explains the name S4F, as S4 is characterised by K, T, and 4. where M𝜑 abbreviates ¬K¬𝜑. efficiently constructed due to potentially containing expo- nentially many worlds (w.r.t. the input theory). Towards 2.3. Non-Monotonic S4F minimisation of knowledge, note that the set Φ needs to be maximal, so that the set of known formulas Ψ is restricted A non-monotonic logic can be obtained by restricting atten- to only what is absolutely necessary. tion to models where what is known is minimal. As defined The procedure for existenceS4F work as follows: Given a by Schwarz and Truszczyński [4, Definitions 3.2 and 3.3], an theory 𝐴 ⊆ ℒK , we guess a partitioning of 𝐴K into (Φ, Ψ). S4F structure ℳ = (𝑉, 𝑊, 𝜉) is said to be strictly preferred Based on this pair, we define the set over another S4F structure 𝒦 = (𝑉 ′ , 𝑊, 𝜉 ′ ) iff 𝑉 ′ = ∅, 𝜉 ′ ⊇ 𝜉,3 and for some 𝜓 ∈ ℒ, we have 𝒦 ⊩ 𝜓 but ℳ ̸⊩ 𝜓. Θ = 𝐴 ∪ {¬K𝜙 | 𝜙 ∈ Φ} ∪ {K𝜓 | 𝜓 ∈ Ψ} ∪ Ψ We say that 𝒦 is a minimal model of a theory 𝑇 ⊆ ℒK iff (1) 𝒦 is a model of 𝑇 , and (2) there is no model ℳ of 𝑇 that which is interpreted as a theory of ⃓ propositional logic over an extended signature 𝒜 ∪ K𝜑 ⃓ 𝜑 ∈ 𝐴K , that is, where {︁ }︁ is strictly preferred over 𝒦. So if ℳ is strictly preferred over 𝒦, then there is a pro- subformulas of the form K𝜑 are treated as propositional positional formula 𝜓 ∈ ℒ such that (1) 𝒦, 𝑤 ⊩ 𝜓 for all atoms. Then, we verify whether the guessed pair is intro- 𝑤 ∈ 𝑊 , and (2) there is a 𝑤′ ∈ 𝑉 such that ℳ, 𝑤′ ̸⊩ 𝜓. spection consistent [13], that is, whether: For a minimal model of a theory 𝑇 , all strictly preferred structures violate some formula of 𝑇 . (C1) Φ ∪ Ψ = 𝐴K and Φ ∩ Ψ = ∅; Intuitively, 𝒦 having a strictly preferred alternative (C2) Θ is propositionally consistent; means that the knowledge of 𝒦 is not minimal. We note that a minimal model (𝑉, 𝑊, 𝜉) has 𝑉 = ∅ by definition, (C3) for each 𝜑 ∈ Φ, we have Θ ̸⊢ 𝜑 (where ⊢ denotes and thus is an S5 structure, that is, a set of worlds with a the provability relation of propositional logic). universal accessibility relation. Afterwards we check whether the introspection consistent pair (Φ, Ψ) corresponds to a minimal S4F model of 𝐴 [13, 2.4. Complexity of Non-Monotonic S4F condition (2)], by checking if for every 𝜓 ∈ Ψ, we have Schwarz and Truszczyński [13] provide complexity results for decision problems associated with non-monotonic S4F. 𝐴 ∪ {¬K𝜑 | 𝜑 ∈ Φ} ⊢S4F 𝜓. The problems are defined w.r.t. a finite S4F theory 𝐴 ⊆ ℒK The containment proof relies on the fact that S4F provabil- and a formula 𝜙 ∈ ℒK and can be summarized as follows: ity (Is a formula 𝜙 S4F-provable from a given finite set of • existenceS4F : Does 𝐴 have a minimal model? premises 𝐴 ⊆ ℒK ?) is in NP [13]. Since the number of calls to an NP-oracle is polynomial, existenceS4F is in ΣP2 . A • in-someS4F : Is there a minimal model ℳ of 𝐴, such matching lower bound follows from the faithful embedding that ℳ ⊩ 𝜙? of default logic [5] into S4F, which will be covered in the • not-in-allS4F :4 Is there a minimal model ℳ of 𝐴, next subsection. such that ℳ ̸⊩ 𝜙? 2.5. S4F in Knowledge Representation • in-allS4F : Does ℳ ⊩ 𝜙 hold for every minimal model ℳ of 𝐴? The logic S4F is immensely useful for knowledge repres- The above reasoning tasks were found to reside on the entation purposes [13, 4], as it allows to naturally embed second level of the polynomial hierarchy, with the first three several non-monotonic logics. Among others, it subsumes being ΣP2 -complete and the last one ΠP2 -complete. We re- the (bimodal) logic of GK by Lin and Shoham [15] as well as call the proof idea by Schwarz and Truszczyński [13] of the (bimodal) logic of MKNF by Lifschitz [16], all while be- existenceS4F given an S4F theory 𝐴 ⊆ ℒK below. ing unimodal and thus arguably having a simpler semantics. Let 𝐴K = {𝜙 | K𝜙 ∈ Sub(𝐴)}, where Sub(𝐴) denotes In the following subsections, we briefly sketch how several the set of all subformulas of formulas in 𝐴. Note that given well-known knowledge representation formalisms can be any minimal S4F model ℳ of 𝐴, which necessarily is an recovered in S4F, and note especially that all of them stay S5 structure, and a formula 𝜙 ∈ ℒK , due to the universal within the fragment of modal defaults. accessibility relation it is the case that either ℳ ⊩ K𝜙 or ℳ ⊩ ¬K𝜙. Then, there has to be a subset Ψ ⊆ 𝐴K , such 2.5.1. Default Logic that ℳ ⊩ K𝜓 and ℳ ⊩ 𝜓 for all 𝜓 ∈ Ψ. For the remain- ing elements of 𝐴K , namely 𝜑 ∈ Φ := 𝐴 ∖ Ψ then it has Most importantly, the default logic of Reiter [5] can be faith- to hold that ℳ ⊩ ¬K𝜑. The minimal models of a theory fully and modularly embedded into S4F [11]: For a default 𝐴 can therefore be compactly represented by partitionings 𝜙 : 𝜓1 , . . . , 𝜓𝑛 /𝜓, the corresponding S4F formula is given (Φ, Ψ) of 𝐴K . Such a sparse representation of a minimal by (K𝜙∧K¬K¬𝜓1 ∧. . .∧K¬K¬𝜓𝑛 ) → K𝜓. Modularly model is necessary, as the actual minimal model cannot be here means that a default theory can be translated default by default, without looking at the whole theory, something 3 We consider a function 𝑓 : 𝐴 → 𝐵 to be a relation 𝑓 ⊆ 𝐴 × 𝐵 that is functional, i.e., where for each 𝑎 ∈ 𝐴 there exists at most one that is not possible [17] when translating default logic into 𝑏 ∈ 𝐵 with (𝑎, 𝑏) ∈ 𝑓 . Consequently, then 𝑔 ⊇ 𝑓 for functions 𝑔 autoepistemic logic [18].5 Faithfully means that the exten- and 𝑓 simply means that 𝑔 assigns just as 𝑓 does, while 𝑔 may have a sions of the default theory are in one-to-one correspondence strictly larger domain. with the minimal models of the resulting S4F translation. (A 4 Note that for a general S4F formula 𝜙 (including objective formulas), 5 this task is not reducible to in-someS4F in a straightforward way by This is even more notable if we take into account that autoepistemic simply asking whether ¬𝜙 is satisfied in some minimal S4F model of logic can be seen as non-monotonic KD45 [4] in the nomenclature of 𝐴, as non-satisfaction does not imply satisfaction of the negation. McDermott and Doyle [19], McDermott [20]. similar translation exists for disjunctive default logic [21].) 2. 𝑆ℳ attacks 𝐴 ∖ 𝑆ℳ : We first show a helpful intermediate Deciding whether a propositional default theory has an ex- result: tension is ΣP2 -complete [22], thus providing the matching lower bound to S4F minimal model existence. Claim 1. For all 𝑎 ∈ 𝐴, we have ℳ ⊩ K𝑎 or ℳ ⊩ K¬𝑎. Proof of the claim. Assume ℳ ̸⊩ K¬𝑎. Then there ex- 2.5.2. Logic Programs ists a 𝑤 ∈ 𝑊 such that ℳ, 𝑤 ⊩ ¬K¬𝑎. Since ℳ In a similar vein, normal logic programs can be is an S5 structure, we get ℳ ⊩ K¬K¬𝑎. By defini- translated modularly into S4F [11, 4]: A rule tion, K¬K¬𝑎 → K𝑎 ∈ 𝑇𝐹 , thus by ℳ ⊩ 𝑇𝐹 we get 𝑝0 ← 𝑝1 , . . . , 𝑝𝑚 , ∼𝑝𝑚+1 , . . . , ∼𝑝𝑚+𝑛 becomes ℳ ⊩ K𝑎. ♢ (K𝑝1 ∧ . . . ∧ K𝑝𝑚 ∧ K¬K𝑝𝑚+1 ∧ . . . ∧ K¬K𝑝𝑚+𝑛 ) → K𝑝0 . The translation is faithful with respect to the Let 𝑎 ∈ 𝐴 ∖ 𝑆ℳ . Then ℳ ⊩ ̸ K𝑎, which by the claim stable model semantics. (This works similarly for means that ℳ ⊩ K¬𝑎. Assume to the contrary of what extended/disjunctive logic programs [23, 4].) we want to show that for all 𝑐 ∈ 𝐴 with (𝑐, 𝑎) ∈ 𝑅, we have 𝑐 ∈ / 𝑆ℳ , and consider any such 𝑐 ∈ 𝐴. Then, by definition of 𝑆ℳ we get ℳ ⊩ ̸ K𝑐. We now construct 2.5.3. Argumentation Frameworks 𝒩 = (𝑉, 𝑊, 𝜉 ∪ 𝜁) with 𝑉 = {𝑣} (w.l.o.g. 𝑣 ∈ / 𝑊 ) and Last but not least, also argumentation frameworks [24] (un- 𝜁(𝑣) = 𝑆ℳ ∪ {𝑎}. 𝒩 is strictly preferred to ℳ because der stable semantics) can be modularly and faithfully trans- 𝒩 , 𝑣 ̸⊩ ¬𝑎 while ℳ ⊩ ¬𝑎, therefore it remains to show lated into S4F. Given that argumentation frameworks (AFs) 𝒩 ⊩ 𝑇𝐹 to obtain the desired contradiction. To show this, can be modularly translated into normal logic programs we only need consider formulas involving 𝑎, for which there (over an extended vocabulary) using Dung’s translation [24, are three possibilities: Section 5; 25], we have the following straightforward result: a) 𝒩 ⊩ K¬K¬𝑎 → K𝑎: We have 𝒩 , 𝑤 ⊩ K¬𝑎 for Proposition 1. Given a (finite) argumentation framework any 𝑤 ∈ 𝑊 , whence 𝒩 , 𝑤 ̸⊩ ¬K¬𝑎 for all 𝑤 ∈ 𝑊 𝐹 = (𝐴, 𝑅), we define the following S4F theory: 𝑇𝐹 := and 𝒩 , 𝑥 ̸⊩ K¬K¬𝑎 for all 𝑥 ∈ 𝑉 ∪ 𝑊 . {K¬K¬𝑎 → K𝑎 | 𝑎 ∈ 𝐴} ∪ {K𝑎 → K¬𝑏 | (𝑎, 𝑏) ∈ 𝑅}. b) 𝒩 ⊩ K𝑎 → K¬𝑏: For any 𝑤 ∈ 𝑊 ̸= ∅, due to The stable extensions of 𝐹 and the minimal models of 𝑇𝐹 are 𝒩 , 𝑤 ⊩ ¬𝑎 we have 𝒩 , 𝑤 ̸⊩ K𝑎; we thus also get in one-to-one correspondence. 𝒩 , 𝑣 ̸⊩ K𝑎. Proof. Stable extension ⇝ minimal model: Let 𝑆 ⊆ 𝐴 be c) 𝒩 ⊩ K𝑐 → K¬𝑎: For all 𝑤 ∈ 𝑊 , we have ℳ, 𝑤 ̸⊩ a stable extension of 𝐹 . Define the S4F structure ℳ𝑆 = K𝑐 by assumption above, whence 𝒩 , 𝑤 ̸⊩ K𝑐 directly. (∅, {𝑤} , 𝜉) with 𝜉(𝑤) = 𝑆. We will show that ℳ𝑆 is a By 𝑐 ∈ / 𝑆ℳ , we also get 𝒩 , 𝑣 ̸⊩ K𝑐. □ minimal model of 𝑇𝐹 . 1. ℳ𝑆 is a model of 𝑇𝐹 : Intuitively, the first part of the theory asserts that argu- • Consider 𝜑 = K¬K¬𝑎 → K𝑎 ∈ 𝑇𝐹 . If 𝑎 ∈ 𝑆, then ments are accepted unless they are defeated, and the second ℳ𝑆 ⊩ K𝑎 and ℳ𝑆 ⊩ 𝜑. If 𝑎 ∈ / 𝑆, then ℳ𝑆 ⊩ K¬𝑎, part expresses that an argument is defeated whenever one whence ℳ𝑆 ̸⊩ K¬K¬𝑎 and ℳ𝑆 ⊩ 𝜑. of its attackers is accepted. • Consider 𝜑 = K𝑎 → K¬𝑏 ∈ 𝑇𝐹 . Then (𝑎, 𝑏) ∈ 𝑅 and since 𝑆 is stable, 𝑎 ∈ / 𝑆 or 𝑏 ∈ / 𝑆. If 𝑎 ∈ / 𝑆, then ℳ𝑆 ̸⊩ K𝑎 and ℳ𝑆 ⊩ 𝜑. If 𝑏 ∈ / 𝑆, then ℳ𝑆 ⊩ K¬𝑏 3. Standpoint S4F and ℳ𝑆 ⊩ 𝜑. Standpoint S4F is the nesting of S4F into standpoint logic. 2. ℳ𝑆 is minimal: Consider the S4F structure 𝒩 = More technically, in the nomenclature of many-dimensional (𝑉, {𝑤} , 𝜉 ′ ) to be strictly preferred to ℳ𝑆 . Then there modal logics [26], it is the product of the two logics above. exist 𝑣 ∈ 𝑉 and 𝜓 ∈ ℒ such that ℳ ⊩ 𝜓 and This means that in each precisification, we have an “ordin- 𝒩 , 𝑣 ̸⊩ 𝜓. In particular, 𝜉 ′ (𝑣) ̸= 𝜉 ′ (𝑤) = 𝜉(𝑤), say, ary” S4F structure with two sets of worlds, which altogether 𝜉 ′ (𝑣)(𝑎) ̸= 𝜉(𝑤)(𝑎) for 𝑎 ∈ 𝐴. come from a common pool of globally “available” possible • 𝑎 ∈ 𝑆. Then 𝜉(𝑤) ⊩ 𝑎 and 𝜉 ′ (𝑣) ⊩ ¬𝑎 and 𝒩 , 𝑣 ̸⊩ K𝑎. worlds. On the other hand, 𝒩 , 𝑤 ⊩ K𝑎 whence 𝒩 , 𝑣 ̸⊩ K¬𝑎 and 𝒩 , 𝑣 ⊩ K¬K¬𝑎. Therefore, 𝒩 , 𝑣 ̸⊩ K¬K¬𝑎 → 3.1. Syntax K𝑎 and thus 𝒩 ⊩ ̸ 𝑇𝐹 . • 𝑎 ∈ / 𝑆. Then 𝜉(𝑤) ⊩ ¬𝑎 and 𝜉 ′ (𝑣) ⊩ 𝑎. Since 𝑆 As before, we start out from a set 𝒮 of standpoint names is stable, there exists a 𝑐 ∈ 𝑆 with (𝑐, 𝑎) ∈ 𝑅. Thus and a set 𝒜 of propositional atoms. We intend the language K𝑐 → K¬𝑎 ∈ 𝑇𝐹 . It firstly holds that 𝒩 , 𝑣 ̸⊩ K¬𝑎. to be used to express what is known according to certain standpoints. This entails that nothing is known about the – 𝜉 ′ (𝑣) ⊩ 𝑐. Then 𝒩 , 𝑣 ⊩ K𝑐 and 𝒩 , 𝑣 ̸⊩ K𝑐 → K¬𝑎, standpoints, but that they are an outer layer that is intu- whence 𝒩 ⊩ ̸ 𝑇𝐹 . itively not accessible to the K modality. Accordingly, we – 𝜉 ′ (𝑣) ⊩ ¬𝑐. Then, since 𝑐 ∈ 𝑆, 𝒩 ⊩ ̸ 𝑇𝐹 can be shown restrict the ways the modalities can be nested already in the as in the case for 𝑎 ∈ 𝑆 above. syntax: while S4F modality K can be used in the scope of a standpoint modality □s , we disallow the reverse.6 Minimal model ⇝ stable extension: Let ℳ = (∅, 𝑊, 𝜉) be a minimal model of 𝑇𝐹 . Define 𝑆ℳ = {𝑎 ∈ 𝐴 | ℳ ⊩ K𝑎}. 1. 𝑆ℳ is conflict-free: Consider 𝑎 ∈ 𝑆ℳ with (𝑎, 𝑏) ∈ 𝑅. By definition of 𝑆ℳ we get ℳ ⊩ K𝑎. From ℳ ⊩ 𝑇𝐹 we get 6 While it would pose no technical obstacles to allow the reverse nest- ℳ ⊩ K𝑎 → K¬𝑏. Thus, ℳ ⊩ K¬𝑏, whence ℳ ⊩ ̸ K𝑏, ing in syntax and semantics, we choose this restriction to clarify the whence 𝑏 ∈ / 𝑆ℳ . intended use of SS4F. Definition 1. The language ℒSK of SS4F is built via: S, 𝜋, 𝑤 ⊩ 𝜙1 ∧ 𝜙2 :⇐⇒ S, 𝜋, 𝑤 ⊩ 𝜙1 and S, 𝜋, 𝑤 ⊩ 𝜙2 S, 𝜋, 𝑤 ⊩ K𝜙 :⇐⇒ 𝜙 ::= 𝜓 | ¬𝜙 | 𝜙 ∧ 𝜙 | □s 𝜙 S, 𝜋, 𝑤 ⊩ 𝜙 for all 𝑤′ ∈ 𝜁𝑜 (𝜋) ∪ 𝜁𝑖 (𝜋), if 𝑤 ∈ 𝜁𝑜 (𝜋), ′ ® where 𝜓 ∈ ℒK is a modal default, that is, S, 𝜋, 𝑤′ ⊩ 𝜙 for all 𝑤′ ∈ 𝜁𝑖 (𝜋), otherwise. 𝜓 ::= K𝜑 | ¬𝜓 | 𝜓 ∧ 𝜓 | K𝜓 S, 𝜋, 𝑤 ⊩ □s 𝜙 :⇐⇒ S, 𝜋 ′ , 𝑤′ ⊩ 𝜙 for all 𝜋 ′ ∈ 𝜎(s) and 𝑤′ ∈ 𝜁𝑜 (𝜋 ′ ) ∪ 𝜁𝑖 (𝜋 ′ ) ♢ with 𝜑 ∈ ℒ being a formula of propositional logic. ♢ So while objective formulas (those without any modal- We sometimes call formulas from ℒK ∖ℒ subjective (because ities) are evaluated in the world, subjective formulas are they depend on what is known), and those from ℒ objective evaluated with respect to a specific precisification, where formulas. For Boolean combinations, we allow the usual standpoint modalities are evaluated with respect to a set of abbreviations 𝜑∨𝜓 := ¬(¬𝜑∧¬𝜓) and 𝜑 → 𝜓 := ¬𝜑∨𝜓, precisifications according to the used standpoint symbol. and for the (standpoint and S4F) modalities we sometimes We say that: use their duals M𝜑 := ¬K¬𝜑 and ♢s 𝜑 := ¬□s ¬𝜑. Given an SS4F formula 𝜙 ∈ ℒSK , as before (for S4F) we • S, 𝜋, 𝑤 is a model for 𝜙 iff S, 𝜋, 𝑤 ⊩ 𝜙, denote the set of its subformulas by Sub(𝜙). The size of • S, 𝜋 is a model for 𝜙, written S, 𝜋 ⊩ 𝜙, iff a formula 𝜙 is defined as the number of its subformulas, (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋, 𝑤 ⊩ 𝜙 for all 𝑤 ∈ 𝜁𝑜 (𝜋) ∪ 𝜁𝑖 (𝜋), that is, ‖𝜙‖ := |Sub(𝜙)|. Both notions generalise in a straightforward way to theories 𝑇 ⊆ ℒSK . • S is a model for 𝜙, written S ⊩ 𝜙, iff An SS4F theory 𝑇 ⊆ ℒSK is simple iff every formula (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋 ⊩ 𝜙 for all 𝜋 ∈ Π. 𝜙 ∈ 𝑇 is of the form □s 𝜓 or ♢s 𝜓 for some 𝜓 ∈ ℒK . As usual, a standpoint S4F structure (Π, Ω, 𝜎, 𝜁, 𝛾) is a model for a theory 𝑇 , written (Π, Ω, 𝜎, 𝜁, 𝛾) ⊩ 𝑇 , iff 3.2. Semantics (Π, Ω, 𝜎, 𝜁, 𝛾) ⊩ 𝜙 for all 𝜙 ∈ 𝑇 . Likewise, a theory 𝑇 en- Definition 2. Consider a set 𝒜 of atoms and a set 𝒮 of tails a formula 𝜙, written 𝑇 |=SS4F 𝜙, iff every model of 𝑇 is standpoint names. A standpoint S4F structure is a tuple a model of 𝜙. We say that a formula 𝜙 ∈ ℒSK is satisfiable iff S = (Π, Ω, 𝜎, 𝜁, 𝛾) where there exists a standpoint S4F structure S = (Π, Ω, 𝜎, 𝜁, 𝛾), a precisification 𝜋 ∈ Π, and a world 𝑤 ∈ 𝜁𝑜 (𝜋) ∪ 𝜁𝑖 (𝜋) • Π is a non-empty set of precisifications, such that (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋, 𝑤 ⊩ 𝜙. • Ω is a non-empty set of worlds, 3.3. Non-Monotonic Semantics • 𝜎 : 𝒮 → 2Π assigns to each standpoint name a set of precisifications, As usual, a non-monotonic semantics can be obtained by re- stricting attention to models that are in some sense minimal. • 𝜁 : Π → 2Ω × 2Ω assigns to each precisification a Here, we require what we call local minimality, where know- pair of disjoint sets of worlds, where we denote ledge has to be minimal in each precisification (according 𝜁(𝜋) = (𝜁𝑜 (𝜋), 𝜁𝑖 (𝜋)) and require 𝜁𝑖 (𝜋) ̸= ∅, to the requirements of minimal S4F models), but the over- all structure of precisifications and extents of standpoint • 𝛾 : Ω → 2𝒜 assigns to each world a propositional names is allowed to freely vary. Before the minimisation of evaluation. ♢ knowledge at each precisification can be carried out, one first has to determine which of the (sub)formulas of the ori- The set Π of precisifications is as before in standpoint logic, ginal theory are relevant at that precisification. The formal in that each precisification represents one possible point of definitions follow. view an entity could have, and where each precisification can belong to one or more standpoints (via 𝜎). The function Definition 4 (Potentially relevant subformulas). 𝜁 assigns an S4F structure (𝜁𝑜 (𝜋), 𝜁𝑖 (𝜋), 𝛾) to each preci- Given a set Π of precisifications, a set 𝒮 of standpoint sification, with outer worlds 𝜁𝑜 (𝜋) and inner worlds 𝜁𝑖 (𝜋), names, a standpoint assignment function 𝜎 : 𝒮 → 2Π , and where worlds 𝑤 ∈ Ω can (but need not) be reused across a simple theory 𝑇 , we define the set of potentially relevant precisifications. As usual, by a propositional evaluation subformulas for a particular precisification 𝜋 ∈ Π as 𝛾(𝑤) ⊆ 𝒜 we mean that all and only the elements of 𝛾(𝑤) are those atoms that are evaluated as true. 𝑇𝜋□ = {𝜙 ∈ Sub(𝑇 ) | ∃s ∈ 𝒮 : 𝜋 ∈ 𝜎(s) and As is generally the case for Kripke structures, the eval- (□s 𝜙 ∈ 𝑇 or ♢s 𝜙 ∈ 𝑇 )} ♢ uation of a formula in a structure might depend on the “point” in the structure at which we evaluate the formula. The potentially relevant formulas will then be used for de- Since we now have a two-dimensional modal logic with S4F termining the non-monotonic semantics of simple theories, structures nested into standpoint structures, we use doubly in that they provide an upper bound on what can possibly pointed structures to clarify where in the nested structure be known in a precisification. we evaluate formulas. Definition 5 (Locally minimal model). For a simple Definition 3. Let S = (Π, Ω, 𝜎, 𝜁, 𝛾) be an SS4F struc- standpoint S4F theory 𝑇 , we say that S = (Π, Ω, 𝜎, 𝜁, 𝛾) ture, 𝜋 ∈ Π, and 𝑤 ∈ Ω. The satisfaction relation ⊩ for is a locally minimal model of 𝑇 iff (1) S ⊩ 𝑇 and (2) for □ pointed standpoint S4F structures is defined as follows: each (︁ 𝜋 ∈ Π there exists )︁ an S4F theory Ξ𝜋 ⊆ 𝑇𝜋 such that 𝜁𝑜 (𝜋), 𝜁𝑖 (𝜋), 𝛾|𝜁(𝜋) is a minimal S4F model for Ξ𝜋 .7 ♢ S, 𝜋, 𝑤 ⊩ 𝑝 :⇐⇒ 𝑝 ∈ 𝛾(𝑤) 7 For a function 𝑓 : 𝐴 → 𝐵 and a subset 𝐶 ⊆ 𝐴, we denote by 𝑓|𝐶 S, 𝜋, 𝑤 ⊩ ¬𝜙 :⇐⇒ S, 𝜋, 𝑤 ̸⊩ 𝜙 the function resulting from restricting the domain of 𝑓 to 𝐶 . Intuitively, for a precisification 𝜋 ∈ Π, the theory Ξ𝜋 for each formula of the form □u 𝛼 not satisfied in S a “witness” contains all standpoint-free formulas that are relevant at 𝜋. precisification 𝜋𝛼 ∈ 𝜎(u) such that S, 𝜋𝛼 ̸⊩ 𝛼 is contained Local (S4F) minimality then guarantees that in each pre- in Π′ , w.l.o.g. we can assume that 𝜋 ′ = 𝜋𝛼 and therefore cisification of the overall structure, there is no unjusti- 𝜋 ′ ∈ Π′ . Then also 𝜋 ′ ∈ 𝜎 ′ (s) and by induction hypothesis fied knowledge (w.r.t. the theory Ξ𝜋 ). Accordingly, non- we have that S′ , 𝜋 ′ ̸⊩ 𝜓 ′ and consequently S′ ̸⊩ □s 𝜓 ′ , monotonic entailment can then be defined as usual, that is, which concludes the proof of the intermediate result. with respect to locally minimal models only. Since 𝜙 ∈ Sub(𝜙) and S ⊩ 𝜙 we get S, 𝜋 ⊩ 𝜙 for every 𝜋 ∈ Π. Naturally, since Π′ ⊆ Π also S, 𝜋 ′ ⊩ 𝜙 for Definition 6. Given a standpoint S4F theory 𝑇 ⊆ ℒSK every 𝜋 ′ ∈ Π′ . Then by our intermediate result we get that that is simple, we say that a formula 𝜙 ∈ ℒSK is: S′ , 𝜋 ′ ⊩ 𝜙 for every 𝜋 ′ ∈ Π′ and consequently S′ ⊩ 𝜙. □ 1. sceptically entailed by 𝑇 , written 𝑇 |≈scep 𝜙, iff S ⊩ 𝜙 for all locally minimal models S of 𝑇 ; 4.1. Complexity of SS4F reasoning tasks 2. credulously entailed by 𝑇 , written 𝑇 |≈cred 𝜙, iff We extend the reasoning tasks for S4F to the SS4F case in a S ⊩ 𝜙 for some locally minimal model S of 𝑇 . ♢ straightforward manner, e.g. existenceSS4F decides whether a simple theory 𝑇 ⊆ ℒSK has a locally minimal SS4F model. Other, intermediate, notions of non-monotonic entail- (Since locally minimal models are only defined for simple ment are possible to define, but not our main interest here. theories, all subsequent results are necessarily restricted to this fragment; we will not always explicitly state the requirement that theories be strict.) In what follows we 4. Complexity show that for locally minimal models, the complexities of SS4F reasoning tasks match those of S4F. In this section we will show that the SS4F reasoning tasks We say that an SS4F structure (Π, Ω, 𝜎, 𝜁, 𝛾) is pointwise we defined are not harder than their S4F counterparts. We S5 iff for every 𝜋 ∈ Π, we find 𝜁𝑜 (𝜋) = ∅. Obviously, by start out with showing that standpoint S4F possesses, much definition of S4F minimal models, every locally minimal like other standpoint logics [6], the small model property, model (of some simple theory 𝑇 ) is pointwise S5. where satisfiable theories are guaranteed to have models of We start out with some preparatory observations on SS4F linear size. structures. The first result looks trivial, it however is not, Lemma 2 (Small model property). An SS4F formula 𝜙 and crucially hinges on the fact that (1) modal defaults allow is satisfiable if and only if 𝜙 has a model with at most atoms only within the scope of K;8 and (2) that we restrict |Sub(𝜙) ∩ ℒSK | ≤ ‖𝜙‖ precisifications. attention to structures that are pointwise S5, and thus offer negative introspection. Proof. The “if” direction holds trivially. For the “only if” direc- tion, consider an arbitrary SS4F structure S = (Π, Ω, 𝜎, 𝜁, 𝛾) Lemma 3. Let S = (Π, Ω, 𝜎, 𝜁, 𝛾) be an SS4F structure such that S ⊩ 𝜙. We will show that it can be “pruned” that is pointwise S5. Then for all 𝜋 ∈ Π and all 𝜙 ∈ ℒSK : to obtain a small model S′ = (Π′ , Ω′ , 𝜎 ′ , 𝜁 ′ , 𝛾 ′ ) with S, 𝜋 ⊩ 𝜙 or S, 𝜋 ⊩ ¬𝜙 |Π′ | ≤ |Sub(𝜙) ∩ ℒSK |. We will consider a set of precisifications that will serve as Proof. We use induction on the structure of 𝜙. Note that in witnesses for the satisfaction of subformulas preceded by a any case, we have diamond modality (i.e. some □s in negative polarity.) To this end, let Π′ be a subset of Π with the following S, 𝜋 ⊩ 𝜙 or S, 𝜋 ̸⊩ 𝜙 property: for each subformula □s 𝜓 ∈ Sub(𝜙) not satisfied in S, Π′ contains one precisification 𝜋𝜓 ∈ Π, for which so to show the claim it suffices to show that S, 𝜋𝜓 ̸⊩ 𝜓 holds (note that the existence of such a 𝜋𝜓 follows S, 𝜋 ̸⊩ 𝜙 implies S, 𝜋 ⊩ ¬𝜙 directly from the definition of ⊩.) Otherwise, assuming all ′ □s 𝜓 are satisfied in S, we set Π = {𝜋} for an arbitrary • 𝜙 = K𝜑. (Note that this case covers the induction 𝜋 ∈ Π. The definition of the remaining components of S′ is base with 𝜑 ∈ ℒ as well as the case of 𝜑 ∈ ℒK .) restricted to Π′ , i.e., Assume S, 𝜋 ̸⊩ K𝜑. Then there exists a 𝑤′ ∈ 𝜁𝑖 (𝜋) • Ω′ = Ω ∩ ⋃︀ ′ 𝜁 (𝜋), such that S, 𝜋, 𝑤′ ̸⊩ K𝜑. Since (∅, 𝜁𝑖 (𝜋), 𝛾|𝜁𝑖 (𝜋) ) is 𝜋∈Π′ an S5 structure with a universal accessibility relation, • 𝜎 ′ (s) = 𝜎(s) ∩ Π′ for each s ∈ 𝒮, we get that for all 𝑤 ∈ 𝜁𝑖 (𝜋) we have S, 𝜋, 𝑤 ̸⊩ K𝜑. That is, for all 𝑤 ∈ 𝜁𝑖 (𝜋), we have S, 𝜋, 𝑤 ⊩ ¬K𝜑. • 𝜁 ′ = 𝜁|Π′ and 𝛾 ′ = 𝛾|Ω′ . By definition, then, S, 𝜋 ⊩ ¬K𝜑. To show that S′ ⊩ 𝜙, we fill first prove an interme- • 𝜙 = ¬𝜑. Let S, 𝜋 ̸⊩ ¬𝜑. By the induction hypothesis, diate result by induction on the structure of each subfor- we get that S, 𝜋 ⊩ 𝜑 or S, 𝜋 ⊩ ¬𝜑. The latter is mula 𝜓 ∈ Sub(𝜙): for every 𝜋 ∈ Π′ it holds that impossible, whence S, 𝜋 ⊩ 𝜑 and thus S, 𝜋 ⊩ ¬¬𝜑. S, 𝜋 ⊩ 𝜓 ⇐⇒ S′ , 𝜋 ⊩ 𝜓. The only interesting case is when 𝜓 = □s 𝜓 ′ . Assuming that S, 𝜋 ⊩ □s 𝜓 ′ , by the se- • 𝜙 = 𝜑 ∧ 𝜓. Let S, 𝜋 ̸⊩ 𝜑 ∧ 𝜓. By the induction mantics we get that S, 𝜋 ′ ⊩ 𝜓 ′ for every 𝜋 ′ ∈ 𝜎(s). Be- hypothesis, we have (1) S, 𝜋 ⊩ 𝜑 or S, 𝜋 ⊩ ¬𝜑, cause 𝜎 ′ (s) ⊆ 𝜎(s) and 𝜎 ′ (s) ⊆ Π′ by induction hypothesis and (2) S, 𝜋 ⊩ 𝜓 or S, 𝜋 ⊩ ¬𝜓. If S, 𝜋 ⊩ 𝜑 and we get that S′ , 𝜋 ′′ ⊩ 𝜓 ′ for every 𝜋 ′′ ∈ 𝜎 ′ (s) and con- S, 𝜋 ⊩ 𝜓, then S, 𝜋 ⊩ 𝜑 ∧ 𝜓, which is impossible sequently (by semantics) S′ ⊩ □s 𝜓 ′ . Conversely, assume 8 For example for the atomic formula 𝑝 ∈ 𝒜, it is the case that in a that S, 𝜋 ̸⊩ □s 𝜓 ′ . Then there is 𝜋 ′ ∈ Π such that 𝜋 ′ ∈ 𝜎(s) precisification 𝜋 where nothing is known (i.e. 𝛾(𝜁𝑖 (𝜋)) covers 2𝒜 ), and S, 𝜋 ′ ̸⊩ 𝜓 ′ . Since by construction of S′ we required that we have both S, 𝜋 ̸⊩ 𝑝 and S, 𝜋 ̸⊩ ¬𝑝. by assumption. Thus S, 𝜋 ⊩ ¬𝜑 or S, 𝜋 ⊩ ¬𝜓. In To this end we define the following relations ⊪+ and ⊪− , either case, we get S, 𝜋 ⊩ ¬(𝜑 ∧ 𝜓). where we abbreviate T𝜋 := (Φ𝜋 , Ψ𝜋 , Ξ𝜋 ) for brevity. • 𝜙 = □s 𝜑. Let S, 𝜋 ̸⊩ □s 𝜑. Then there exists a T𝜋 ⊪+ □s 𝜑 :⇐⇒ T𝜋′ ⊪+ 𝜑 for every 𝜋 ′ ∈ 𝜎(s) 𝑤 ∈ 𝜁𝑖 (𝜋) with S, 𝜋, 𝑤 ̸⊩ □s 𝜑. In turn, there exists a 𝜋 ′ ∈ 𝜎(s) and a 𝑤′ ∈ 𝜁𝑖 (𝜋 ′ ) such that T𝜋 ⊪− □s 𝜑 :⇐⇒ T𝜋′ ⊪− 𝜑 for some 𝜋 ′ ∈ 𝜎(s) S, 𝜋 ′ , 𝑤′ ̸⊩ 𝜑. Since 𝜋 ′ is independent of 𝑤, this T𝜋 ⊪+ K𝜑 :⇐⇒ Θ𝜋 ⊢ 𝜑 𝜋 ′ ∈ 𝜎(s) exists for every 𝑤 ∈ 𝜁𝑖 (𝜋), and we obtain − T𝜋 ⊪ K𝜑 :⇐⇒ Θ𝜋 ̸⊢ 𝜑 that for all 𝑤 ∈ 𝜁𝑖 (𝜋), we have S, 𝜋, 𝑤 ̸⊩ □s 𝜑. Thus for all 𝑤 ∈ 𝜁𝑖 (𝜋), we get S, 𝜋, 𝑤 ⊩ ¬□s 𝜑, that is, + T𝜋 ⊪ ¬𝜑 :⇐⇒ T𝜋 ⊪− 𝜑 S, 𝜋 ⊩ ¬□s 𝜑. □ − T𝜋 ⊪ ¬𝜑 :⇐⇒ T𝜋 ⊪+ 𝜑 T𝜋 ⊪+ 𝜑 ∧ 𝜓 :⇐⇒ T𝜋 ⊪+ 𝜑 and T𝜋 ⊪+ 𝜓 The following variant is equivalent, but due to its form T𝜋 ⊪− 𝜑 ∧ 𝜓 :⇐⇒ T𝜋 ⊪− 𝜑 or T𝜋 ⊪− 𝜓 more useful in proofs. Corollary 4. Let S = (Π, Ω, 𝜎, 𝜁, 𝛾) be an SS4F structure Our approach then is to verify that T𝜋 ⊪+ 𝜙 for all 𝜙 ∈ 𝑇 that is pointwise S5. Then for all 𝜋 ∈ Π and all 𝜙 ∈ ℒSK : and 𝜋 ∈ Π (which can be done in deterministic polynomial time with an NP oracle for deciding ⊢ in the cases with S, 𝜋 ̸⊩ 𝜙 if and only if S, 𝜋 ⊩ ¬𝜙 K𝜑), and we claim that this establishes overall modelhood of the guessed structure for 𝑇 . To show this correspondence, Proof. The “only if” direction is clear from the proof of we define (slightly abusing notation S) the SS4F structure Lemma 3. For the “if” direction, it suffices to note that S(Π, 𝜎, (T𝜋 )𝜋∈Π ) = (Π, Ω, 𝜎, 𝜁, 𝛾) based on the partition- S, 𝜋 ⊩ 𝜙 implies S, 𝜋 ̸⊩ ¬𝜙. □ ings (T𝜋 )𝜋∈Π as follows: Theorem 5. existenceSS4F is in ΣP2 . • Ω= ⋃︀ Ω𝜋 where for every 𝜋 ∈ Π, we set 𝜋∈Π Proof. Let 𝑇 be an SS4F theory. By Lemma 2 on the small model property of SS4F, we can deterministically construct Π ¶ ⃓ © Ω𝜋 = (𝜋, 𝜈) ⃓ 𝜈 ⊆ 𝒜+ with 𝜈 ⊩ Θ𝜋 ⃓ (by considering all subformulas of the form □s 𝜑 occurring in negative polarity) and 𝜎. denoting 𝒜+ = 𝒜 ∪ {K𝜑 | K𝜑 ∈ Sub(𝑇 )}; Now, we guess a triple (Φ𝜋 , Ψ𝜋 , Ξ𝜋 ) for each 𝜋 ∈ Π, with Ξ𝜋 ⊆ 𝑇𝜋□ and Φ𝜋 , Ψ𝜋 ⊆ (Sub(𝑇 ) ∩ ℒK )K . • 𝜁𝑜 (𝜋) = ∅ and 𝜁𝑖 (𝜋) = Ω𝜋 for every 𝜋 ∈ Π; (We guess |Π| such triples without any oracle calls in between.) For each precisification 𝜋, we check whether • 𝛾((𝜋, 𝜈)) = 𝜈 for every (𝜋, 𝜈) ∈ Ω𝜋 . their respective Φ𝜋 , Ψ𝜋 are introspection consistent, Note that we allow all formulas K𝜑 ∈ Sub(𝑇 ) to be evalu- i.e. the following (for brevity we use the abbreviation ated as “virtual atoms” in every world in every precisification. Θ𝜋 = Ξ𝜋 ∪ {¬K𝜙 | 𝜙 ∈ Φ𝜋 } ∪ {K𝜓 | 𝜓 ∈ Ψ𝜋 } ∪ Ψ𝜋 ): This leads us to our first technical observation: The defini- (C1) Φ𝜋 ∪ Ψ𝜋 = (Sub(𝑇 ) ∩ ℒK )K and Φ𝜋 ∩ Ψ𝜋 = ∅, tion of the S5 structures at each precisification 𝜋 ∈ Π along with the conditions (C1)–(C3) verified earlier exactly provides (C2) Θ𝜋 is propositionally consistent, the desired correspondence between the “propositional” read- ing (via the propositional theory Θ𝜋 ) and the “S4F” reading (C3) for each 𝜑 ∈ Φ𝜋 , we have Θ𝜋 ̸⊢ 𝜑 (where ⊢ denotes (via the S5 structure Ω𝜋 ) of S4F formulas: the provability relation of propositional logic). Claim 2. For every precisification 𝜋 ∈ Π and potentially Afterwards, we check whether an introspection consistent pair relevant formula 𝜓 ∈ Sub(𝑇 ) ∩ (ℒK ∪ ℒ): (Φ𝜋 , Ψ𝜋 ) corresponds to a minimal S4F model of Ξ𝜋 ,by check- ing if for every 𝜓 ∈ Ψ𝜋 , (∀𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ⊩ 𝜓) ⇐⇒ Ξ𝜋 ∪ {¬K𝜑 | 𝜑 ∈ Φ𝜋 } ⊢S4F 𝜓 (︁ )︁ ∀𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜓 The above requires at most polynomially many calls to an NP oracle (the number of calls is polynomially bounded by the Proof of the claim. We use induction on the structure of 𝜓; cardinality of the set Ψ𝜋 ; the oracle decides ⊢ and ⊢S4F ). since we also cover ℒ, the base case is for 𝜓 = 𝑝 ∈ 𝒜. Most of At this step, it is proven that at each precisification 𝜋, the the cases are trivial, the only interesting case is for 𝜓 = K𝜑, pair (Φ𝜋 , Ψ𝜋 ) represents a minimal S4F model for the relevant which in turn covers all 𝜑 ∈ ℒK ∪ ℒ. theory Ξ𝜋 . What remains We first use 𝜑 ∈ (Sub(𝑇 ) ∩ ℒK )K = Ψ𝜋 ∪ Φ𝜋 to show: (︁ to be proven is whether )︁ the entire construction, namely Π, 𝜎, (Φ, Ψ, Ξ)𝜋∈Π , is a model for the initial SS4F theory 𝑇 (condition (1) of Definition 5). Θ𝜋 |= K𝜑 ⇐⇒ Θ𝜋 |= 𝜑 (†) It is clear that for all 𝜋 ∈ Π, we have Sub(Ξ𝜋 ) ⊆ Sub(𝑇 ) If Θ𝜋 |= K𝜑, then, since Θ𝜋 is propositionally consistent and the local theory Ξ𝜋 is satisfied at 𝜋; what remains to be – condition (C2) –, we have Θ𝜋 ̸|= ¬K𝜑. Thus ¬K𝜑 ∈ / Θ𝜋 detected is whether there is a modal default 𝜙 ∈ 𝑇𝜋□ ∖ Ξ𝜋 and in particular, 𝜑 ∈ / Φ𝜋 , whence by (C1) we get 𝜑 ∈ Ψ𝜋 . that has wrongly been excluded from being relevant at 𝜋. Then also 𝜑 ∈ Θ𝜋 and Θ𝜋 |= 𝜑. This can be checked locally using the NP oracle again, mak- On the other hand, if Θ𝜋 |= 𝜑, then Θ𝜋 ⊢ 𝜑, whence by ing use of Θ𝜋 at each precisification 𝜋. The procedure will be (C3) we obtain 𝜑 ∈ / Φ𝜋 . Thus, by (C1), 𝜑 ∈ Ψ𝜋 , which in given inductively on the structure of an SS4F formula 𝜙. turn means K𝜑 ∈ Θ𝜋 and Θ𝜋 |= K𝜑. (IH) We now obtain: ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ 𝜓 (Corollary 4) ∀𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ⊩ K𝜑 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬¬𝜓 ⇐⇒ Θ𝜋 |= K𝜑 • 𝜙 = 𝜑 ∧ 𝜓. We have (†) ⇐⇒ Θ𝜋 |= 𝜑 ⇐⇒ ∀𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ⊩ 𝜑 T𝜋 ⊪+ 𝜑 ∧ 𝜓 (IH) ⇐⇒ T𝜋 ⊪+ 𝜑 and T𝜋 ⊪+ 𝜓 ⇐⇒ ∀𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜑 (IH) ⇐⇒ ∀𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜑 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ 𝜑 ⇐⇒ ∀𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ K𝜑 and S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ 𝜓 ⇐⇒ ∀𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ K𝜑 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ 𝜑 ∧ 𝜓 This concludes the proof of Claim 2. ♢ and To obtain the desired result, we will prove (making use of T𝜋 ⊪− 𝜑 ∧ 𝜓 Claim 2 in the base(︁ case) that given the SS4F )︁ theory 𝑇 and the ⇐⇒ T𝜋 ⊪− 𝜑 or T𝜋 ⊪− 𝜓 guessed structure Π, 𝜎, (Φ, Ψ, Ξ)𝜋∈Π of partitions, we can (IH) verify modelhood by checking ⊪+ and ⊪− , more formally, ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬𝜑 for all precisifications 𝜋 ∈ Π and for all 𝜙 ∈ Sub(𝑇 ): or S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬𝜓 + (Corollary 4) T𝜋 ⊪ 𝜙 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ 𝜙 (1) ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ̸⊩ 𝜑 − or S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ̸⊩ 𝜓 T𝜋 ⊪ 𝜙 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬𝜙 (2) (Definition 3) The proof works by structural induction on 𝜙. ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ̸⊩ 𝜑 ∧ 𝜓 (Corollary 4) • 𝜙 = K𝜓. Then 𝜓 ∈ Sub(𝑇 ) ∩ (ℒK ∪ ℒ), and regarding ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬(𝜑 ∧ 𝜓) (1) we obtain: • 𝜙 = □s 𝜓. Then T𝜋 ⊪+ K𝜓 T𝜋 ⊪+ □s 𝜓 ⇐⇒ Θ𝜋 ⊢ 𝜓 ⇐⇒ Θ𝜋 |= 𝜓 ⇐⇒ T𝜋′ ⊪+ 𝜓 for every 𝜋 ′ ∈ 𝜎(s) ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ′ ⊩ 𝜓 for every 𝜋 ′ ∈ 𝜎(s) (IH) ⇐⇒ ∀𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ⊩ 𝜓 (Claim 2) ⇐⇒ ∀𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜓 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ □s 𝜓 ⇐⇒ ∀𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜓 and likewise ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ K𝜓 T𝜋 ⊪− □s 𝜓 Regarding (2) we get: ⇐⇒ T𝜋′ ⊪− 𝜓 for some 𝜋 ′ ∈ 𝜎(s) T𝜋 ⊪− K𝜓 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ′ ⊩ ¬𝜓 for some 𝜋 ′ ∈ 𝜎(s) (IH) ⇐⇒ Θ𝜋 ̸⊢ 𝜓 S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ′ ̸⊩ 𝜓 for some 𝜋 ′ ∈ 𝜎(s) (Corollary 4) ⇐⇒ ⇐⇒ Θ𝜋 ̸|= 𝜓 ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ̸⊩ □s 𝜓 ⇐⇒ ∃𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ̸⊩ 𝜓 (Corollary 4) (Claim 2) ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬□s 𝜓 ⇐⇒ ∃𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ̸⊩ 𝜓 ⇐⇒ ∃𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ̸⊩ 𝜓 Thus by verifying T𝜋 ⊪+ 𝜙 for (︁ all 𝜙 ∈ 𝑇 and 𝜋 ∈ )︁ Π, we ⇐⇒ ∃𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ̸⊩ K𝜓 have checked that the structure Π, 𝜎, (Φ, Ψ, Ξ)𝜋∈Π (which (S5) we do not explicitly construct) constitutes a model of 𝑇 . To- ⇐⇒ ∀𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ̸⊩ K𝜓 gether with the checks done earlier, this establishes that T𝜋 ⇐⇒ ∀𝑤 ∈ 𝜁𝑖 (𝜋) : S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋, 𝑤 ⊩ ¬K𝜓 constitutes a locally minimal model of 𝑇 . □ ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬K𝜓 Example 2. Consider the following simple SS4F theory: • 𝜙 = ¬𝜓. We have, with regard to (1), 𝑇 = {□s K𝑝, □s K(𝑝 → 𝑞), □t K𝑞, □t K¬𝑝} T𝜋 ⊪+ ¬𝜓 ⇐⇒ T𝜋 ⊪− 𝜓 A witnessing model representing the locally minimal (IH) SS4F model of 𝑇 could be ({𝜋1 , 𝜋2 }, 𝜎, (T𝜋1 , T𝜋2 )) with ⇐⇒ S(Π, 𝜎, (T𝜋 )𝜋∈Π ), 𝜋 ⊩ ¬𝜓 𝜎(s) = {𝜋1 }, 𝜎(t) = {𝜋2 } and: Similarly, for (2), T𝜋1 = ({¬𝑝} , {𝑝, 𝑝 → 𝑞, 𝑞} , {K𝑝, K(𝑝 → 𝑞)}) T𝜋 ⊪− ¬𝜓 ⇐⇒ T𝜋 ⊪+ 𝜓 T𝜋2 = ({𝑝, 𝑝 → 𝑞} , {𝑞, ¬𝑝} , {K𝑞, K¬𝑝}) . ♢ The construction of a witnessing model can also be minimal SS4F model S = (Π, Ω, 𝜎, 𝜁, 𝛾) of the theory 𝑇 used for credulous reasoning, where we additionally verify from Example 3, in which 𝜎( ) = {𝜋1 , 𝜋2 }, 𝜎( ) = that (Φ𝜋 , Ψ𝜋 , Ξ𝜋 ) ⊪+ 𝜙 for all 𝜋 ∈ Π to demonstrate {𝜋3 }, 𝜎( ) = {𝜋4 } and in which the extensions at each that 𝑇 |≈cred 𝜙. In a similar vein, for sceptical reasoning, precisification can be represented by the following sets of we guess a locally minimal model for 𝑇 and verify that consequences: (Φ𝜋 , Ψ𝜋 , Ξ𝜋 ) ⊪− 𝜙 for some 𝜋 ∈ Π to show that 𝑇 |̸≈scep 𝜙. 𝜋1 : 𝑇* ∪ {hot} 𝜋2 : 𝑇* ∪ {iced } Proposition 6. in-someSS4F and not-in-allSS4F are ΣP2 - 𝜋3 : 𝑇* ∪ {hot, espresso} 𝜋4 : 𝑇* ∪ {hot, low _caffeine} . complete, in-allSS4F is ΠP2 -complete. Therefore, we get the following conclusions: 5. Instantiations 𝑇 |≈cred □ [︁ Kespresso ]︁ 𝑇 |≈cred □* Khot [︁ ]︁ [︁ ]︁ Intuitively, each precisification of a locally minimal SS4F 𝑇 |≈cred □ Klow _caffeine 𝑇 |≈cred □ Kiced model encodes an S4F minimal model for the locally- relevant S4F theory. Given that S4F theories are capable To emphasise the non-monotonic nature of our framework, of encoding multiple non-monotonic reasoning formalisms we note that the two bottom conclusions would be retracted (as described in Section 2.5), we find that SS4F provides if we added additional background knowledge to 𝑇 stating standpoint-enhanced variants of those formalisms. As such, e.g. that coffee is necessarily a hot, highly caffeinated drink: each precisification of a locally minimal model encodes an extension of a default theory in case of standpoint default □* K(coffee → (hot ∧ ¬low _caffeine)). logic, stable extension in case of standpoint argumentation framework or an answer set in case of standpoint logic pro- 5.2. Standpoint (Abstract) Argumentation gram. Below we provide examples of the first two SS4F Similarly, employing the S4F encodings of abstract argu- instantiations. mentation frameworks with standpoint modalities gives rise to standpoint argumentation frameworks. A profile 5.1. Standpoint Default Logic 𝒫 = (𝐹1 , . . . , 𝐹𝑛 ) of 𝑛 argumentation frameworks (with Utilising the S4F encoding of defaults we obtain standpoint 𝐹𝑖 = (𝐴𝑖 , 𝑅𝑖 ) for all 1 ≤ 𝑖 ≤ 𝑛) can be encoded as a single defaults of the form SS4F theory 𝑇𝐹 over 𝒮 = {1, . . . , n, *} as follows: 𝑛 □s [(K𝜙 ∧ K¬K¬𝜓1 ∧ . . . ∧ K¬K¬𝜓𝑛 ) → K𝜓] ⋃︁ 𝑇𝐹 := {□i [K¬K¬𝑎 → K𝑎] | 𝑎 ∈ 𝐴𝑖 } ∪ 𝑖=1 which we conveniently denote as □s [𝜙 : 𝜓1 , . . . , 𝜓𝑛 /𝜓]. Be- low we assume the standpoint default theory 𝑇 to be a set of {□i [K𝑎 → K¬𝑏] | (𝑎, 𝑏) ∈ 𝑅𝑖 } standpoint defaults. To facilitate the reading of background Example 4 presents individual frameworks in their usual knowledge, by formulas □s K𝜙 we denote modal defaults graphical representation, i.e. with nodes denoting argu- of the form □s [⊤ : /𝜙] (i.e. where 𝑛 = 0). ments and edges attacks between them. For such a rep- Example 3 (Example 1 continued). The following S4F resentation being within the scope of a standpoint modality formulas of a theory 𝑇* express common knowledge, such means that each node and attack is encoded for this stand- as that we are indeed dealing with a coffee, that an espresso point using the formula above. cannot be low in caffeine and that a drink cannot be hot and Example 4 ([27]). The following argumentation frame- iced at the same time, i.e. works correspond to individual views 𝐴𝐹1 , 𝐴𝐹2 and 𝐴𝐹3 , provided by Baumeister et al. [27, Figure 4.]. Arguments 𝑇* = {Kcoffee, K¬(iced ∧ hot), model discussion about public access to information and K¬(espresso ∧ low _caffeine)} medical supplies in the context of a potential epidemic [27, Table 1.]. Generally, in each view arguments draw from a We use 𝑇□* to denote the set 𝑇□* = {□* 𝜙 | 𝜙 ∈ 𝑇* }. Ad- common pool of arguments, whereas attacks between them ditionally, we provide the set of standpoint defaults 𝑇𝐷 are up for individual judgement of a respective agent. Here, presented in the introduction, expressing that coffee is usu- the entire theory 𝑇𝐹 is defined as: ally consumed hot, unless served in Vietnam, where iced ⎡ ⎤ variants are more common and that a typical coffee in Italy is 𝑏 𝑔 𝑑 a highly-caffeinated espresso, contrary to the typical, filtered coffee in the US. □V1 ⎢⎣ ⎥ ⎦ 𝑐 𝑓 𝑒 ß ⎡ ⎤ 𝑔 [︁ ]︁ [︁ ]︁ 𝑇𝐷 = □* coffee : hot/hot , □ coffee : iced /iced , 𝑎 𝑏 𝑑 [︁ coffee : espresso/espresso , ]︁ □V2 ⎢⎣ ⎥ ⎦ □ 𝑐 𝑒 ™ [︁ ]︁ ⎡ ⎤ □ coffee : low _caffeine/low _caffeine 𝑎 𝑏 𝑔 𝑑 □V3 ⎢⎣ ⎥ ⎦ We obtain the standpoint default theory 𝑇 = 𝑇𝐷 ∪ 𝑇□* .♢ 𝑐 𝑓 𝑒 Since extensions of a default theory can be characterised by where standpoint argumentation frameworks are used to finite sets of defaults’ consequences [5, 22], there is a locally express each of the distinct viewpoints, 𝑉1 , 𝑉2 and 𝑉3 . ♢ Viewpoints from Example 4 have the following stable ex- restricted our attention to simple theories, where standpoint tensions – 𝑉1 : {𝑐, 𝑒, 𝑔}, 𝑉2 : {𝑎, 𝑐, 𝑒, 𝑔}, 𝑉3 : {𝑎, 𝑐, 𝑒, 𝑔} and modalities are essentially used only in an atomic form. The {𝑎, 𝑑, 𝑓 }. Since in a locally minimal SS4F model of 𝑇𝐹 each reason is that the definition of the set 𝑇𝜋□ is hard to general- precisification must encode precisely one stable extension ise without enabling to potentially guess unjustified know- of a related framework, we find e.g. 𝑇𝐹 |≈cred □V2 K𝑎 or ledge into the locally relevant theory. For example, with 𝑇𝐹 |≈cred □* K𝑐, but 𝑇𝐹 |̸≈scep □* K𝑐. 𝑇 = {□s K𝑝 ∨ ¬□s K𝑝} we expect, as the theory is tauto- We consider how standpoint argumentation relates to logical, a unique minimal model where nothing is known; approaches for collective acceptability in abstract argument- alas, guessing Ξ𝜋 = {K𝑝} is not straightforward to avoid ation discussed in the literature [28, 27]. In the so-called and leads to knowing 𝑝 without justification. argument-wise approaches, acceptability of the individual A potential fix via considering globally minimal models views (frameworks) is determined using standard methods that do not require syntax-based guessing is the objective (argumentation semantics) followed by semantic aggrega- of current and future work. Furthermore, while we have tion, where arguments deemed acceptable individually are mostly ignored sharpening statements s ⪯ u herein, they aggregated into a single set of jointly accepted arguments. could be easily added, but would increase the amount of Other techniques, referred to as framework-wise, first ag- constructs to treat in checks and proofs. gregate individual views into a collective representation, e.g. In further future work, we intend to come up with a single argumentation framework and then employ standard (disjunctive) ASP encoding for relevant fragments of SS4F (or dedicated) methods to obtain the joint set of accepted with the intent of providing a prototypical implementation. arguments from that representation. We also want to study strong equivalence for SS4F; the case Semantics of standpoint argumentation, in which pre- of plain S4F has been studied by Truszczyński [14]. Finally, cisifications encode single stable extensions and where it is also worthwhile to develop a proof system for our new moreover standpoint modalities are employed to aggreg- logic. S4F has a proof system via the axioms (K), (T), (4), ate the extensions, follows the argument-wise approach. and (F); propositional standpoint logic has proof systems as Interestingly, general (i.e. non-simple) SS4F theories are cap- well [1, 29]. It will be challenging to combine these proof able of capturing the framework-wise techniques e.g. the systems to obtain one for SS4F. nomination rule [27], in which an attack between a pair of arguments in the resulting framework is established if it occurs in at least one of the input frameworks. For a set of all Acknowledgments arguments of a profile 𝒫, defined as 𝐴𝒫 = 𝐴1 ∪ . . . ∪ 𝐴𝑛 , We are indebted to Lucía Gómez Álvarez for helpful discus- necessitation can be obtained by instantiating the below sions on the subject matter. schema for every pair of arguments 𝑎, 𝑏 ∈ 𝐴𝒫 : We also acknowledge funding from BMBF within ′ ′ projects KIMEDS (grant no. GW0552B), MEDGE (grant ♢* [K𝑎 → K¬𝑏] → □* [K𝑎 → K¬𝑏 ]. no. 16ME0529), and SEMECO (grant no. 03ZU1210B). In particular, instantiating the schema for 𝑇𝐹 would effect- ively amount to supplying 𝑇𝐹 with: References ′ ⎡ ⎤ ′ ′ 𝑔 ′ 𝑎 𝑏 𝑑 [1] L. Gómez Álvarez, S. Rudolph, Standpoint logic: Multi- □* ⎢⎣ ⎥ ⎦ perspective knowledge representation, in: F. Neuhaus, 𝑐′ 𝑓′ 𝑒′ B. Brodaric (Eds.), Formal Ontology in Information Systems – Proceedings of the Twelfth International In a similar vein, also the majority (resp. the unanimity) Conference, FOIS 2021, Bozen–Bolzano, Italy, Septem- rule [27] – adding the attack if it is present in the majority ber 11–18, 2021, volume 344 of Frontiers in Artificial (resp. all) of the individual frameworks – could be captured Intelligence and Applications, IOS Press, 2021, pp. 3–17. in SS4F. However, as mentioned above, enabling framework- URL: https://doi.org/10.3233/FAIA210367. wise aggregation techniques requires non-simple SS4F the- [2] B. Bennett, Standpoint semantics: a framework for ories, which is beyond the scope of this paper and is con- formalising the variable meaning of vague terms, Un- sidered as future work. derstanding Vagueness. Logical, Philosophical and Lin- guistic Perspectives (2011) 261–278. [3] K. K. Segerberg, An Essay in Classical Modal Logic, 6. Conclusion Ph.D. thesis, Stanford University, Department of Philo- sophy, 1971. In this paper we introduced standpoint S4F, a two- [4] G. Schwarz, M. Truszczyński, Minimal knowledge dimensional modal logic for describing heterogeneous view- problem: A new approach, Artif. Intell. 67 (1994) points that can incorporate default reasoning to make se- 113–141. URL: https://doi.org/10.1016/0004-3702(94) mantic commitments. We defined syntax and semantics and 90013-2. analysed the complexity of the most pertinent reasoning [5] R. Reiter, A logic for default reasoning, Artif. In- problems associated to our logic. The pleasant result was tell. 13 (1980) 81–132. URL: https://doi.org/10.1016/ that incorporating standpoint modalities comes at no addi- 0004-3702(80)90014-4. tional computational cost, as the complexity of the underly- [6] L. Gómez Álvarez, S. Rudolph, H. Strass, How to Agree ing logic, non-monotonic S4F, is preserved. We exemplified to Disagree – Managing Ontological Perspectives us- the new formalism by showcasing two instantiations with ing Standpoint Logic, in: U. Sattler, A. Hogan, C. M. concrete NMR formalisms, namely Reiter’s default logic [5] Keet, V. Presutti, J. P. A. Almeida, H. Takeda, P. Mon- and Dung’s argumentation frameworks [24]. nin, G. Pirrò, C. d’Amato (Eds.), The Semantic Web – A drawback of our current preliminary results is that we ISWC 2022 – 21st International Semantic Web Confer- [19] D. V. McDermott, J. Doyle, Non-monotonic logic I, ence, Virtual Event, October 23–27, 2022, Proceedings, Artif. Intell. 13 (1980) 41–72. URL: https://doi.org/10. volume 13489 of Lecture Notes in Computer Science, 1016/0004-3702(80)90012-0. Springer, 2022, pp. 125–141. URL: https://doi.org/10. [20] D. V. McDermott, Nonmonotonic logic II: nonmono- 1007/978-3-031-19433-7_8. tonic modal theories, J. ACM 29 (1982) 33–57. URL: [7] L. Gómez Álvarez, S. Rudolph, H. Strass, Tractable https://doi.org/10.1145/322290.322293. diversity: Scalable multiperspective ontology manage- [21] M. Gelfond, H. Przymusinska, V. Lifschitz, ment via standpoint EL, in: Proceedings of the Thirty- M. Truszczyński, Disjunctive defaults, in: J. F. Second International Joint Conference on Artificial Allen, R. Fikes, E. Sandewall (Eds.), Proceedings of Intelligence, IJCAI 2023, 19th-25th August 2023, Ma- the 2nd International Conference on Principles of cao, SAR, China, ijcai.org, 2023, pp. 3258–3267. URL: Knowledge Representation and Reasoning (KR’91). https://doi.org/10.24963/ijcai.2023/363. Cambridge, MA, USA, April 22-25, 1991, Morgan [8] L. Gómez Álvarez, S. Rudolph, H. Strass, Pushing the Kaufmann, 1991, pp. 230–237. boundaries of tractable multiperspective reasoning: A [22] G. Gottlob, Complexity Results for Nonmonotonic deduction calculus for standpoint EL+, in: P. Marquis, Logics, Journal of Logic and Computation 2 (1992) T. C. Son, G. Kern-Isberner (Eds.), Proceedings of the 397–425. URL: https://doi.org/10.1093/logcom/2.3.397. 20th International Conference on Principles of Know- [23] M. Gelfond, V. Lifschitz, Classical negation in logic ledge Representation and Reasoning, KR 2023, Rhodes, programs and disjunctive databases, New Gener. Com- Greece, September 2-8, 2023, 2023, pp. 333–343. URL: put. 9 (1991) 365–386. URL: https://doi.org/10.1007/ https://doi.org/10.24963/kr.2023/33. BF03037169. [9] L. G. Álvarez, S. Rudolph, Reasoning in SHIQ with [24] P. M. Dung, On the acceptability of arguments and axiom- and concept-level standpoint modalities, in: its fundamental role in nonmonotonic reasoning, lo- Proceedings of KR 2024, 2024. gic programming and 𝑛-person games, Artif. In- [10] N. Gigante, L. Gómez Álvarez, T. S. Lyon, Stand- tell. 77 (1995) 321–358. URL: https://doi.org/10.1016/ point linear temporal logic, in: P. Marquis, T. C. Son, 0004-3702(94)00041-X. G. Kern-Isberner (Eds.), Proceedings of the 20th Inter- [25] H. Strass, Approximating operators and semantics national Conference on Principles of Knowledge Rep- for abstract dialectical frameworks, Artif. Intell. 205 resentation and Reasoning, KR 2023, Rhodes, Greece, (2013) 39–70. URL: https://doi.org/10.1016/j.artint.2013. September 2-8, 2023, 2023, pp. 311–321. URL: https: 09.004. //doi.org/10.24963/kr.2023/31. [26] A. Kurucz, F. Wolter, M. Zakharyaschev, D. M. Gabbay, [11] M. Truszczyński, Modal interpretations of default Many-dimensional modal logics: Theory and applica- logic, in: J. Mylopoulos, R. Reiter (Eds.), Proceedings tions, Elsevier, 2003. of the 12th International Joint Conference on Artificial [27] D. Baumeister, D. Neugebauer, J. Rothe, Collective Intelligence. Sydney, Australia, August 24–30, 1991, Acceptability in Abstract Argumentation, Journal of Morgan Kaufmann, 1991, pp. 393–398. URL: http:// Applied Logics – IfCoLoG Journal of Logics and Their ijcai.org/Proceedings/91-1/Papers/061.pdf. Applications 8 (2021) 1503–1542. [12] G. Schwarz, Minimal model semantics for nonmono- [28] G. Bodanza, F. Tohmé, M. Auday, Collective argument- tonic modal logics, in: Proceedings of the Seventh ation: A survey of aggregation issues around argu- Annual Symposium on Logic in Computer Science mentation frameworks, Argument and Computation (LICS ’92), Santa Cruz, California, USA, June 22-25, 8 (2017) 1–34. 1992, IEEE Computer Society, 1992, pp. 34–43. URL: [29] T. S. Lyon, L. Gómez Álvarez, Automating reasoning https://doi.org/10.1109/LICS.1992.185517. with standpoint logic via nested sequents, in: G. Kern- [13] G. Schwarz, M. Truszczyński, Nonmonotonic reason- Isberner, G. Lakemeyer, T. Meyer (Eds.), Proceedings ing is sometimes simpler, in: G. Gottlob, A. Leitsch, of the 19th International Conference on Principles of D. Mundici (Eds.), Computational Logic and Proof The- Knowledge Representation and Reasoning, KR 2022, ory, Springer Berlin Heidelberg, Berlin, Heidelberg, Haifa, Israel, July 31 – August 5, 2022, 2022. URL: https: 1993, pp. 313–324. //proceedings.kr.org/2022/26/. [14] M. Truszczyński, The modal logic S4F, the default logic, and the logic here-and-there, in: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelli- gence, July 22–26, 2007, Vancouver, British Columbia, Canada, AAAI Press, 2007, pp. 508–514. URL: http: //www.aaai.org/Library/AAAI/2007/aaai07-080.php. [15] F. Lin, Y. Shoham, A logic of knowledge and justified assumptions, Artif. Intell. 57 (1992) 271–289. URL: https://doi.org/10.1016/0004-3702(92)90019-T. [16] V. Lifschitz, Minimal belief and negation as failure, Artif. Intell. 70 (1994) 53–72. URL: https://doi.org/10. 1016/0004-3702(94)90103-1. [17] G. Gottlob, Translating default logic into standard autoepistemic logic, J. ACM 42 (1995) 711–740. URL: https://doi.org/10.1145/210332.210334. [18] R. C. Moore, Semantical considerations on nonmono- tonic logic, Artif. Intell. 25 (1985) 75–94. URL: https: //doi.org/10.1016/0004-3702(85)90042-6.