Epistemic Reasoning in Logic Programs

1 Introduction

As a new logic programming paradigm developed by Gelfond, epistemic logic programming integrates epistemic notions such as knowledge and belief into disjunctive answer set semantics [Gelfond, 1994], which has an enhanced capacity to handle complex incomplete information reasoning and represent agents' epistemic behaviours. However, recently Zhang has shown that epistemic logic programming embeds a significantly higher computational complexity than non-disjunctive and disjunctive answer set programming (assuming that P ̸= NP and the polynomial hierarchy does not collapse) [Zhang, 2006]. Therefore, the question of whether there are some useful classes of epistemic logic programs that have a lower computational complexity becomes crucial to apply epistemic logic programming to practical domains.

In this paper, we undertake a deep study on this topic. We first refine some key notions of Gelfond's epistemic semantics and show its essential complexity properties. We then show that Lee and Lifschitz's result on loop formulas for disjunctive logic programs can be extended to a special class of epistemic logic programs. We also study the polysize model property for epistemic logic programs. Based on these discoveries, we eventually identify two non-trivial classes of epistemic logic programs whose consistency checking complexity is reduced from PSPACE-complete to NP-complete and ΣP2 -complete respectively. We observe that many important applications on epistemic representation fall into these two classes of epistemic logic programs.

2 Gelfond's Semantics for Epistemic Reasoning

2.1 Language, Structure and Satisfaction

We consider a language LG which is a propositional language augmented with two modal operators K and M to represent knowledge and belief respectively. Formulas of LG are standard propositional formulas augmented with Kϕ and Mϕ and are closed under ∧, ∨ and ¬. A G-structure V is a collection of sets of propositional literals called the set of possible states of an agent. A situation in a G-structure V is a pair (V, s), where s ∈ V. The satisfaction in LG is defined in terms of the truth relation and falsity relation between a formula and a situation. The truth of a formula ϕ in a situation (V, s), denoted as (V, s) |= ϕ, and the falsity, denoted as

• (V, s) =| ϕ, are defined as follows.
• (V, s) |= p iff p ∈ s where p is a propositional atom.
• (V, s) |= Kϕ iff (V, si) |= ϕ for all si ∈ V.
• (V, s) |= Mϕ iff (V, si) |= ϕ for some si ∈ V.
• (V, s) |= ϕ ∧ ψ iff (V, s) |= ϕ and (V, s) |= ψ.
• (V, s) |= ϕ ∨ ψ iff (V, s) |= ϕ or (V, s) |= ψ.
• (V, s) |= ¬ϕ iff (V, s) =| ϕ.
• (V, s) =| p iff ¬p ∈ s where p is an atom.
• (V, s) =| Kϕ iff (V, s) |= Kϕ does not hold 1 .
• (V, s) =| Mϕ iff (V, s) |= Mϕ does not hold.
• (V, s) =| ϕ ∧ ψ iff (V, s) =| ϕ or (V, s) =| ψ.
• (V, s) =| ϕ ∨ ψ iff (V, s) =| ϕ and (V, s) =| ψ.

It is clear that if a formula is of the formKϕ, ¬Kϕ, Mϕ or ¬Mϕ where ϕ does not contain operator K or M, that is, ϕ is an objective formula, then its truth value in (V, s) will not depend on s, and we call this formula subjective. In this case, (V, s) |= Kϕ (or (V, s) |= Mϕ) can be simply written as V |= Kϕ (or V |=Mϕ resp.) On the other hand, it is easy to see that an objective formula's truth value in (V, s) will only depend on s. Therefore, notion (V, s) |= ϕ may also be simplified as s |= ϕ. A propositional literal is also called an objective literal, and formulas KL, ¬KL, ML, ¬ML are called subjective literals where L is a propositional literal.

1 In this case, we will denote (V, s) ̸|= Kϕ.

It is important to notice that in Gelfond's semantics, (V, s) =| ϕ is not equivalent to (V, s) ̸|= ϕ in general. This is because by allowing s to be a set of propositional literals, an atom is not assigned a truth value in s if neither of the atom nor its negation is presented in s. Consequently, K and M are not dual modal operators 2 in LG. For instance, consider V = {{a, b}, {a, b, ¬c}}. Clearly we have V |= ¬K¬c. But we do not have V |=Mc.

