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 diference between epistemic operators examples in the paper are used to illustrate the necessity of using permitted operators in ASP and its extensions. answer set prolog, epistemic specifications, epistemic defaults under stable semantics [2] with plenty of extensions. Example 2. “ if is possible” is often encoded as an ES ASPOCP 2021: Workshop on Answer Set Programming and Other 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
Furthermore, let us see the introspection situation in
Answer Set Prolog (ASP) [
is true, but a belief
may not contain it. Rule ( 2″)
in its body, which can
Epistemic Specifications (ES) is one of these extensions
that allow for introspective reasoning with incomplete
knowledge through epistemic operators. Gelfond [
Example 1 ( by default). An interpretation of “ by default” is “ is true if it is permitted.” Under this intermitted”, the belief set is {}. answer set {}.
There are usually two ASP programs Π1 and Π2 that are used to encode “ by default” respectively. Π1 ∶ { ← ¬¬.} , where ¬ denotes negation as failure (NAF). Π2 ∶ { ← ¬ ∼ .} , where ∼ denote strong negation. However, neither Π1 nor Π2 follows our interpretation. Π1 has two answer sets, {} and {}. Π2 seems fine, but Π2 ∪ {← .} is not satisfiable, which we expect to have an nEvelop-O ←
M.
However, Π3 has an unique world view {∅}, which is against our interpretation that “ is true because is permitted”, and we expect a world view {{}} .
Here we have another example of introspection in
Example 3, which is a variant of an example in [
There are two rules about the sentinel’s introspection by a classical ES rule ←
M .
However, we can not find an accurate ES rule to express the second one, which can be interpreted as the sentinel should keep alert if is permitted by some belief sets. For instance, we try to describe the sentinel’s introspection with the following rules.
← ← ¬
M .
K ∼ .
( 1) ( ′)
2 ( 2″) semantics we want. not be derived if there is no rule with ∼ head. Therefore, neither rule ( 2′) nor rule ( 2″) has the in its
Hence, this paper aims to develop the extensions of ASP and ES respectively to address the issues of handling defaults originated from permitted expressions. Specifically, we develop two extensions of ASP, which are called ASPD and ESD respectively, 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. Intuitively, “ by default” can be encoded as ← ASPD, and “ if is possible” can be encoded as ← in ESD. Furthermore, the second rule in Example 3 can C. in
A. be written as
default.
rules of the form
Defaults are very useful in logic programs because they
allow drawing conclusions based on commonsense or
typical knowledge with incomplete knowledge. Default
Logic (DL) [
The defeasible rules in default logic are called default ∶ 1, … , (1) where , ,
are classical formulas. is the prerequisite of the default, s are justifications , is the consequent.
The default rule 1 intuitively means ”If is provable and all s are consistent with it, then assume as default.”
A default rule is normal if is equivalent to ; it is seminormal if implies . A default theory is a pair (, ) where is a set of default rules, and is a set of formulas.
Definition 1 (Extension of Default Theories). Let (, ) be a default theory, be a set of formulas. Define 0 = and for ≥ 0 : ={ ∶ 1, … , ∈ | ∈
+1 = ℎ( ) ∪ {( )| ∈ , ∀ ∶∼ ∉ }
}. where ℎ( ) is the set of all classical propositional consequences of , ( ) rule . Then is an extension for (, )
if = Note that we use operator ¬ for negation as failure (NAF) and ∼ for classical negation in this paper. An extension of
∞ ⋃=0 .
is the consequent of the default represents a possible set of beliefs of
Gelfond et al. [
if is one of the minimal deductively closed set of formulas ′, where for any default rule from , if ∈ ′ and ∼ 1, … , ∼ ∉ ,
Researchers have paid much attention to the relationships between modal logic and default logic to capture the semantics of default logic. They have found many inherent connections between these two kinds of knowledge.
Konolige [
The rest of this paper is organized as follows. In Sec- Let (, ) be a disjunctive default theory, be a set of Epistemic Specifications (ES) extends traditional answer An ES program is a finite set of rules of the form: set programs with epistemic modal operators K and M. Figure 1: Modal support graph of Π4 with M-cycle
1 … ← +1 , … , , 1, … , .
(3) K, ¬K, M, or ¬M. where is a literal, s are objective literals of the form or ¬ , s are subjective literals with an epistemic operator
A belief set of an ES program Π is a consistent set of literals in the language of Π. A view is a collection of belief sets. If an extended literal is satisfied by a point structure ⟨, ⟩ , where ∈
, is defined as: • ⟨, ⟩ ⊧ • ⟨, ⟩ ⊧ ¬ • ⟨, ⟩ ⊧ • ⟨, ⟩ ⊧ • ⟨, ⟩ ⊧ ¬ • ⟨, ⟩ ⊧ ¬ if ∈ , where is a literal.
if ∉ .
K if ∀ ∈ ∶ ⊧ M if ∃ ∈ ∶ ⊧
K if ∃ ∈ ∶ ⊭ M if ∀ ∈ ∶ ⊭ MS graph for short, is a directed graph where: Extended Literal
Label K ¬ K ¬K M ¬ M ¬M q M r2 r1 : :
M
p node ; denoting the rule; • for each rule in Π, there is a rule node labeled by • for each distinct objective literal in the language
of Π, there is a literal node labeled by ; • for each objective literal in the head of rule , there
is an unlabeled edge from the rule node to literal • for each extended literal in the body of rule , there is an edge labeled according to Table 2 going from literal node to rule node .
Definition 6 (M-Cycle). A cycle in the MS graph of an epistemic logic program is called an M-cycle if labels an edge within the cycle.
Example 4 (M-cycle). Consider a program Π4: ← M, ¬. ← M, ¬.
under the semantics of ESGK. However,
many researchers claimed their disagreement against this
example, including Yi-Dong shen [
The aim of justified semantics of ES, which we called ESZZ in this paper, is to develop an intuitive understanding of the M operator and get rid of circular justification in a stronger sense. It refines the semantics of Epistemic Specifications by constructing a justified reduct and disjunction reduct. By the new semantics, since all literals in a world view need to be justified, the M-cycle does not cause a self-support problem.
ESZZ provides a classical method to define the views with a maximal guess of epistemic negations. = { call 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 Π if is the unique stable model , ) ) .
,∨ a maximal view if is the collection of all answer
of ⋃=1 Πfull 2. removing rules whose body contains a subjective 3. replacing every occurrence of subjective literal in rule or its copies by a literal in (, ).
Example 6 (Continuing Example 5). The modal reduct of Π5 w.r.t. , 1, is
This section introduce the syntax and semantics of ASPD, which extends ASP with operator C.
An ASPD program Π is a finite collection of rules of the form where are extended literals of the form or ¬ , s are literals in classical logic, are default literals of the form C or ¬C . Intuitively, C means it is permitted (or not forbidden) to assume is true, and ¬C means is proved to be not permitted. A rule containing operator C is a default rule.
Example 7. Consider the following default logic programs Π6 and Π′6 ( ). ( ) ← ( ), ( ). ← ( ), ( ).
C ( ).
. However, with the addiinconsistent to assume that ( ) tional fact rule ( 3) and constraint rule ( 4) in Π′6, it is is true. Thus ( ) ′ is not in the consequent of Π6 ∪ Π6.
Example 7 illustrated the semantics of ASPD we have defined intuitively. Now we will give a formal definition. C C¬ ¬C ¬C¬ ⟨ , ⟩ ⊧ remove remove replace with ¬ replace with ⟨ , ⟩ ⊭ replace with replace with ¬ and Π7″: defaults neither.
On the one hand, Π′7 has three answer sets, {, } , {} , and {}. Apparently {} is not a stable model of Π7 that we want, thus ¬¬ can not represent defaults. On the other hand, Π7″ is unsatisfiable, which means ¬ ∼ can not represent
ASPD also provides a method to represent negative defaults, which is not provided by classical default logic. be an ASPD program. A literal set , where ⊆ (Π) Definition 16 (Stable Models of ASPD programs). Let Π is called a stable model of Π if ∃ ∶ ⟨, ⟩ ∈ (Π) ,
The set of all stable models of the program Π is denoted by 2 = ⟨{}, {}⟩ , 3 = ⟨{}, {}⟩. {, } is an answer set of Π7 1
7 3). However, there exists ′ = {, } that two stable models {, }
′ ASP programs Π7: not a default stable model of Π7, and (Π 7) = {{, }, {}} .
Example 8 is a typical instance of ASPD that shows the feature of the operator C. Neither ¬¬ nor ¬ ∼ can capture the semantics of C . For example, program Π7 has and {} . Considering following , and this default ′ ⊧ Π⟨{},{,}⟩ , and Φ( 3, Π) ⊂ Φ( ′, Π7). Therefore, 3 is ← ←
C.
C.
← , . ← . ← ¬¬. ← ¬¬.
← , . ← . ← ¬ ∼ . ← ¬ ∼ .
← , . ← . sider the ASPD program Π8 Example 9 (Programs with Defaults and Negation). Conand the ASPD program Π9 ← ¬ C. ←
C¬. and default interpretations 1 = ⟨{}, {}⟩ , and 2 = ⟨∅, {}⟩ .
For program Π8 and 1, we have Π8 1 = { ← ¬.} and {{}} = (Π interpretation 1′ = ⟨{}, {, }⟩ 8 1). However, there is another default
that Π8 1′ = {} and {, } ⊧ the third condition in Definition Π8 1′, and Φ({, }, Π 8) = {C} while Φ({}, Π 8) = ∅. By
15, 1 is not a default stable model of Π8. Because {} is not an answer set of Π8 1′, subjective literal . K ¬K M ¬M A ¬A epistemic defaults and be a non-empty collection of belief sets, where a belief set is a default interpretation ⟨ , ⟩ .
The modal reduct of Π w.r.t , denoted by Π , is an ASPD program obtained from Π as Table 5 by eliminating every
Definition 18 is a modification of the modal reduct of traditional Epistemic Specifications. The last two rows define the reduct of the new subjective operator A. However, we still need a method to reduce the circular justifications: subjective interpretation and justified reduct.
Definition 19 (Subjective Interpretation). Let Π be a program with epistemic defaults, = { 1, … , } be a collection of belief sets. The mapping from subjective literal and belief set is defined as (, )for all , ∈
9 2). However, there exists a default interpretation 2′ = ⟨∅, {}⟩ , and Φ({}, Π 9) = {C¬} . Meanwhile, Φ({}, Π 9) = ∅, Π9 2′ = {.} , thus {} ⊧ Π 9 2′. Therefore, 2 is not a default stable model of Π9. It is easy to check that 1 is a default stable model of Π9.
16, 1′ is not a default
Example 9 shows how does ASPD deal with the nega- : tion of defaults and how does the function Φ works.
Now, let us revisited Example 1. “ by default” can be described by an ASPD program containing only one rule: ←
C.
It is easy to check that {} is the unique stable model of the program as we expect.
← ←
A, ¬.
A, ¬. ( A, ) = C 2 for ∈ {1, 2} .
Let 1 = ⟨{}, {}⟩
, 2 = ⟨{}, {}⟩ , W = { 1, 2}. The subjective interpretations w.r.t. is ( A, ) = C 1 and an extension of ESZZ.
A rule of ESD is of the form This section introduces the syntax and semantics of ESD, literal with classical epistemic operators, the justified literals in ASPD) of the form or ¬ , s are subjective liter- gram Π10 with a self-supported of A. Example 10 (Subjective Interpretation). Considering proDefinition 20 (Justified Reduct) . Consider an ESD program Π, a collection of belief sets { 1, … , }. The justified reduct of obtained by the following steps:
Π w.r.t. ⟨ , ⟩ , denoted by Π⟨ , ⟩ , is 1. removing rule if there exists a subjective literal ∈ ( )
with operator K, ¬K, M or ¬M if ⊧ ; 2. replacing subjective literals in rule or its copies with literals in (,
) if ⊧ ; 3. replacing objective literals with .
The justified reduct of a program Π w.r.t.
shows the justification of all literals in
Π. However, a justified reduct is a default logic program with disjunctions, which is possible to have stable models not contained by .
Kl l Ml highest conviction lowest conviction :Ml :
l :Kl be a collection of default interpreta- the form M can be interpreted as ”it is safe to believe is reduct w.r.t. , Gelfond-Lifschitz reduct and disjunction reduct w.r.t. . is a justified view
of Π if ⟨, ∪ ⟩ the only default stable model of ⋃=1 Πfull only default stable models of Π101. Example 11 has shown that 1 is a justified view of Π10. Thus 1 is a world view
A ∧
A , the . 1 and 2 are the of Π10.
Consider 2 = {⟨∅, ∅⟩}. The modal reduct Π102 = { ← 2 10 ) = 2. The justified C, ¬. ←
C, ¬.} , and (Π Thus 2 is also a world view of Π10. 5. Relation with ESGK This section will compare the semantics of ESD to the one of ESGK, which we have introduced in Section 2. reduct of Π10 w.r.t. 2 is { 1 ← C 1, ¬ 1. 1 ← C 1, ¬ 1.}. unique belief set that contains ( ) . It means
Kahl [
Because the definition of the justified reduct and modal ⟨ 2, ⟩ . reduct of operator K and M is equal to Yan Zhang and
Yuanlin Zhang [
M and K will be omitted if the literals in this loop do not have any external support. As a result, a subjective literal of possible.”, and other rules or belief sets should justify the possibility of .
A further observation of the unjustified world views caused by operator M reminds us that the semantics of modal operator M may be ambiguous. In classical ES programs, the M-cycle of one rule is often used to express default information. For example, the traditional description “a bird can fly by default” is usually expressed in ES programs by the following rule:
However, for a bird jective literal M ( ) , the only justification of sub
is exactly this rule and the M ( )
is not justified by this belief set.
Example 14 (Continuing Example 3). Consider the following extension Π12 of the program in Example 3. 15, we can find that although
M-cycles’s semantics are defined diferently, operator
A provides a method to represent defaults information, which M-cycles represent Definition 24 (Default View Image). For a view of an ESGK program Π, the default view image ̂of is a collection of default interpretations that ̂= {⟨, ⟩| ∈ } ←
M, .
Proposition 1 (Relationship between direct M-cycle and A-cycle). Let Π be an ES program that every modal operator M in Π occurs in a rule of the form where is a collection of objective literals or extended subjective literals, Π′ be a program obtained from Π by replacing M with A. A collection of belief sets is a world view of Π under ESGK semantics if and only if its default view image ̂is a world view of Π′ under the semantics of D
. (6) (7)
Proof. Let rule be a rule in Π of the form (7), ′ is obtained from by replacing M with A . If ⊭ and ′ are satisfied, thus we only need to consider the
, both situations that ⊧
A , the modal reduct of ′ w.r.t ̂is . , thus ∀ ̂ ∈ ̂∶
̂ ⊧ . , ⊧ reducts of rest rules in Π and Π′ are equal, thus
{ ← ¬¬, .}
view of Π. is the collection of all answer sets of Π , which means is a world view of Π. • If ̂⊭
A , A is replaced by C in the modal reduct Π′ ̂. By the definition of satisfiability, ∀ ∈ ∶ ⊭
⊭Π′ ̂ C , thus ∀ ∈ ∶ M . The modal reduct of is ← ¬¬, . ⊭ , , thus the modal reduct of Π = Π′ ̂/{ ←
C, .}∪ , and Π′ ̂is not consistent with . ) = (Π ′ ) = , is a world According to the proof of soundness and completeness More trivially, we can expand Proposition 1 to all kinds above, Proposition 1 holds. of M-cycle.
Theorem 1 (Relationship between M-cycle and A-cycle). Let Π be an arbitrary ESGK program, Π′ be an D program obtained by replacing every subjective literal of the form M in rule with subjective literal A if there is an edge labeled with M from rule node to in an M-cycle. A view under the semantics of ESGK if and only if its default view of Π image ̂is a world view of Π′.
Here is the sketch of the proof of Theorem 1. As shown in the proof of Proposition 1, it needs to prove that the modal reducts of rules in M-cycle and translated A-cycle under two semantics respectively are equal. The proof needs to consider the following situations:
2. rules with disjunctive heads in the cycle; 3. NAF operator ¬ in the cycle; 4. modal operators K and ¬K in the cycle;
Here we use multiple rules as an example.
Proposition 2. For an ESGK program containing following rules , is a world view of Π if and only if the default view image ̂is a world view of the D program containing ⋯ ⋯ 1 ← M, 1
. we only need to prove the equivalence of rule ( 1) and 1. For the soundness part, considering Π′.
A , thus the modal reduct of 1′ w.r.t. ̂is 1 ← . By the definition of default view image, ̂also satisfies , thus ∀ ∈ ∶ The modal reducts of Π and Π′ are equal, thus ⊧ , ⊧
M .
is a world view of Π. • if ̂⊭
A , ′ is deleted in the modal reduct Π′ ̂ and ∀ ⊭Π′ ̂ C , thus ∀ ∈ ∶ M , the modal reduct of 1 is 1 ← ¬¬, 1., thus ⊭ , ⊭ the modal reduct Π
= Π′ ̂∪ { 1¬¬, 1.} and (Π
′ ) = , is a world view of Π. Π′ ̂is not consistent with . It means (Π ) =
According to the proof of soundness and completeness,
Example 16 (Program with NAF and M-cycle). Consider a program Π14:
← ¬. ←
M.
← ¬. ←
By the definition of world view of ES GK, the only world view of Π14 is {{}, {}} .
The corresponding D program is Π′14 • assume ̂2 = {⟨{}, {, }⟩} , ̂2 ⊧ A , then 2 ≠ • assume ̂2 = {⟨{}, {}⟩} , ̂2 ⊭ A , then 2 ≠ (Π (Π ′1̂42); ′1̂42), thus ̂2 is not a world view of Π′14. It can be showed 3, 4 are not world views of Π′14, which means ̂1 is the only world view of Π′14.
In this paper, with some examples, we illustrate that the defaults originated from permitted cannot be represented convincingly via the existing ASP and ES languages, and hence present logic programming languages to express defaults originated from permitted. Especially, we also compared the ability of expression and semantics of this language with ESGK and proposed a translation from programs of ESGK to programs of our language with epistemic defaults. It shows that the new language can also provide to separate the representation of permitted and possibilities, which can eliminate the ambiguity of M in ESGK and other similar languages for Epistemic Specifications.
In the future, we are intend to find a simplified definition of justified views for a more intuitive semantics. We are then planning to analyze the computational complexity of solving and develop an algorithm with acceptable eficiency for our further study on the application of our language. After that, we will do some further research on the semantics of D and D, and see if their semantics can be captured by classical ASP and ES.
The work was supported by the Pre-research Key Laboratory Fund for Equipment (Grant No. 6142101190304).