Answer Set Programming with Epistemic Defaults Shutao Zhang1 , Zhizheng Zhang1 and Jun Shen1 1 School of Computer Science and Engineering, Southeast University, China Abstract Answer Set Prolog (ASP) and its extensions are considered powerful tools for encoding defaults. However, some defaults that are usually originated from permitted modal expressions seem hard to deal with through ASP and its existing extensions. In this paper, we develop two extensions of ASP, which are called ASPD and ESD , by introducing permitted operators. The former uses an operator C preceding a literal to express the literal is permitted to be true in the current belief set. The latter extends Epistemic Specification (ES) with an epistemic operator A preceding a literal to express the literal is permitted to be true in some belief sets. The syntax and semantics of ASPD and ESD are introduced sequentially. Then, the relationship between ESD and the ES is carefully discussed to show the difference between epistemic operators M and A. Besides, several examples in the paper are used to illustrate the necessity of using permitted operators in ASP and its extensions. Keywords answer set prolog, epistemic specifications, epistemic defaults 1. Introduction Furthermore, let us see the introspection situation in ES as shown in Example 2. Answer Set Prolog (ASP) [1] is a successful KR language under stable semantics [2] with plenty of extensions. Example 2. β€œπ‘ if π‘ž is possible” is often encoded as an ES Epistemic Specifications (ES) is one of these extensions program Ξ 3 : that allow for introspective reasoning with incomplete knowledge through epistemic operators. Gelfond [3] and 𝑝 ← Mπ‘ž. Kahl [4] presented an extension of the answer set prolog However, Ξ 3 has an unique world view {βˆ…}, which by introducing the epistemic operators K and M to sup- is against our interpretation that β€œπ‘ is true because π‘ž is port strong introspection. Shen and Eiter [5] proposed permitted”, and we expect a world view {{𝑝}}. a language for strong introspection through epistemic Here we have another example of introspection in negation operator NOT instead of K and M. Although Example 3, which is a variant of an example in [6]. ASP and ES are considered as powerful tools for encoding defaults, some defaults that are usually originated from Example 3. A sentinel should raise the alarm if he found permitted expressions seem hard to deal with in ASP and some evidence that it is possible to be dangerous. Mean- ES. while, he should keep alert if the danger has not been elim- Example 1 (𝑝 by default). An interpretation of β€œπ‘ by inated. default” is β€œπ‘ is true if it is permitted.” Under this inter- There are two rules about the sentinel’s introspection pretation, β€œπ‘ by default” naturally means a belief set {𝑝}. and decisions in this example. The first one is a rule with Moreover, with additional information that β€œπ‘ is not per- introspection about the possibility and can be encoded mitted”, the belief set is {}. by a classical ES rule There are usually two ASP programs Ξ 1 and Ξ 2 that are used to encode β€œπ‘ by default” respectively. Ξ 1 ∢ π‘Žπ‘™π‘Žπ‘Ÿπ‘š ← Mπ‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ1 ) {𝑝 ← ¬¬𝑝.}, where Β¬ denotes negation as failure (NAF). However, we can not find an accurate ES rule to express Ξ 2 ∢ {𝑝 ← Β¬ ∼ 𝑝.}, where ∼ denote strong negation. the second one, which can be interpreted as the sentinel However, neither Ξ 1 nor Ξ 2 follows our interpretation. should keep alert if π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  is permitted by some be- Ξ 1 has two answer sets, {𝑝} and {}. Ξ 2 seems fine, but lief sets. For instance, we try to describe the sentinel’s Ξ 2 βˆͺ {← 𝑝.} is not satisfiable, which we expect to have an introspection with the following rules. answer set {}. ASPOCP 2021: Workshop on Answer Set Programming and Other π‘Žπ‘™π‘’π‘Ÿπ‘‘ ← Mπ‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ2β€² ) Computing Paradigms, September 30, 2021, Porto, Portugal π‘Žπ‘™π‘’π‘Ÿπ‘‘ ← Β¬K ∼ π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ2β€³ ) Envelope-Open shutao_zhang@seu.edu.cn (S. Zhang); seu_zzz@seu.edu.cn (Z. Zhang); junshen@seu.edu.cn (J. Shen) Rule (π‘Ÿ2β€² ) means π‘Žπ‘™π‘’π‘Ÿπ‘‘ can be derived if there exists at least Orcid 0000-0003-0853-9281 (S. Zhang); 0000-0001-9851-6184 (Z. Zhang); 0000-0001-7245-7075 (J. Shen) one answer set in which π‘‘π‘Žπ‘”π‘’π‘Ÿπ‘œπ‘’π‘  is true, but a belief Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). set permitting π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  may not contain it. Rule (π‘Ÿ2β€³ ) CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) contains a new literal ∼ π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  in its body, which can not be derived if there is no rule with ∼ π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  in its A default rule is normal if 𝛽 is equivalent to πœ”; it is semi- head. Therefore, neither rule (π‘Ÿ2β€² ) nor rule (π‘Ÿ2β€³ ) has the normal if 𝛽 implies πœ”. A default theory is a pair (𝐷, π‘Š ), semantics we want. where 𝐷 is a set of default rules, and π‘Š is a set of formulas. Hence, this paper aims to develop the extensions of ASP and ES respectively to address the issues of handling Definition 1 (Extension of Default Theories). Let (𝐷, π‘Š ) defaults originated from permitted expressions. Specifi- be a default theory, 𝐸 be a set of formulas. Define 𝐸0 = π‘Š cally, we develop two extensions of ASP, which are called and for 𝑖 β‰₯ 0: ASPD and ESD respectively, by introducing permitted op- 𝛼 ∢ 𝛽1 , … , 𝛽 𝑛 erators. The former uses an operator C preceding a literal 𝐺𝐷𝑖 ={ ∈ 𝐷|𝛼 ∈ 𝐸𝑖 , βˆ€π›½π‘– ∢∼ 𝛽𝑖 βˆ‰ 𝐸} πœ” to express the literal is permitted to be true in the current belief set. The latter extends Epistemic Specification (ES) 𝐸𝑖+1 =𝑇 β„Ž(𝐸𝑖 ) βˆͺ {πΆπ‘œπ‘›π‘ π‘’π‘ž(𝛿)|𝛿 ∈ 𝐺𝐷𝑖 }. with an epistemic operator A preceding a literal to ex- where 𝑇 β„Ž(𝐸𝑖 ) is the set of all classical propositional conse- press the literal is permitted to be true in some belief sets. quences of 𝐸𝑖 , πΆπ‘œπ‘›π‘ π‘’π‘ž(𝛿) is the consequent of the default Intuitively, β€œπ‘ by default” can be encoded as 𝑝 ← C𝑝. in ∞ rule 𝛿. Then 𝐸 is an extension for (𝐷, π‘Š ) iff 𝐸 = ⋃𝑖=0 𝐸𝑖 . ASPD , and β€œπ‘ if π‘ž is possible” can be encoded as 𝑝 ← Aπ‘ž. Note that we use operator Β¬ for negation as failure (NAF) in ESD . Furthermore, the second rule in Example 3 can and ∼ for classical negation in this paper. An extension of be written as default theory (𝐷, π‘Š ) represents a possible set of beliefs of π‘Žπ‘™π‘’π‘Ÿπ‘‘ ← Aπ‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ2 ) this theory. Gelfond et al. [8] proposed the Disjunctive Default According to rule (π‘Ÿ2 ), the sentinel should keep alert if Logic (DDL) that extended classical DL with disjunction π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  is not proved to be inconsistent in at least one to extend the representation ability of default logic. The of his belief sets. disjunctive defaults have the form of Usually, a non-ground logic program, which is a logic program with variables, is considered as a shorthand for 𝛼 ∢ 𝛽1 , … , π›½π‘š the corresponding ground program. Therefore, we only (2) πœ”1 | … |πœ”π‘› consider ground logic programs in this paper unless in some examples. Definition 2. (Extension of Disjunctive Default Theories) The rest of this paper is organized as follows. In Sec- Let (𝐷, π‘Š ) be a disjunctive default theory, 𝐸 be a set of tion 2, we review Default Logic and Epistemic Specifica- formulas. 𝐸 is an extension for (𝐷, π‘Š ) if 𝐸 is one of the tions. In Section 3, we propose the syntax and semantics minimal deductively closed set of formulas 𝐸 β€² , where for of 𝐴𝑆𝑃D . In Section 4, we propose the syntax and se- any default rule from 𝐷, if 𝛼 ∈ 𝐸 β€² and ∼ 𝛽1 , … , ∼ π›½π‘š βˆ‰ 𝐸, mantics of 𝐸𝑆D . In section 5, we discuss the relationship then βˆƒπœ”π‘– ∢ πœ”π‘– ∈ 𝐸 β€² . between the new language and ESGK [4]. At last, we conclude the paper with some future work. Researchers have paid much attention to the relation- ships between modal logic and default logic to capture the semantics of default logic. They have found many inher- 2. Preliminaries ent connections between these two kinds of knowledge. Konolige [9] proved the existence a reversible translation 2.1. Default Logic from default logic into strongly grounded autoepistemic logic (AEL). Based on his work, Gottlob [10] constructed Defaults are very useful in logic programs because they a nonmodular translation from default logic to standard allow drawing conclusions based on commonsense or AEL. Truszczynski [11] has shown that the nonmono- typical knowledge with incomplete knowledge. Default tonic logic S4F captures the default logic. Cabalar et al. Logic (DL) [7] has been extensively researched since it [12] proposed intuitionistic default logic, a variation of was proposed as a nonmonotonic paradigm to represent default logic inside S4F. Meanwhile, some researchers default. focused on represent default by logic programming lan- The defeasible rules in default logic are called default guages. Gelfond [13] has shown that the nonmonotonic rules of the form logic ASP without constraints or disjunctions captures 𝛼 ∢ 𝛽1 , … , 𝛽 𝑛 the default logic. He also presented a method to represent (1) defaults in ASP by adding literals and rules about abnor- πœ” mal information [1]. Lifschitz [14] introduced an idea where 𝛼, 𝛽, πœ” are classical formulas. 𝛼 is the prerequisite to translate ASP programs into default theories, which of the default, 𝛽𝑖 s are justifications, πœ” is the consequent. Chen et al. [15] used to develop a default logic solver The default rule 1 intuitively means ”If 𝛼 is provable and based on ASP solvers. all 𝛽𝑖 s are consistent with it, then assume πœ” as default.” 𝑠 π‘Š βŠ§π‘  π‘Š βŠ­π‘  Extended Literal 𝑒 ¬𝑒 K𝑒 Β¬K𝑒 M𝑒 Β¬M𝑒 K𝑒 replace 𝑠 by 𝑒 delete the rule Label Β¬ K Β¬K M Β¬M Β¬K𝑒 remove 𝑠 replace 𝑠 with ¬𝑒 M𝑒 remove 𝑠 replace 𝑠 with ¬¬𝑒 Table 2 Β¬M𝑒 replace 𝑠 by ¬𝑒 delete the rule Labels of outcoming edges from literal nodes Table 1 Modal reduct of ESGK r2 M Β¬ q p 2.2. Epistemic Specifications and Justified Β¬ Semantics M r1 Epistemic Specifications (ES) extends traditional answer set programs with epistemic modal operators K and M. Figure 1: Modal support graph of Ξ 4 with M-cycle An ES program is a finite set of rules of the form: 𝑒1 π‘œπ‘Ÿ … π‘œπ‘Ÿ π‘’π‘˜ ← π‘’π‘˜+1 , … , π‘’π‘š , 𝑠1 , … , 𝑠𝑛 . (3) β€’ for each rule π‘Ÿπ‘– in Ξ , there is a rule node labeled by where 𝑙 is a literal, 𝑒𝑖 s are objective literals of the form 𝑙 or π‘Ÿπ‘– denoting the rule; ¬𝑙, 𝑠𝑖 s are subjective literals with an epistemic operator β€’ for each distinct objective literal 𝑒 in the language K, Β¬K, M, or Β¬M. of Ξ , there is a literal node labeled by 𝑒; A belief set of an ES program Ξ  is a consistent set of β€’ for each objective literal 𝑒 in the head of rule π‘Ÿ, there literals in the language of Ξ . A view is a collection of is an unlabeled edge from the rule node π‘Ÿ to literal belief sets. If an extended literal is satisfied by a point node 𝑒; structure ⟨𝐴, π‘Š ⟩, where 𝐴 ∈ π‘Š, is defined as: β€’ for each extended literal in the body of rule π‘Ÿ, there β€’ ⟨𝐴, π‘Š ⟩ ⊧ 𝑙 iff 𝑙 ∈ 𝐴, where 𝑙 is a literal. is an edge labeled according to Table 2 going from β€’ ⟨𝐴, π‘Š ⟩ ⊧ ¬𝑙 iff 𝑙 βˆ‰ 𝐴. literal node 𝑒 to rule node π‘Ÿ. β€’ ⟨𝐴, π‘Š ⟩ ⊧ K𝑒 iff βˆ€π΄ ∈ π‘Š ∢ 𝐴 ⊧ 𝑒. β€’ ⟨𝐴, π‘Š ⟩ ⊧ M𝑒 iff βˆƒπ΄ ∈ π‘Š ∢ 𝐴 ⊧ 𝑒. Definition 6 (M-Cycle). A cycle in the MS graph of an β€’ ⟨𝐴, π‘Š ⟩ ⊧ Β¬K𝑒 iff βˆƒπ΄ ∈ π‘Š ∢ 𝐴 ⊭ 𝑒. epistemic logic program is called an M-cycle if 𝑀 labels β€’ ⟨𝐴, π‘Š ⟩ ⊧ Β¬M𝑒 iff βˆ€π΄ ∈ π‘Š ∢ 𝐴 ⊭ 𝑒. an edge within the cycle. For an objective literal 𝑒, it can be denoted as 𝐴 ⊧ 𝑒. For a Example 4 (M-cycle). Consider a program Ξ 4 : subjective literal 𝑠, it can be denoted as π‘Š ⊧ 𝑠. 𝑝 ←Mπ‘ž, Β¬π‘ž. (π‘Ÿ1 ) Many versions of semantics have been proposed for the language of Epistemic Specifications. Kahl [4] introduced π‘ž ←M𝑝, ¬𝑝. (π‘Ÿ2 ) a typical one, which we call ESGK in this paper, by the definition of modal reduct and world view. Figure 1 shows the modal support graph of Ξ 4 , which con- tains an M-cycle through π‘ž, rule (π‘Ÿ1 ), 𝑝 and rule (π‘Ÿ2 ). Definition 3 (Modal Reduct of ESGK ). Let Ξ  be a finite ES program, π‘Š be a collection of belief sets. The modal In Example 4, program Ξ 4 should has a unique world reduct of Ξ  w.r.t π‘Š, denoted by Ξ π‘Š , is obtained from Ξ  by view {{𝑝}, {π‘ž}} under the semantics of ESGK . However, eliminating subjective literals as Table 1. many researchers claimed their disagreement against this example, including Yi-Dong shen [5] and Yuanling Zhang Definition 4 (World Views of ESGK ). π‘Š is a world view [16]. of Ξ  if and only if π‘Š is equal to a collection of all answer The aim of justified semantics of ES, which we called sets of Ξ π‘Š . ESZZ in this paper, is to develop an intuitive understand- ing of the M operator and get rid of circular justification To have a clear view of circular modal justification, in a stronger sense. It refines the semantics of Epistemic Kahl also introduced the conception of the M-cycle, a Specifications by constructing a justified reduct and dis- cycle in modal support graph of a program with an edge junction reduct. By the new semantics, since all literals of M. in a world view need to be justified, the M-cycle does not Definition 5 (Modal Supported Graph). Given an epis- cause a self-support problem. temic logic program Ξ , a modal supported graph of Ξ , or ESZZ provides a classical method to define the views MS graph for short, is a directed graph where: with a maximal guess of epistemic negations. 𝑠 π‘Š βŠ§π‘  π‘Š βŠ­π‘  Example 6 (Continuing Example 5). The modal reduct K𝑒 replace 𝑠 by 𝑒 delete the rule of Ξ 5 w.r.t. π‘Š, 𝐴1 , 𝜌 is Β¬K𝑒 remove 𝑠 delete the rule M𝑒 remove 𝑠 delete the rule 𝑝1 ← π‘ž1 . Β¬M𝑒 replace 𝑠 by ¬𝑒 delete the rule 𝑝1 ← π‘ž2 . Table 3 General Modal Reduct of Maximal View Definition 11 (Justified Views). Consider Ξ  be a program with epistemic defaults, π‘Š = {𝐴1 , … , 𝐴𝑛 } a collection of belief sets. Let 𝐡 = {𝑙𝑖 |𝐴𝑖 ⊧ 𝑙, 1 ≀ 𝑖 ≀ 𝑛}, the full reduct Definition 7 (Maximal Views). Let Ξ  be an ES program of Ξ  w.r.t. βŸ¨π΄π‘– , π‘Š ⟩, denoted by Π⟨𝐴 𝑖 ,π‘Š ⟩ full , is obtained from and π‘Š = {𝐴1 , … , 𝐴𝑛 }, where 𝐴𝑖 s are belief sets. A dis- Ξ  by applying justified reduct w.r.t. π‘Š, Gelfond-Lifschitz junctive program Ξ π‘Š is called the general modal reduct 𝐡,∨ π‘Š ,𝐴 ,𝜌 𝐡 π‘Š = {𝐴1 , … , 𝐴𝑛 } if it is obtained by eliminating every sub- reduct and disjunction reduct w.r.t. 𝐡, i.e ((Ξ  𝑖 ) ) . jective literals in Ξ  with the transformation in Table 3. We π‘Š is a justified view of Ξ  iff 𝐡 is the unique stable model call π‘Š a maximal view if π‘Š is the collection of all answer of ⋃𝑛 Ξ βŸ¨π΄π‘– ,π‘Š ⟩ . 𝑖=1 full sets of Ξ π‘Š . Definition 12 (World Views of ESZZ ). Let Ξ  be an ES In addition to the maximal view, the justified view program and π‘Š a collection of belief sets. π‘Š is a world requires all belief sets in a world view to be justified, view of Ξ  iff π‘Š is a justified view and maximal view of Ξ . which means all subjective literals satisfied by a belief set are not only supported by themselves. Definition 8 (Disjunction Reduct). Let Ξ  be a positive 3. Answer Set Programming with disjunctive program and 𝐴 be a consistent set of literals in Defaults the language of Ξ . The disjunction reduct of Ξ  w.r.t. 𝐴, D denoted by Π𝐴,∨ , is a program obtained from Ξ  removing This section introduce the syntax and semantics of ASP , all literals not in 𝐴 from the head of all the rules in Ξ . which extends ASP with operator C. An ASPD program Ξ  is a finite collection of rules of The intuitive meaning of disjunction reduct is that if a the form literal 𝑙 in the head of rule π‘Ÿ is not contained in a belief set 𝐴, then 𝑙 does not affect other literals in β„Žπ‘’π‘Žπ‘‘(π‘Ÿ). 𝑒1 π‘œπ‘Ÿ β‹― π‘œπ‘Ÿ π‘’π‘˜ ← π‘’π‘˜+1 , β‹― , π‘’π‘š , 𝑑1 , β‹― , 𝑑𝑛 . (4) Definition 9 (Modal Operator Interpretation). Let Ξ  be where 𝑒𝑖 are extended literals of the form 𝑙 or ¬𝑙, 𝑙s are a program with epistemic defaults, π‘Š = {𝐴1 , … , 𝐴𝑛 } be literals in classical logic, 𝑑𝑖 are default literals of the form a collection of belief sets. The mapping 𝜌 from subjective C𝑒 or Β¬C𝑒. Intuitively, C𝑒 means it is permitted (or not literal 𝑠 and belief set 𝐴𝑖 is defined as 𝜌(𝑠, 𝐴𝑖 ) for all 𝐴𝑖 , 𝐴𝑗 ∈ forbidden) to assume 𝑒 is true, and Β¬C𝑒 means 𝑒 is proved π‘Š: to be not permitted. A rule containing operator C is a default rule. β€’ if π‘Š ⊧ K𝑒, 𝜌(K𝑒, 𝐴𝑖 ) = {𝑒𝑖 }; β€’ if π‘Š ⊧ Β¬K𝑒, 𝜌(Β¬K𝑒, 𝐴𝑖 ) = {¬𝑒𝑗 |𝐴𝑗 βŠ§π‘’}ΜΈ ; Example 7. Consider the following default logic programs β€’ if π‘Š ⊧ M𝑒, 𝜌(M𝑒, 𝐴𝑖 ) = {𝑒𝑗 |𝐴𝑗 ⊧ 𝑒}; Ξ 6 β€’ if π‘Š ⊧ Β¬M𝑒, 𝜌(Β¬M𝑒, 𝐴𝑖 ) = {¬𝑒𝑖 }. π‘π‘–π‘Ÿπ‘‘(𝑑𝑀𝑒𝑒𝑑𝑦). (π‘Ÿ1 ) Example 5. Let Ξ 5 = {𝑝 ← Mπ‘ž.}, π‘Š = {𝐴1 = {π‘ž}, 𝐴2 = 𝑓 𝑙𝑖𝑒𝑠(𝑋 ) ← π‘π‘–π‘Ÿπ‘‘(𝑋 ), C𝑓 𝑙𝑖𝑒𝑠(𝑋 ). (π‘Ÿ2 ) {𝑝, π‘ž}}. The modal operator interpretation of π‘ž w.r.t 𝐴1 is 𝜌(Mπ‘ž, 𝐴1 ) = {π‘ž1 , π‘ž2 }. and Ξ β€²6 Definition 10 (Modal Reduct for ESZZ ). Consider an ES 𝑝𝑒𝑛𝑔𝑒𝑖𝑛(𝑑𝑀𝑒𝑒𝑑𝑦). (π‘Ÿ3 ) program Ξ , a collection π‘Š of belief sets {𝐴1 , … , 𝐴𝑛 }. The ← 𝑝𝑒𝑛𝑔𝑒𝑖𝑛(𝑋 ), 𝑓 𝑙𝑖𝑒𝑠(𝑋 ). (π‘Ÿ4 ) modal reduct of Ξ  w.r.t. π‘Š, 𝐴𝑖 , and 𝜌, denoted as Ξ π‘Š ,𝐴𝑖 ,𝜌 , is derived by following steps. Since 𝑓 𝑙𝑖𝑒𝑠(𝑑𝑀𝑒𝑒𝑑𝑦) does not conflict with rule (π‘Ÿ1 ) or rule (π‘Ÿ2 ), Ξ 6 concludes 𝑓 𝑙𝑖𝑒𝑠(𝑑𝑀𝑒𝑒𝑑𝑦). However, with the addi- 1. Renaming each objective literal 𝑒 not occurring in tional fact rule (π‘Ÿ3 ) and constraint rule (π‘Ÿ4 ) in Ξ β€²6 , it is any subjective literal in Ξ  by 𝑒𝑖 ; inconsistent to assume that 𝑓 𝑙𝑖𝑒𝑠(𝑑𝑀𝑒𝑒𝑑𝑦) is true. Thus 2. removing rules whose body contains a subjective 𝑓 𝑙𝑖𝑒𝑠(𝑑𝑀𝑒𝑒𝑑𝑦) is not in the consequent of Ξ 6 βˆͺ Ξ β€²6 . literal 𝑠 that π‘ŠβŠ§π‘ ;ΜΈ 3. replacing every occurrence of subjective literal 𝑠 in Example 7 illustrated the semantics of ASPD we have rule π‘Ÿ or its copies by a literal in 𝜌(𝑠, 𝐴𝑖 ). defined intuitively. Now we will give a formal definition. 𝑑 βŸ¨π‘‹ , π‘Œ ⟩ ⊧ 𝑑 βŸ¨π‘‹ , π‘Œ ⟩ ⊭ 𝑑 Definition 16 (Stable Models of ASPD programs). Let Ξ  C𝑙 remove 𝑑 replace 𝑑 with 𝑙 be an ASPD program. A literal set 𝐴, where 𝐴 βŠ† πΏπ‘–π‘‘π‘’π‘Ÿπ‘Žπ‘™(Ξ ), C¬𝑙 remove 𝑑 replace 𝑑 with ¬𝑙 is called a stable model of Ξ  if βˆƒπ‘Œ ∢ ⟨𝐴, π‘Œ ⟩ ∈ 𝐷𝑆𝑀(Ξ ). Β¬C𝑙 replace 𝑑 with ¬𝑙 delete the rule The set of all stable models of the program Ξ  is denoted by Β¬C¬𝑙 replace 𝑑 with 𝑙 delete the rule 𝑆𝑀(Ξ ). Table 4 Let us take a close look at Definition 13 and 15. It Obtain Ξ βŸ¨π‘‹ ,π‘Œ ⟩ by eliminating defaults, where 𝑙 is a positive shows that by the second condition of Definition 15, 𝐻 is literal without C or Β¬. stable, i.e., 𝑋 is minimal, while the third condition makes sure π‘Œ is maximal, thus the default stable model βŸ¨π‘‹ , π‘Œ ⟩ can satisfy as many extended literals in Ξ  as possible. Definition 13 (Satisfiability). A default interpretation of program Ξ  is a pair of consistent literal sets βŸ¨π‘‹ , π‘Œ ⟩, where Example 8 (Default Stable Models). Consider the ASPD 𝑋 βŠ† π‘Œ βŠ† πΏπ‘–π‘‘π‘’π‘Ÿπ‘Žπ‘™(Ξ ) and πΏπ‘–π‘‘π‘’π‘Ÿπ‘Žπ‘™(Ξ ) is the set of all literals program Ξ 7 in the Herbrand universe of Ξ . Let βŸ¨π‘‹ , π‘Œ ⟩ be a default interpretation of Ξ , π‘Ž ← Cπ‘Ž. 𝑏 ← C𝑏. β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ 𝑙 iff 𝑙 ∈ 𝑋 where 𝑙 is a literal; ← π‘Ž, 𝑏. β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ ¬𝑒 iff 𝑋 ⊧ ΜΈ 𝑒 where 𝑒 is an extended literal; β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ C𝑙 iff 𝑙 ∈ π‘Œ; 𝑐 ← π‘Ž. β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ C¬𝑒 iff π‘Œ ⊧ ΜΈ 𝑒; Consider default interpretations 𝑀1 = ⟨{π‘Ž, 𝑐}, {π‘Ž, 𝑐}⟩, and β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ Β¬C𝑒 iff βŸ¨π‘‹ , π‘Œ ⟩ ⊧ ΜΈ C𝑒; 𝑀2 = ⟨{𝑏}, {𝑏}⟩, 𝑀3 = ⟨{}, {}⟩. {π‘Ž, 𝑐} is an answer set of Ξ 7 1 𝑀 β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ π‘Ÿ iff βˆƒπ‘’ ∈ β„Žπ‘’π‘Žπ‘‘(π‘Ÿ) ∢ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ 𝑒 or βˆƒπœ™ ∈ 𝑀2 and {𝑏} is an answer set of Ξ 7 . By Definition 16, 𝑀1 and π‘π‘œπ‘‘π‘¦(π‘Ÿ) ∢ βŸ¨π‘‹ , π‘Œ ⟩ ⊭ πœ™, where π‘Ÿ is a rule in Ξ , 𝑒 is an 𝑀2 are default stable models of Ξ 7 . For 𝑀3 , the π‘Œ-part of 𝑀3 extended literal in the head of π‘Ÿ, πœ™ is an extended 𝑀 literal or default literal; is π‘Œ3 = {} ∈ 𝐴𝑆(Ξ 7 3 ). However, there exists π‘Œ β€² = {π‘Ž, 𝑐} that β€² π‘Œ ⊧Π ⟨{},{π‘Ž,𝑐}⟩ , and Ξ¦(π‘Œ3 , Ξ ) βŠ‚ Ξ¦(π‘Œ β€² , Ξ 7 ). Therefore, 𝑀3 is β€’ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ Ξ  iff βˆ€π‘Ÿ ∈ Ξ  ∢ βŸ¨π‘‹ , π‘Œ ⟩ ⊧ π‘Ÿ, and this default interpretation is called a default model of Ξ . not a default stable model of Ξ 7 , and 𝑆𝑀(Ξ 7 ) = {{π‘Ž, 𝑐}, {𝑏}}. In a default interpretation βŸ¨π‘‹ , π‘Œ ⟩ which satisifies an Example 8 is a typical instance of ASPD that shows 𝐴𝑆𝑃D program Ξ , if 𝑙 ∈ π‘Œ, then C𝑙 is allowed by βŸ¨π‘‹ , π‘Œ ⟩. In the feature of the operator C. Neither ¬¬𝑒 nor Β¬ ∼ 𝑒 can that case, 𝑋 should be an answer set of the default reduct capture the semantics of C𝑒. For example, program Ξ 7 has Ξ βŸ¨π‘‹ ,π‘Œ ⟩ , which is obtained by removing default literals two stable models {π‘Ž, 𝑐} and {𝑏}. Considering following from Ξ . ASP programs Ξ β€²7 : Definition 14 (Default Reduct). Let Ξ  be an ASPD pro- π‘Ž ← Β¬Β¬π‘Ž. gram, βŸ¨π‘‹ , π‘Œ ⟩ be a default model of Ξ . The default reduct 𝑏 ← ¬¬𝑏. of Ξ  w.r.t. βŸ¨π‘‹ , π‘Œ ⟩, denoted by Ξ βŸ¨π‘‹ ,π‘Œ ⟩ , is obtained by elim- ← π‘Ž, 𝑏. inating the occurrence of C𝑒 or Β¬C𝑒 in rule π‘Ÿ as Table 4. 𝑐 ← π‘Ž. Now we use default reduct to define the default stable and Ξ β€³ 7: models of a program with default rules. π‘Ž ← Β¬ ∼ π‘Ž. Definition 15 (Default Stable Models). For an ASPD 𝑏 ← Β¬ ∼ 𝑏. program Ξ , a default model βŸ¨π‘‹ , π‘Œ ⟩ is a default stable model ← π‘Ž, 𝑏. of Ξ  iff 𝑐 ← π‘Ž. 1. 𝑋 is an answer set of Ξ βŸ¨π‘‹ ,π‘Œ ⟩ , 2. π‘Œ ⊧ Ξ βŸ¨π‘‹ ,π‘Œ ⟩ , On the one hand, Ξ β€²7 has three answer sets, {π‘Ž, 𝑐}, {𝑏}, and 3. let Ξ¦(π‘Œ , Ξ ) be a set of default literals of the form C𝑒 {}. Apparently {} is not a stable model of Ξ 7 that we want, in Ξ  that satisfied by βŸ¨π‘‹ , π‘Œ ⟩, there does not exist a thus ¬¬𝑒 can not represent defaults. On the other hand, β€³ consistent set of literals π‘Œ β€² that 𝑋 βŠ† π‘Œ β€² , Ξ¦(π‘Œ , Ξ ) βŠ‚ Ξ 7 is unsatisfiable, which means Β¬ ∼ 𝑒 can not represent β€² Ξ¦(π‘Œ β€² , Ξ ) and π‘Œ β€² ⊧ Ξ βŸ¨π‘‹ ,π‘Œ ⟩ . defaults neither. ASPD also provides a method to represent negative The set of all default stable models of a program Ξ  is denoted defaults, which is not provided by classical default logic. by 𝐷𝑆𝑀(Ξ ). Example 9 (Programs with Defaults and Negation). Con- 𝑠 π‘Š βŠ§π‘  π‘Š βŠ­π‘  sider the ASPD program Ξ 8 K𝑒 replace 𝑠 by 𝑒 delete the rule Β¬K𝑒 remove 𝑠 delete the rule π‘Ž ← Β¬C𝑏. M𝑒 remove 𝑠 delete the rule Β¬M𝑒 replace 𝑠 by ¬𝑒 delete the rule and the ASPD program Ξ 9 A𝑒 remove 𝑠 C𝑒 Β¬A𝑒 replace 𝑠 by Β¬C𝑒 delete the rule π‘Ž ← C¬𝑏. Table 5 and default interpretations 𝑀1 = ⟨{π‘Ž}, {π‘Ž}⟩, and 𝑀2 = Modal Reduct of ES with Epistemic Defaults. βŸ¨βˆ…, {𝑏}⟩. 𝑀 For program Ξ 8 and 𝑀1 , we have Ξ 8 1 = {π‘Ž ← ¬𝑏.} and {{π‘Ž}} = 𝐴𝑆(Ξ 8 ). However, there is another default Definition 18 (Modal Reduct). Let Ξ  be a program with 𝑀1 𝑀′ epistemic defaults and π‘Š be a non-empty collection of belief interpretation 𝑀1β€² = ⟨{π‘Ž}, {π‘Ž, 𝑏}⟩ that Ξ 8 1 = {} and {π‘Ž, 𝑏} ⊧ sets, where a belief set is a default interpretation βŸ¨π‘‹ , π‘Œ ⟩. β€² 𝑀 Ξ 8 1 , and Ξ¦({π‘Ž, 𝑏}, Ξ 8 ) = {C𝑏} while Ξ¦({π‘Ž}, Ξ 8 ) = βˆ…. By The modal reduct of Ξ  w.r.t π‘Š, denoted by Ξ π‘Š , is an ASPD the third condition in Definition 15, 𝑀1 is not a default program obtained from Ξ  as Table 5 by eliminating every 𝑀′ stable model of Ξ 8 . Because {π‘Ž} is not an answer set of Ξ 8 1 , subjective literal 𝑠. by the first condition of Definition 16, 𝑀1β€² is not a default Definition 18 is a modification of the modal reduct of stable model of Ξ 8 . On the other hand, 𝑀2 ∈ 𝐷𝑆𝑀(Ξ 8 ), traditional Epistemic Specifications. The last two rows and βˆ… is a stable model of Ξ 8 . define the reduct of the new subjective operator A. How- For program Ξ 9 and default interpretation 𝑀2 , we have 𝑀 ever, we still need a method to reduce the circular justifi- βˆ… = 𝐴𝑆(Ξ 9 2 ). However, there exists a default interpreta- cations: subjective interpretation and justified reduct. tion 𝑀2β€² = βŸ¨βˆ…, {π‘Ž}⟩, and Ξ¦({π‘Ž}, Ξ 9 ) = {C¬𝑏}. Meanwhile, 𝑀′ 𝑀′ Definition 19 (Subjective Interpretation). Let Ξ  be a Ξ¦({𝑏}, Ξ 9 ) = βˆ…, Ξ 9 2 = {π‘Ž.}, thus {π‘Ž} ⊧ Ξ 9 2 . Therefore, 𝑀2 program with epistemic defaults, π‘Š = {𝐴1 , … , 𝐴𝑛 } be a is not a default stable model of Ξ 9 . It is easy to check that collection of belief sets. The mapping 𝜌 from subjective 𝑀1 is a default stable model of Ξ 9 . literal 𝑠 and belief set 𝐴𝑖 is defined as 𝜌(𝑠, 𝐴𝑖 ) for all 𝐴𝑖 , 𝐴𝑗 ∈ Example 9 shows how does ASPD deal with the nega- π‘Š: tion of defaults and how does the function Ξ¦ works. β€’ if π‘Š ⊧ K𝑒, 𝜌(K𝑒, 𝐴𝑖 ) = {𝑒𝑖 }; Now, let us revisited Example 1. β€œπ‘ by default” can be D β€’ if π‘Š ⊧ Β¬K𝑒, 𝜌(Β¬K𝑒, 𝐴𝑖 ) = {¬𝑒𝑗 |𝐴𝑗 ⊭ 𝑒}; described by an ASP program containing only one rule: β€’ if π‘Š ⊧ M𝑒, 𝜌(M𝑒, 𝐴𝑖 ) = {𝑒𝑗 |𝐴𝑗 ⊧ 𝑒}; 𝑝 ← C𝑝. β€’ if π‘Š ⊧ Β¬M𝑒, 𝜌(Β¬M𝑒, 𝐴𝑖 ) = {¬𝑒𝑖 }; β€’ if π‘Š ⊧ A𝑒, 𝜌(A𝑒, 𝐴𝑖 ) = {C𝑒𝑗 |𝐴𝑗 ⊧ C𝑒}; It is easy to check that {𝑝} is the unique stable model of β€’ if π‘Š ⊭ A𝑒, 𝜌(A𝑒, 𝐴𝑖 ) = {C𝑒𝑖 }; the program as we expect. β€’ if π‘Š ⊧ Β¬A𝑒, 𝜌(Β¬A𝑒, 𝐴𝑖 ) = {Β¬C𝑒𝑖 }; β€’ if π‘Š ⊭ Β¬A𝑒, 𝜌(Β¬A𝑒, 𝐴𝑖 ) = {Β¬C𝑒𝑗 |𝐴𝑗 ⊭ Β¬C𝑒}. 4. Epistemic Specifications with In Definition 19, 𝜌 is a mapping from a subjective literal Defaults to the belief sets that justifies it. 𝜌 provides a method to find the self-support cycles in a program. For a subjective This section introduces the syntax and semantics of ESD , literal 𝑠 with classical epistemic operators, the justified an extension of ESZZ . reduct of 𝑠 is ignored if π‘ŠβŠ§π‘ ,ΜΈ because circular justification A rule of ESD is of the form is not permitted in this situation. However, for 𝑠 with operator A or Β¬A, 𝑠 need to be justified whenever π‘Š ⊧ 𝑠 𝑒1 π‘œπ‘Ÿ β‹― π‘œπ‘Ÿ π‘’π‘˜ ← π‘’π‘˜+1 , β‹― , π‘’π‘š , 𝑠1 , β‹― , 𝑠𝑛 . (5) or not. where 𝑙𝑖 are literals, 𝑒𝑖 are objective literals (or extended Example 10 (Subjective Interpretation). Considering pro- literals in ASPD ) of the form 𝑙 or ¬𝑙, 𝑠𝑖 s are subjective liter- gram Ξ 10 with a self-supported of A. als of the form K𝑒, Β¬K𝑒, M𝑒, Β¬M𝑒, A𝑒 or Β¬A𝑒. Intuitively, 𝑝 ← Aπ‘ž, Β¬π‘ž. A𝑒 means that 𝑒 may be permitted. π‘ž ← A𝑝, ¬𝑝. Definition 17 (Satisfaction of A𝑒). For a collection of Let 𝐴1 = ⟨{𝑝}, {𝑝}⟩, 𝐴2 = ⟨{π‘ž}, {π‘ž}⟩, W = {𝐴1 , 𝐴2 }. The default interpretations π‘Š, π‘Š ⊧ A𝑒 iff βˆƒπ‘€ ∈ π‘Š ∢ 𝑀 ⊧ C𝑒. subjective interpretations w.r.t. π‘Š is 𝜌(A𝑝, 𝐴𝑖 ) = C𝑝1 and 𝜌(Aπ‘ž, 𝐴𝑖 ) = Cπ‘ž2 for 𝑖 ∈ {1, 2}. Definition 20 (Justified Reduct). Consider an ESD pro- highest conviction gram Ξ , a collection π‘Š of belief sets {𝐴1 , … , 𝐴𝑛 }. The jus- Kl Β¬Ml tified reduct of Ξ  w.r.t. βŸ¨π΄π‘– , π‘Š ⟩, denoted by Ξ βŸ¨π΄π‘– ,π‘Š ⟩ , is l Β¬l obtained by the following steps: Ml Β¬Kl 1. removing rule π‘Ÿ if there exists a subjective literal lowest conviction 𝑠 ∈ π‘π‘œπ‘‘π‘¦(π‘Ÿ) with operator K, Β¬K, M or Β¬M if π‘Š ⊧ 𝑠; 2. replacing subjective literals 𝑠 in rule π‘Ÿ or its copies Figure 2: Preference Relation of Subjective Literals with literals in 𝜌(𝑠, 𝐴𝑖 ) if π‘Š ⊧ 𝑠; 3. replacing objective literals 𝑙 with 𝑙𝑖 . The justified reduct of a program Ξ  w.r.t. π‘Š shows Example 13 (Compare M-cycle). Consider an ES pro- the justification of all literals in Ξ . However, a justified gram Ξ 11 reduct is a default logic program with disjunctions, which 𝑝 ← M𝑝. is possible to have stable models not contained by π‘Š. Definition 21 (Justified View). Consider Ξ  be a program Let π‘Š1 = {𝑝}, π‘Š2 = {βˆ…}. with epistemic defaults, π‘Š = {𝐴1 , … , 𝐴𝑛 } a collection of Under the semantics of ESGK , the modal reducts of Ξ 11 π‘Š π‘Š default interpretations. Let 𝐡 = {𝑙𝑖 |𝐴𝑖 ⊧ 𝑙, 1 ≀ 𝑖 ≀ 𝑛}, 𝐢 = are Ξ 111 = {𝑝.} and Ξ 112 = {𝑝 ← ¬¬𝑝.}. Because π‘Š1 = π‘Š1 π‘Š2 {𝑙𝑖 |𝐴𝑖 ⊧ C𝑙, 1 ≀ 𝑖 ≀ 𝑛}, the full reduct of Ξ  w.r.t. βŸ¨π΄π‘– , π‘Š ⟩, 𝐴𝑆(Ξ 11 ), π‘Š2 β‰  𝐴𝑆(Ξ 11 ), π‘Š1 is a world view of Ξ  while ⟨𝐴 ,π‘Š ⟩ π‘Š2 is not. denoted by Ξ full𝑖 , is obtained from Ξ  by applying justified reduct w.r.t. π‘Š, Gelfond-Lifschitz reduct and disjunction Kahl [4] assumes that a rational agent should prefer reduct w.r.t. 𝐡. π‘Š is a justified view of Ξ  iff ⟨𝐡, 𝐡 βˆͺ 𝐢⟩ is to believe the subjective literals M𝑙 than 𝑙 than K𝑙. The 𝑛 ⟨𝐴 ,π‘Š ⟩ the only default stable model of ⋃𝑖=1 Ξ full𝑖 . epistemic negation defined by Shen [5] shows the same preference relation. This preference relation makes a Example 11 (Justified Views of Ξ 10 ). Consider program rule with directly M-cycle works like a justification part Ξ 10 in Example 10. The justified reducts Ξ 10 ⟨𝐴1 ,π‘Š ⟩ = in a normal default rule. More generally, a program with {𝑝1 ← Cπ‘ž2 , Β¬π‘ž1 .π‘ž1 ← C𝑝1 , ¬𝑝1 .}, Ξ 10 ⟨𝐴2 ,π‘Š ⟩ = {𝑝2 ← M-cycles works like a default theory. Cπ‘ž2 , Β¬π‘ž2 .π‘ž2 ← C𝑝1 , ¬𝑝2 .}. By Definition 21, 𝐡 = 𝐢 = Because the definition of the justified reduct and modal ⟨𝐴 ,π‘Š ⟩ ⟨𝐴 ,π‘Š ⟩ {𝑝1 , π‘ž2 }, which is the answer set of Ξ 10 full1 βˆͺ Ξ 10 full2 . reduct of operator K and M is equal to Yan Zhang and Thus π‘Š is a justified view of Ξ 10 . Yuanlin Zhang [16], the circular justification of M and K will be omitted if the literals in this loop do not have Definition 22 (World View). Let Ξ  be a program with any external support. As a result, a subjective literal of epistemic defaults, π‘Š be a collection of default interpreta- the form M𝑙 can be interpreted as ”it is safe to believe 𝑙 is tions. π‘Š is a world view of Ξ  iff possible.”, and other rules or belief sets should justify the 1. π‘Š is equal to the collection of all default stable possibility of 𝑙 . models of the modal reduct Ξ π‘Š and A further observation of the unjustified world views caused by operator M reminds us that the semantics 2. π‘Š is a justified view of Ξ . of modal operator M may be ambiguous. In classical Example 12 (World View of Ξ 10 ). Consider Program Ξ 10 ES programs, the M-cycle of one rule is often used to and π‘Š1 = {𝐴1 , 𝐴2 } in Example 10. Since π‘Š ⊧ A𝑝 ∧ Aπ‘ž, the express default information. For example, the traditional π‘Š modal reduct Ξ 101 is {𝑝 ← Β¬π‘ž.π‘ž ← ¬𝑝.}. 𝐴1 and 𝐴2 are the description β€œa bird can fly by default” is usually expressed π‘Š in ES programs by the following rule: only default stable models of Ξ 101 . Example 11 has shown that π‘Š1 is a justified view of Ξ 10 . Thus π‘Š1 is a world view 𝑓 𝑙𝑦(𝑋 ) ← π‘π‘–π‘Ÿπ‘‘(𝑋 ), M𝑓 𝑙𝑦(𝑋 ). of Ξ 10 . π‘Š2 Consider π‘Š2 = {βŸ¨βˆ…, βˆ…βŸ©}. The modal reduct Ξ 10 = {𝑝 ← However, for a bird 𝑑𝑀𝑒𝑒𝑑𝑦, the only justification of sub- π‘Š Cπ‘ž, Β¬π‘ž.π‘ž ← C𝑝, ¬𝑝.}, and 𝐷𝑆𝑀(Ξ 102 ) = π‘Š2 . The justified jective literal M𝑓 𝑙𝑦(𝑑𝑀𝑒𝑒𝑑𝑦) is exactly this rule and the reduct of Ξ 10 w.r.t. π‘Š2 is {𝑝1 ← Cπ‘ž1 , Β¬π‘ž1 .π‘ž1 ← C𝑝1 , ¬𝑝1 .}. unique belief set that contains 𝑓 𝑙𝑦(𝑑𝑀𝑒𝑒𝑑𝑦). It means Thus π‘Š2 is also a world view of Ξ 10 . M𝑓 𝑙𝑦(𝑑𝑀𝑒𝑒𝑑𝑦) is not justified by this belief set. Example 14 (Continuing Example 3). Consider the fol- 5. Relation with ESGK lowing extension Ξ 12 of the program in Example 3. This section will compare the semantics of ESD to the π‘Žπ‘™π‘Žπ‘Ÿπ‘š ← Mπ‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ1 ) one of ESGK , which we have introduced in Section 2. π‘Žπ‘™π‘’π‘Ÿπ‘‘ ← Aπ‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘ . (π‘Ÿ2 ) π‘‘π‘Žπ‘›π‘”π‘’π‘Ÿπ‘œπ‘’π‘  ← π‘Žπ‘™π‘Žπ‘Ÿπ‘š. (π‘Ÿ3 ) Proof. Let rule π‘Ÿ be a rule in Ξ  of the form (7), π‘Ÿ β€² is ob- tained from π‘Ÿ by replacing M𝑝 with A𝑝. If π‘Š ⊭ 𝐡, both Rule (π‘Ÿ3 ) means the sentinel will belief it is dangerous if the π‘Ÿ and π‘Ÿ β€² are satisfied, thus we only need to consider the alarm has been raised. This looks reasonable because the situations that π‘Š ⊧ 𝐡. alarm can be raised by other sentinels. Rule (π‘Ÿ1 ) and rule To prove the soundness of Proposition 1, consider the (π‘Ÿ3 ) constitute an M-cycle, and by the natural language following situations: description, π‘Žπ‘™π‘Žπ‘Ÿπ‘š should not exist in any belief sets of the world views of Ξ 12 . β€’ For Β¬K𝑙 ∈ 𝐡, if π‘Š ⊭ Β¬K𝑙, the modal reduct of Example 3 shows the difference between the represen- ESGK replaces Β¬K𝑙 with ¬𝑙. By the definition of tation of the introspection about permitted and possibil- satisfiability, βˆ€π΄π‘– ∈ π‘Š ∢ 𝑙 ∈ 𝐴𝑖 , which means ities. With the idea in this example, β€œa bird can fly by π‘Ÿ is deleted in the Gelfond-Lifschitz reduct. By Μ‚ default” should be represented in ESD by the following Definition 18, π‘Ÿ is deleted in Ξ β€²π‘Š . If π‘Š ⊧ Β¬K𝑙, then rule: Β¬K𝑙 is removed in both reducts. 𝑓 𝑙𝑦(𝑋 ) ← π‘π‘–π‘Ÿπ‘‘(𝑋 ), A𝑓 𝑙𝑦(𝑋 ). β€’ For M𝑙 ∈ 𝐡 or M𝑙 ∈ Ξ /π‘Ÿ, if π‘Š ⊧ M𝑙, then M𝑙 is removed in both reducts. If π‘Š ⊭ M𝑙, it is replaced This rule forms an A-cycle, which can be defined as the Μ‚ by ¬¬𝑙 in Ξ β€²π‘Š , while the rule is removed in Ξ β€²π‘Š . M-cycle in Section 2. Because M𝑙 does not occur in any M-cycles, ¬¬𝑙 Definition 23 (A-cycle). For a subjective literal 𝑠 of the does not support 𝑙. According to the definition form A𝑒 or Β¬A𝑒 in a rule π‘Ÿ, label the edge from 𝑒 to the of satisfiability in ESGK , 𝑙 is not satisfied by any objective literals 𝑒 β€² ∈ β„Žπ‘’π‘Žπ‘‘(π‘Ÿ) in MS graphs by the leading belief set in π‘Š, thus the rule M𝑙 occurs in is deleted modal operators A or Β¬A. A cycle in the MS graph of an in the Gelfond-Lifschitz reduct. epistemic logic program is called an A-cycle if A labels an β€’ For other subjective literals 𝑠 ∈ 𝐡 without oper- edge within the cycle. ator M, the modal reduct of 𝑠 by Definition 3 is equal to the one by Definition 18. Example 15 (A-cycle). Consider program Ξ 13 : β€’ If π‘Š ⊧ M𝑝 and π‘Š ⊧ 𝐡, the modal reduct of π‘Ÿ w.r.t 𝑝 ← A𝑝. π‘Š is 𝑝 ← 𝐡., which means βˆ€π΄π‘– ∈ π‘Š ∢ 𝑝 ∈ 𝐴𝑖 and π‘Š Μ‚ ⊧ A𝑝. By the definition of justified reduct, Let π‘Š = {𝐴1 = ⟨{𝑝}, {𝑝}⟩}. The modal reduct of Ξ 13 w.r.t ̂𝑖 ∈ π‘ŠΜ‚ ∢ 𝑝𝑖 ← C𝑝𝑖 ., 𝑝𝑖 is π‘Ÿ is translated into βˆ€π΄ π‘Š is {𝑝.}, which means π‘Š = 𝐷𝑆𝑀(Ξ π‘Š 13 ). The justified ⟨𝐴 ,π‘Š ⟩ justified. By the definition of modal reduct, π‘Ÿ is reduct of Ξ 13 w.r.t. ⟨𝐴1 , π‘Š ⟩ is Ξ 13 1 = {𝑝1 ← C𝑝1 .}, translated into 𝑝 ← 𝐡.. For the other rules in and ⟨{𝑝1 }, {𝑝1 }⟩ is the unique default stable model of it, Ξ , the modal reducts under both semantics are which means π‘Š is a justified view of Ξ . As a result, π‘Š is a Μ‚ equal, thus (Ξ /π‘Ÿ)π‘Š = (Ξ β€² /π‘Ÿ β€² )π‘Š . It shows that world view of Ξ 13 . β€² π‘Š is a world view of Ξ  under the semantics in With close observation of Example 13 and Example Definition 22. 15, we can find that although M-cycles’s semantics are β€’ If π‘Š ⊭ M𝑝 and π‘Š ⊧ 𝐡, the modal reduct of π‘Ÿ defined differently, operator A provides a method to rep- w.r.t π‘Š is {𝑝 ← ¬¬𝑝, 𝐡.}, which is equivalent to resent defaults information, which M-cycles represent {𝑝 π‘œπ‘Ÿ ¬𝑝 ← 𝐡.}. Because βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 ⊭ 𝑝, 𝑝 under the semantics of ESGK . must not be consistent with the other rules in Ξ /π‘Ÿ, thus βˆ€π΄π‘– ∈ π‘Š Μ‚ ∢ 𝐴𝑖 ⊭ C𝑝 and π‘Š ⊭ A𝑝, rule Definition 24 (Default View Image). For a view π‘Š of Μ‚ of π‘Š is a π‘Ÿ β€² is deleted from Ξ β€² in the modal reduct of π‘Ÿ β€² . an ESGK program Ξ , the default view image π‘Š Μ‚ is a justified view of Ξ β€² and equals As a result, π‘Š collection of default interpretations that Μ‚ to the collection of default stable models of Ξ β€²π‘Š . Μ‚ = {⟨𝐴, 𝐴⟩|𝐴 ∈ π‘Š } π‘Š (6) It shows that π‘Š is a world view of Ξ β€² under the semantics in Definition 22. Proposition 1 (Relationship between direct M-cycle and A-cycle). Let Ξ  be an ES program that every modal opera- To prove the completeness of Proposition 1, consider tor M in Ξ  occurs in a rule of the form the following situations: 𝑝 ← M𝑝, 𝐡. (7) β€’ As shown in the proof of soundness, subjective where 𝐡 is a collection of objective literals or extended sub- literals in 𝐡 and Ξ /π‘Ÿ are equivalent under the two jective literals, Ξ β€² be a program obtained from Ξ  by replac- semantics. ing M with A. A collection of belief sets π‘Š is a world view β€’ If π‘Š Μ‚ ⊧ A𝑝, the modal reduct of π‘Ÿ β€² w.r.t π‘Š Μ‚ is 𝑝., GK of Ξ  under ES semantics if and only if its default view ̂𝑖 ∈ π‘Š Μ‚ ∢ 𝐴̂𝑖 ⊧ 𝑝., π‘Š ⊧ M𝑝. The modal thus βˆ€π΄ image π‘Š Μ‚ is a world view of Ξ β€² under the semantics of 𝐸𝑆D . reducts of rest rules in Ξ  and Ξ β€² are equal, thus π‘Š is the collection of all answer sets of Ξ π‘Š , which Proof. According to the proof of Proposition 1, rules (π‘Ÿ2 ) means π‘Š is a world view of Ξ . , … , (π‘Ÿπ‘–+1 ) are equivalent to rules (π‘Ÿ2β€² ) , … , (π‘Ÿπ‘–+1β€² ). Thus β€’ If π‘ŠΜ‚ ⊭ A𝑝, A𝑝 is replaced by C𝑝 in the modal we only need to prove the equivalence of rule (π‘Ÿ1 ) and β€² reduct Ξ β€²π‘Š . By the definition of satisfiability, (π‘Ÿ1 ) when π‘Š ⊧ 𝐡1 . For the soundness part, considering Μ‚ βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 βŠ­Ξ β€²π‘ŠΜ‚ C𝑝, thus βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 ⊭ 𝑝, following situations: π‘Š ⊭ M𝑝. The modal reduct of π‘Ÿ is 𝑝 ← ¬¬𝑝, 𝐡., β€’ If π‘Š ⊧ M𝑝, the modal reduct of π‘Ÿ1 is π‘ž1 ← 𝐡1 .. Μ‚ thus the modal reduct of Ξ π‘Š = Ξ β€²π‘Š /{𝑝 ← C𝑝, 𝐡.}βˆͺ Meanwhile, for every 𝐴 ̂𝑗 ∈ π‘Š Μ‚ the justified reduct Μ‚ {𝑝 ← ¬¬𝑝, 𝐡.}, and Ξ β€²π‘Š is not consistent with 𝑝. of π‘Ÿ1β€² is π‘ž1𝑗 ← C𝑝𝑖 , 𝐡1𝑗 .. If M𝑝 is concluded by It means 𝐴𝑆(Ξ π‘Š ) = 𝐴𝑆(Ξ β€²π‘Š ) = π‘Š, π‘Š is a world Ξ /{π‘Ÿ1 , … , π‘Ÿπ‘–+1 }, then according to the definition of Μ‚ ,π‘Š ⟨𝐴 Μ‚βŸ© view of Ξ . justified view, 𝑝 is justified by (Ξ β€² /{π‘Ÿ β€² , … , π‘Ÿ β€² }) 𝑗 . 𝑖 1 𝑖+1 𝑓 𝑒𝑙𝑙 According to the proof of soundness and completeness Otherwise, M𝑝 is satisfied only when 𝐡1 , … , 𝐡𝑖+1 above, Proposition 1 holds. are satisfied by π‘Š, which means 𝑝𝑗 is justified by the justified reduct of π‘Ÿ1β€² , … , π‘Ÿπ‘–+1 β€² . As a result, 𝑝 is 𝑗 More trivially, we can expand Proposition 1 to all kinds justified for every 𝐴 ̂𝑗 ∈ π‘Š,Μ‚ π‘Š Μ‚ is a world view of of M-cycle. Ξ β€² . Theorem 1 (Relationship between M-cycle and A-cycle). β€’ If π‘Š ⊭ M𝑝, the modal reduct of π‘Ÿ1 is π‘ž1 ← ¬¬𝐡1 .. Let Ξ  be an arbitrary ESGK program, Ξ β€² be an 𝐸𝑆D program Because βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 ⊭ 𝑝, 𝑝 must not be con- obtained by replacing every subjective literal of the form M𝑙 sistent with Ξ /π‘Ÿ, thus βˆ€π΄ ̂𝑖 ∈ π‘Š Μ‚ ∢ 𝐴𝑖 ⊭ C𝑝 and in rule π‘Ÿ with subjective literal A𝑙 if there is an edge labeled π‘Š ⊭ A𝑝, π‘Ÿ β€² is deleted from Ξ β€² in the modal reduct. with M from rule node π‘Ÿ to 𝑙 in an M-cycle. A view π‘Š of Ξ  As a result, π‘ŠΜ‚ is a justified view of Ξ β€² and equals under the semantics of ESGK if and only if its default view to the collection of default equilibrium models of Μ‚ is a world view of Ξ β€² . Μ‚ Μ‚ is a world view of Ξ β€² . image π‘Š Ξ β€²π‘Š , which means π‘Š Here is the sketch of the proof of Theorem 1. As shown For the completeness part, consider following situa- in the proof of Proposition 1, it needs to prove that the tions: modal reducts of rules in M-cycle and translated A-cycle Μ‚ ⊧ A𝑝, thus the modal reduct of π‘Ÿ1β€² w.r.t. π‘Š β€’ if π‘Š Μ‚ is under two semantics respectively are equal. The proof needs to consider the following situations: π‘ž1 ← 𝐡. By the definition of default view image, π‘ŠΜ‚ also satisfies 𝑝, thus βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 ⊧ 𝑝, π‘Š ⊧ M𝑝. 1. multiple rules in the cycle; The modal reducts of Ξ  and Ξ β€² are equal, thus π‘Š 2. rules with disjunctive heads in the cycle; is a world view of Ξ . 3. NAF operator Β¬ in the cycle; Μ‚ ⊭ A𝑝, π‘Ÿ β€² is deleted in the modal reduct Ξ β€²π‘ŠΜ‚ β€’ if π‘Š 4. modal operators K and Β¬K in the cycle; and βˆ€π΄π‘– βŠ­Ξ β€²π‘ŠΜ‚ C𝑝, thus βˆ€π΄π‘– ∈ π‘Š ∢ 𝐴𝑖 ⊭ 𝑝, π‘Š ⊭ Here we use multiple rules as an example. M𝑝, the modal reduct of π‘Ÿ1 is π‘ž1 ← ¬¬𝑝, 𝐡1 ., thus Μ‚ the modal reduct Ξ π‘Š = Ξ β€²π‘Š βˆͺ {π‘ž1 ¬¬𝑝, 𝐡1 .} and Proposition 2. For an ESGK program containing follow- Μ‚ Ξ β€²π‘Š is not consistent with 𝑝. It means 𝐴𝑆(Ξ π‘Š ) = ing rules 𝐴𝑆(Ξ β€²π‘Š ) = π‘Š, π‘Š is a world view of Ξ . π‘ž1 ← M𝑝, 𝐡1 . (π‘Ÿ1 ) According to the proof of soundness and completeness, π‘ž2 ← π‘ž 1 , 𝐡 2 . (π‘Ÿ2 ) Proposition 2 holds. β‹― π‘žπ‘– ← π‘žπ‘–βˆ’1 , 𝐡𝑖 . (π‘Ÿπ‘– ) Example 16 (Program with NAF and M-cycle). Consider 𝑝 ← π‘žπ‘– , 𝐡𝑖+1 . (π‘Ÿπ‘–+1 ) a program Ξ 14 : , π‘Š is a world view of Ξ  if and only if the default view 𝑝 ← Β¬π‘ž. image π‘ŠΜ‚ is a world view of the 𝐸𝑆D program containing 𝑝 π‘œπ‘Ÿ π‘ž ← Mπ‘ž. π‘ž1 ← A𝑝, 𝐡1 . (π‘Ÿ1β€² ) By the definition of world view of ESGK , the only world π‘ž2 ← π‘ž1 , 𝐡2 . (π‘Ÿ2β€² ) view of Ξ 14 is {{𝑝}, {π‘ž}}. The corresponding 𝐸𝑆D program is Ξ β€²14 β‹― π‘žπ‘– ← π‘žπ‘–βˆ’1 , 𝐡𝑖 . (π‘Ÿπ‘–β€² ) 𝑝 ← Β¬π‘ž. 𝑝 ← π‘žπ‘– , 𝐡𝑖+1 . β€² ) (π‘Ÿπ‘–+1 𝑝 π‘œπ‘Ÿ π‘ž ← Aπ‘ž. Assume π‘Š1 = {{𝑝}, {π‘ž}}, π‘Š2 = {{𝑝}}, π‘Š3 = {{π‘ž}}, π‘Š4 = [3] M. Gelfond, New Semantics for Epistemic Specifi- {{𝑝, π‘ž}}. It is obvious that π‘Š1 is a world view of Ξ β€²14 . For cations, in: Proceedings of the 11th International π‘Š2 consider following situations: Conference on Logic Programming and Nonmono- tonic Reasoning, volume 6645, Springer, Vancouver, β€’ assume π‘Š Μ‚2 = {⟨{𝑝}, {𝑝, π‘ž}⟩}, π‘Š Μ‚2 ⊧ Aπ‘ž, then π‘Š2 β‰  Canada, 2011, pp. 260–265. Μ‚ π‘Š 𝐷𝑆𝑀(Ξ β€² 142 ); [4] P. T. Kahl, Refining The Semantics For Epistemic β€’ assume π‘Š Μ‚2 = {⟨{𝑝}, {𝑝}⟩}, π‘ŠΜ‚2 ⊭ Aπ‘ž, then π‘Š2 β‰  Logic Programs, Phd, Texas Tech University, 2014. Μ‚ π‘Š [5] Y.-D. Shen, T. Eiter, Evaluating epistemic negation 𝐷𝑆𝑀(Ξ β€² 142 ), in answer set programming, Artificial Intelligence 237 (2016) 115–135. thus π‘ŠΜ‚2 is not a world view of Ξ 14 . It can be showed π‘Š3 , β€² [6] E. I. Su, L. F. del Cerro, A. Herzig, Autoepistemic π‘Š4 are not world views of Ξ β€² 14 , which means π‘Š Μ‚1 is the equilibrium logic and epistemic specifications, Artif. only world view of Ξ β€²14 . Intell. 282 (2020) 103249. [7] R. Reiter, A logic for default reasoning, Artificial 6. Conclusion Intelligence 13 (1980) 81–132. [8] M. Gelfond, H. Przymusinska, V. Lifschitz, In this paper, with some examples, we illustrate that the M. Truszczynski, Disjective defaults, in: Pro- defaults originated from permitted cannot be represented ceedings of the 2nd International Conference convincingly via the existing ASP and ES languages, and on Principles of Knowledge Representation and hence present logic programming languages to express Reasoning, Morgan Kaufmann, 1991, pp. 230–237. defaults originated from permitted. Especially, we also [9] K. Konolige, On the relation between default and compared the ability of expression and semantics of this autoepistemic logic, Artificial Intelligence 35 (1988) language with ESGK and proposed a translation from 343–382. GK programs of ES to programs of our language with [10] G. Gottlob, Translating default logic into standard epistemic defaults. It shows that the new language can autoepistemic logic, J. ACM 42 (1995) 711–740. also provide to separate the representation of permitted [11] M. Truszczynski, Modal interpretations of default and possibilities, which can eliminate the ambiguity of logic, in: Proceedings of the 12th International GK M in ES and other similar languages for Epistemic Joint Conference on Artificial Intelligence, 1991, pp. Specifications. 393–398. In the future, we are intend to find a simplified defini- [12] P. Cabalar, D. Lorenzo, New insights on the in- tion of justified views for a more intuitive semantics. We tuitionistic interpretation of default logic, in: Pro- are then planning to analyze the computational complex- ceedings of the 16th Eureopean Conference on Arti- ity of solving and develop an algorithm with acceptable ficial Intelligence, ECAI’2004, including Prestigious efficiency for our further study on the application of our Applicants of Intelligent Systems, PAIS 2004, Valen- language. After that, we will do some further research on cia, Spain, August 22-27, 2004, IOS Press, 2004, pp. the semantics of 𝐴𝑆𝑃D and 𝐸𝑆D , and see if their semantics 798–802. can be captured by classical ASP and ES. [13] M. Gelfond, V. Lifschitz, Classical negation in logic programs and disjunctive databases, New Gener. Comput. 9 (1991) 365–386. Acknowledgments [14] V. Lifschitz, Thirteen definitions of a stable model, in: Fields of Logic and Computation, Essays Dedi- The work was supported by the Pre-research Key Labo- cated to Yuri Gurevich on the Occasion of His 70th ratory Fund for Equipment (Grant No. 6142101190304). Birthday, volume 6300 of Lecture Notes in Computer Science, Springer, 2010, pp. 488–503. [15] Y. Chen, H. Wan, Y. Zhang, Y. Zhou, dl2asp: Imple- References menting default logic via answer set programming, [1] M. Gelfond, Y. Kahl, Knowledge Representation, in: T. Janhunen, I. NiemelΓ€ (Eds.), Logics in Artifi- Reasoning, and the Design of Intelligent Agents, cial Intelligence - 12th European Conference, JELIA Cambridge University Press, 2013. 2010, Helsinki, Finland, September 13-15, 2010. Pro- [2] M. Gelfond, V. Lifschitz, The stable model semantics ceedings, volume 6341 of Lecture Notes in Computer for logic programming, in: Proceedings of the Fifth Science, Springer, 2010, pp. 104–116. International Conference and Symposium on Logic [16] Y. Zhang, Y. Zhang, Epistemic specifications and Programming, volume 2, MIT Press, Cambridge, conformant planning, AAAI Workshop - Technical Massachusetts, USA, 1988, pp. 1070–1080. Report WS-17 (2017) 781–787.