A G-structure V is called consistent if for each s ∈ V, s does not contain a propositional atom as well as its negation. Otherwise, V is inconsistent and is denoted as V = {Lit} where Lit denotes the inconsistent set of all propositional literals.

Given a G-structure V, we say a formula ϕ is satisfied in V if there is some s ∈ V such that (V, s) |= ϕ. A formula ϕ is satisfiable if ϕ is satisfied in some consistent G-structure V. A consistent G-structure V is called a model of ϕ if for every s ∈ V, (V, s) |= ϕ, denoted as V |= ϕ. We may use Mod(ϕ) to denote the set of all models of ϕ.

Lemma 1 A formula ϕ of LG is satisfiable if and only if it is satisfied in a consistent G-structure with at most |ϕ| states, where |ϕ| denotes the length of formula ϕ.

Theorem 1 Deciding whether a formula is satisfiable is NPcomplete.

Given a satisfiable formula ϕ, very often the maximal model of ϕ is of a special interest in our study, as will be shown in section 3. Formally a G-structure V is a maximal model of ϕ if V is a model of ϕ and there does not exist another consistent V ′ such that V ′ |= ϕ and V ⊂ V ′ . Consider formula K(a ≡ ¬b), it has three models {{a, ¬b}}, {{¬a, b}} and {{a, ¬b}, {¬a, b}}, where only the last one is a maximal model. On the other hand, formula ((a ∧ ¬b) ≡ ¬Mb) ∧ ((¬a ∧ b) ≡ ¬Ma) has two models {{a, ¬b}} and {{¬a, b}} and both are maximal models.

Proposition 1 Let ϕ be a formula of LG and let V be a Gstructure. Deciding whether V is a maximal model of ϕ is co-NP-complete.

2.2 World View Semantics for Epistemic Logic Programs

We specify an epistemic logic program in language LG to be a finite set of rules of the form:

and constraints of the form:

In (1) and (2), F1, · · · , Fk are objective literals, G1, · · · ,Gm are objective or subjective literals, and Gm+1, · · · ,Gn are objective literals. Sometimes, we also present a rule in the form head ← body, where head = {F1, · · · , Fk} and body = {G1, · · · ,Gm, not Gm+1, · · · , not Gn}. Note that if head = ∅, then the rule becomes a constraint; and if body = ∅, i.e. head ←, it means that head should be true without any condition.

2K and M are called dual if ¬K¬ϕ is equivalent to Mϕ.

For an epistemic logic program Π without constraints, its semantics is given by its world view which is defined in the following steps:

Step 1. Let Π be an epistemic logic program not containing modal operators K and M and negation as failure not. A set s of propositional literals is called a belief set of Π iff s is a minimal set of satisfying conditions: (i) for each rule F ← G1, · · · , Gm from Π such that s |= G1 ∧ · · · ∧ Gm we have s |= F (F is F1 ∨ · · · ∨ Fk); and (ii) if s contains a pair of complementary literals then we write s = Lit.

Step 2. Let Π be an epistemic logic program not containing modal operators K and M and s be a set of propositional literals in the language of Π. By Πs we denote the result of (i) removing from Π all the rules containing formulas of the form not G such that s |= G and (ii) removing from the rules in Π all other occurrences of formulas of the form not G. We call s is a belief set of Π if it is a belief set of Πs.

Step 3. Finally, let Π be an arbitrary epistemic logic program and V a collection of sets of propositional literals in its language. By ΠV we denote the epistemic logic program obtained from Π by (i) removing from Π all rules containing formulas of the form G such that G is subjective and V ̸|= G, and (ii) removing from rules in Π all other occurrences of subjective formulas.

Now we define that a collection V of sets of ground literals is a world view of Π if V is the collection of all belief sets of ΠV. Clearly, a world view of an epistemic logic program is also a G-structure in language LG.

It is easy to extend the world view definition above for epistemic logic programs Π with constraints: V is a world view of Π if V is a world view of the program obtained by deleting all constraints from Π, and for each constraint in Π of the form (2), either V ̸|= Gi for some 1 ≤ i ≤ m, or V |= Gj for some (m + 1) ≤ j ≤ n. An epistemic logic program may have one, more than one, or no world views.

Theorem 2 [Zhang, 2006] Deciding whether an epistemic logic program has a world view is PSPACE-complete.

It is easy to see that extended/normal logic programs and disjunctive logic programs are two special classes of epistemic logic programs whose world views always exist. Although computing the world view (i.e. the collection of all stable models/answer sets) for these types of programs could be difficult (this will be addressed in section 7), in general, we are more interested in discoverying non-trivial classes of epistemic logic programs with a lower computational complexity.

3 Completion for Epistemic Logic Programs without Positive Knowledge

Let us consider a simple epistemic logic program Π = {a ← ¬Mb}. This program has one world view {{a}}. However, under the previous G-structure semantics, Π's equivalent formula ¬b∧(a ≡ ¬Mb)3 has a unique model {{a, ¬b}}, which is obviously different from Π's world view. This inconsistency can be avoided if we slightly revise the definitions of G-structure and the associated satisfaction in LG .

To begin with, we first need to remove negative propositional atoms from epistemic logic programs. An epistemic logic program Π is said in canonical form if no negative propositional atom occurs in Π. Note that this does not exclude occurrences of negative subjective formulas in Π. For instance, program {a∨b ← ¬Mc} is to be in canonical form, while program {a∨b ← ¬M¬c} is not. For an arbitrary program Π, we can always transform it into the canonical form by introducing new propositional atoms in the language. In particular, for each atom a in LG, we introduce a new atom a′ to represent literal ¬a. Therefore, by replacing each negative atom ¬a occurring in Π with the corresponding new atom a′ , the resulting program, denoted as Πc , is in canonical form. If V is a G-structure in language LG, V c is obtained by replacing each negative atom occurring in V with the corresponding new atom.

Proposition 2 Let Π be an epistemic logic program and Πc be Π's canonical form. A consistent G-structure V is a world view of Π if and only if V c is a world view of Πc .

Due to Proposition 2, in the rest of this paper, we can assume that all epistemic logic programs are in canonical form in our context. Now we re-define a G-structure to be a collection of sets of propositional atoms. Consequently, we revise the falsity relation in LG as follows: (V, s) =| ¬p iff p ̸∈ s (p is a propositional atom), while the truth relation and falsity relation for all other formulas remain the same. We should mention that this change will imply that K and M become dual modal operators in LG (recall that in section 2.1, we showed that K and M are not dual operators). Despite this difference, this new satisfaction will not affect the world view definition for epistemic logic programs.

Given an epistemic logic programΠ, we use Atom(Π) to denote the set of all atoms occurring in Π. Now we define a class of epistemic logic programs without positive knowledge, denoted as ELP -K . That is, for each Π ∈ ELP -K , no knowledge operator K positively occurs in the body of each rule. It is easy to obverse that many typical epistemic logic programs in applications are actually ELP -K programs [Gelfond, 1994].

Definition 1 Let Π be an ELP -K program. The completion of Π, denoted as Comp(Π), consists of the following formulas: (1) if head ← body is a rule in Π, then the following formula is in Comp(Π)4 :

(2) for each a ∈ Atom(Π), the following formula is in Comp(Π):

3 Later we will see that this formula is the completion of Π.

4 When we view body as a formula in language LG, the negation as failure not in body is interpreted as the classical negation ¬.

and (3) for each a ∈ Atom(Π), if there is no rule head ← body in Π such that a ∈ head, then ¬a is in Comp(Π).

Example 1 Let Π consist of the following rules:

Clearly, Π is an ELP -K program. From Definition 1, Comp(Π) consists of the following formulas:

It is easy to check that Π has a unique world view {{a, d}, {b, d}}, which is also the unique model of Comp(Π). □

In general, Definition 1 cannot be extended to arbitrary epistemic logic programs. Consider the following program Π′ :

If we apply Definition 1 to Π′ , its completion is the same as in Example 1 except formula d ≡ ¬Ka is replaced by d ≡ Ka. We can see that Π′ has one world view {{a}, {b}}, where Comp(Π′ ) has two maximal models {{a}, {b}} and {{a, d}}. Since Π′ does not contain any loop (see next section), Definition 1 actually does not provide a precise completion characterization for arbitrary epistemic logic programs.

The following proposition establishes an important connection between an ELP -K program and its completion.

Proposition 3 Let Π be an ELP -K program. If V is a world view of Π, then it is also a maximal model of Comp(Π).

4 Loop Formulas for ELP -K Programs

Now we show that Lee and Lifschitz's loop formula result for disjunctive logic programs [Lee and Lifschitz, 2003] can also be extended to ELP -K programs.

Given an epistemic logic program Π, the positive dependency graph of Π, denoted as G+Π , is the directed graph constructed in the following way: the set of vertices is Atom(Π) ∪ KM(Π), where KM(Π) is the set of all subjective atoms occurring in Π, and for each pair of vertices x, y ∈ Atom(Π) ∪KM(Π): (1) there is an edge from x to y if there is a rule head ← body in Π, such that x ∈ head, and y positively occurs in body; (2) for each path in the graph formed from (1), if both a and Ka (or Ma) occur in the path, then for any x′ , y′ ∈ Atom(Π) ∪ KM(Π) such that (x′ , a) and (a, y′ ) are edges, add edges (x′ ,Ka) and (Ka, y′) ((x′ ,Ma) and (Ma, y′ ) resp.) respectively; (3) based the graph formed from (1) and (2), if there is no such cycle containing vertex a but not Ka (Ma resp.), then remove vertex a and all its associated edges. We may use Pos(body) to denote the set of all (objective and subjective) atoms positively occurring in body. We call a nonempty set L ⊆ Atom(Π) ∪ KM(Π) a loop of Π if for any x and y in L, there is a path in G+Π from x to y with length > 0.

Definition 2 Let Π be an epistemic logic program and L a loop of Π. R(L) is denoted as the set of following formulas:

for each rule head ← body in Π such that head ∩ L ̸= ∅ and Pos(body) ∩ L = ∅. Then the loop formula LF(L) associated with L in Π is specified as

We use LF(Π) to denote the set of all loop formulas in Π.

It is easy to see that (5) is equivalent to Lee and Lifschitz's disjunctive loop formula [Lee and Lifschitz, 2003] and Lin and Zhao's loop formula [Lin and Zhao, 2004] if Π is restricted to a disjunctive logic program and a normal logic program respectively.

Example 2 Consider an epistemic logic programΠ:

Π has one loop L = {a,Mc}. Then we have R(L) = ∅, and LF(L) = {¬(a ∨Mc)}. On the other hand, since Π is an ELP -K , Π's completion Comp(Π) consists of the following formulas:

Mc ⊃ a ∨ b, a ⊃ ((¬b ∧ Mc) ∨ c), b ⊃ (¬a ∧ Mc), c ⊃ a, d ≡ ¬Ka.

We can see that Comp(Π) has two (maximal) models {{a, c}} and {{d}}, where Comp(Π)∪LF (L) has one (maximal) model {{d}}, which is also the unique world view of Π. □

Theorem 3 Let Π be an ELP -K program, Comp(Π) the completion of Π, and LF(Π) the set of loop formulas of Π. A G-structure is a world view of Π if and only if it is a maximal model of C omp(Π) ∪ LF (Π).

4.1 Proof of Theorem 3

In order to prove Theorem 3, we need to first show some important properties of formulas and epistemic logic programs in language LG. We first introduce the notion of epistemic reduction for formulas.

Let V be a G-structure and ϕ a formula of LG. A formula ϕV is called the epistemic reduction of ϕ with respect to V if ϕV is obtained from ϕ in the following way: (1) for each ϕ's subformula of the form Kφ (here φ is objective), Kφ is replaced by φ if V |= Kφ, otherwise Kφ is replaced by F; and (2) for each ϕ's subformula of the formMφ, Mφ is replaced by T if V |= Mφ, otherwise Mφ is replaced by F.

Consider formula ϕ = Ka ∨ Mb. Suppose a and b are the only propositional atoms in the language. Then V = {∅, {a}, {b}, {a, b}} is a maximal model of ϕ. Furthermore, we can see that ϕV = T, where V is exactly the set of all models of ϕV .

Proposition 4 Let ϕ be a formula of LG and let V be a Gstructure. Then V is a maximal model of ϕ if and only if Mod(ϕV ) = {s | s ∈ V}.

Now with a slight change, we may extend the notion of epistemic reduction to epistemic logic programs. Let Π be an epistemic logic programs and V be a G-structure in language LG. A disjunctive logic program (without containing any K and M operators) eReduct(Π, V) is called the epistemic reduction of Π under V if it is obtained fromΠ in the following way: (1) removing all rules from Π where G is a subjective literal occurring in the rules and V ̸|= G, and (2) removing all other occurrences of subjective literals in the remaining rules (i.e. replacing those G with T due to V |= G). Then we have the following results.

Proposition 5 Let Π be an epistemic logic program and V a G-structure of LG. V is a world view of Π if and only if V is the collection of all stable models of disjunctive logic program eReduct(Π, V).

The following two lemmas establish an important connection between an ELP -K program and its completion and loop formulas.

Lemma 2 Let Π be an ELP -K program and V a world view of Π. Then (Comp(Π) ∪ LF(Π))V ≡ Comp(eReduct(Π, V)) ∪ LF (eReduct(Π, V)).

Lemma 3 Let Π be an ELP -K program and V a maximal model of Comp(Π) ∪ LF(Π). Then (Comp(Π) ∪ LF(Π))V ≡ Comp(eReduct(Π, V)) ∪ LF (eReduct(Π, V)).

Proof of Theorem 3: Consider an ELP -K program Π and Comp(Π) ∪LF (Π). We show that V is a world view of Π iff V is a maximal model of Comp(Π) ∪ LF (Π).

(⇒) Suppose V is a world view of Π. Then from Proposition 5, we know that V is the collection of all stable models of disjunctive program eReduct(Π, V). On the other hand, from Lemma 2, we have (Comp(Π) ∪ LF(Π))V ≡ Comp(eReduct(Π, V)) ∪ LF(eReduct(Π, V)). On the other hand, from Theorem 1 in [Lee and Lifschitz, 2003], we know that each stable model of program eReduct(Π, V) is also a model of formula Comp(eReduct(Π, V)) ∪ LF(eReduct(Π, V)). So we conclude V = Mod((Comp(Π) ∪ LF(Π))V ). Finally, from Proposition 4, it follows that V is a maximal model of Comp(Π) ∪ LF (Π).

(⇐) Suppose V is a maximal model of Comp(Π) ∪ LF (Π). From Lemma 3, we know (Comp(Π)∪LF (Π))V ≡ Comp(eReduct(Π, V)) ∪ LF(eReduct(Π, V)). According to Proposition 4, on the other hand, V = Mod((Comp(Π) ∪ LF(Π))V ). Then from Theorem 1 in [Lee and Lifschitz, 2003], each model of Comp(eReduct(Π, V)) ∪ LF(eReduct(Π, V)) is also a stable model of disjunctive logic program eReduct(Π, V). Finally, from Proposition 5, it follows that V is a world view of Π. This completes our proof of Theorem 3. □

5 Polynomial Bound on Loop Formulas

Since there may be an exponential number of loops in an epistemic logic program, the way of transforming an ELP -K

program into Comp(Π) ∪ LF (Π) and then computing its Gstructures will not have particular computation advantages. However, we will show that for ELP -K programs with polynomially bounded numbers of loop formulas, the consistency check problem will be significantly reduced from PSPACEcomplete to NP-complete. Formally, given an epistemic logic program Π, we say that Π has a polynomial bound on its loop formulas if the number of cycles in G+Π is bounded by O(f(|G+Π |)) where f(|G+Π |) is a polynomial of |G+Π |.

Theorem 4 Let Π be an ELP -K program that has a polynomial bound on its loop formulas. Deciding whether Π has a world view is NP-complete.

Proof: Here we only give membership proof. From Theorem 3, Π has a world view iff Comp(Π) ∪ LF (Π) has a maximal model. Clearly, if the number of cycles in G+Π is bounded by O(f(|G+Π |)), then the size of formula Comp(Π) ∪ LF(Π) is also bounded by O(f(|G+Π |)). So we can guess such LF(Π) in polynomial time with a nondeterministic Turing machine. From Theorem 1, we know that checking whether Comp(Π) ∪ LF(Π) has a model is in NP. Also it is easy to see that Comp(Π) ∪LF(Π) has a model iff it has a maximal model. □

In the following, we provide a polynomial upper bound on the number of loop formulas for an epistemic logic program. Given an epistemic logic program Π and a ∈ head(Π), an inference chain of a is a sequence of atoms (a, b1, · · · , bl-1, bl), where a, b1, · · · , bl are different atoms in Atom(Π), and there are l different rules r1, · · · , rl in Π such that a ∈ head(r1), b1 ∈ Pos(body(r1)), b1 ∈ head(r2), b2 ∈ Pos(body(r2)), · · ·, bl-1 ∈ head(rl) and bl ∈ Pos(body(rl)). For each a ∈ head(Π), it may have one or more inference chains. The inference depth of a, denoted as i-depth(a), is the length of a's longest inference chain. The inference depth of Π is defined as i-depth(Π) = max(i-depth(a) : a ∈ head(Π)).

Proposition 6 Let Π be an epistemic logic program. If i-depth(Π) < k for some fixed k, then |LF(Π)| is bounded by O((2k /k!) · nk ), where |Atom(Π)| = n.

Proposition 7 Let Π be an epistemic logic program. For a fixed k, deciding whether i-depth(Π) < k is solvable in time O(k · nk+1 ) where |Atom(Π)| = n.

6 PolysizeModel Property

Some special modal logics such as single agent S5 and KD45 [Blackburn et al., 2001] have polysize model property which brings the consistency check (satisfiability problem) in these logics down to NP-complete. We have shown that Gelfond's epistemic semantics also has this property (i.e. Lemma 1). However, epistemic logic programs under the world view semantics do not satisfy the polysize model property in general. For instance, the following program

xi ∨ x′i ←, yi ← ¬My′i , y′i ← ¬Myi, where i = 1, · · · , n,

has an exponential number of world views and each world view contains an exponential number of belief sets. Nevertheless, it is easy to observe that many specific epistemic logic programs indeed satisfy the polysize model property. Consequently, we can further identify an important class of epistemic logic programs whose consistency check is ΣP2 - complete.

Definition 3 An epistemic logic program Π is said to satisfy the polysize model property if either Π has no world view, or for each Π's world view V, |V| is bounded by O(f(|Π|)), where f(|Π|) is a polynomial of |Π|.

Theorem 5 Let Π be an epistemic logic program satisfying the polysize model property. Deciding whether Π has a world view is ΣP2 -complete.

Proof: Since for each world view V of Π, |V| is bounded by O(f(|Π|)), we can guess, in polynomial time, a k with k being bounded by O(f(|Π|)) and a collection V consisting of k different sets of atoms. Then we check whether V is a world view of Π in the following way: (1) transform Π into a disjunctive logic program ΠV by performing Step 3 in section 2.2, and (2) for each s ∈ V, check whether s is a stable model of ΠV. Clearly, (1) can be done in polynomial time, and (2) is solvable with k queries to an NP oracle.

Hardness proof. The hardness is proved by a reduction of the validity of QBF A = ∃x1 · · · ∃xn∀y1 · · · ∀ymA′ (n,m ≥ 1), where A′ = D1 ∨ · · · ∨ Dh and each Dk = lk,1 ∧ lk,2 ∧ lk,3 is a conjunction of propositional literals li,j over {x1, · · · , xn, y1, · · · , ym}. We know that deciding whether A is valid is ΣP2 -complete [Papadimitriou, 1995]. We construct in polynomial time an epistemic logic program Π from A and show that Π has a world view and each of its world views contains exactly one belief set if and only if A is valid. In particular, Π is constructed on propositional atoms {x1, · · · , xn, y1, · · · , ym}∪{x′1 , · · · , x′n , y′1 , · · · , y′m}∪ {valid, invalid}, where x′ and y′ are used to imitate the negations of x and y respectively. Π consists of the following

invalid ← ¬Minvalid, not valid,

where ρ(l) = a if l = a and ρ(l) = a′ if l = ¬a for any a ∈ {x1, · · · , xn, y1, · · · , ym}. It is easy to see that if Π has a world view V, then V must only contain one belief set. Then we can show that Π has a world view if and only if A is valid. □

Now we investigate under what conditions, an epistemic logic program will satisfy the polysize model property. We first define the dependency graph for an epistemic logic program. The dependency graph GΠ of Π is a directed graph where the set of vertices is Atom(Π); and for vertices a and b, there is an edge (a, b) from a to b if there is a rule head ← body in Π such that a ∈ head and b ∈ body or a, b ∈ head (a ̸= b). The edge (a, b) is labeled with + if b positively occurs in body; (a, b) is labeled with - if not b occurs in body or b occurs in head (assuming a ̸= b); and (a, b) is labeled with -K or -M if ¬Kb or ¬Mb occurs in body respectively. A cycle in GΠ is called negative cycle if the cycle has at least one edge labeled with - while all other edges in the cycle (if there are some) are labeled with +. A cycle is called a mixed negative cycle if the cycle has at least one edge labeled with -K or -M.

Proposition 8 Let Π be an epistemic logic program, GΠ its dependency graph and k a fixed number. Then the following results hold:

1. If GΠ has k negative even cycles 5 and Π has a world view, then Π's each world view contains at most 2k belief sets;
2. If GΠ has k mixed negative even cycles, then Π has at most 2k world views;
3. If GΠ has k negative even cycles but has no mixed negative even cycle, then either Π has no world view or has a unique world view containing at most 2k belief sets.

Corollary 1 For any epistemic logic program Π where its dependency graph GΠ has a fixed number of negative even cycles, deciding whether Π has a world view is ΣP2 -complete.

7 Concluding Remarks

As argued by Gelfond, epistemic logic programming has a rich expressive power for epistemic representation which other modal nonmonotonic logics do not have. Nevertheless, as shown in [Zhang, 2006], the enhanced expressive power is due to a higher computational cost than other nonmonotonic logics and logic programming paradigms. Although this is the case in general, as we will observe next, many important applications of epistemic representation actually fall into the two classes of epistemic logic programs that we identified earlier.

One important application of epistemic logic programming is to represent the epistemic closed world assumption (ECWA) which involves a strong introspection. It was noted that other logic programs and modal nonmonotonic logics such as autoepistemic logic [Marek and Truszczynski, 1991] usually have difficulties to handle it. As demonstrated in [Gelfond, 1994], representing ECWA is important when disjunctive information is presented in the agent's knowledge base. In epistemic logic programs, ECWA can be simply represented by rules like

for all atoms in the language 6 . We observe that adding such ECWA rules into an epistemic logic program neither introduces any new loop formulas nor increases the size of world views of the program, although they may generate more world views. Therefore, in principle ECWA rules do not add an extra burden on the world view computation for an epistemic logic program.

5 A cycle contains an even number of edges labeled with -.

6 Here a′ is used to represent the negation of atom a.

Now let us examine the following normal logic program Π∗ given in [Lifschitz and Razborov, 2006]:

If we view Π∗ as an epistemic logic program, then this program does not belong to either of the two classes we identified earlier. Computing Π∗ 's world view would be hard because Π∗ has 2n loop formulas and the unique world view also contains 2n2 belief sets.

Program Π∗ defines the reachability in arbitrary directed graphs. Finding a reachable path from r1 to ri is to compute one answer set containing ri. When we review Π∗ as an epistemic logic program, we have to compute the world view that is the collection of all answer sets of Π∗ . This actually can be avoided if we rewrite Π∗ to Π† as follows:

Program Π† has an exponential number of world views but each one only contains one belief set of size 2n. Then under program Π† , to find a reachable path from r1 to ri, we only need to compute one world view of Π† where its belief set contains ri. In this way, the computation is the same as that of programΠ∗ under the answer set semantics.