Evaluating Epistemic Negation in Answer Set Programming (Extended Abstract)

1 Introduction

Negation is a key mechanism in answer set programming (ASP) for reasoning with incomplete knowledge. There are multiple types of negation: default negation, strong negation, and epistemic negation. By abuse of notation, in this paper we use ¬, ∼, and not to denote these three negation operators, respectively. When default negation is available, strong negation is easily compiled away using new predicate symbols [Gelfond and Lifschitz, 1991] and thus it can be omitted. The default negation ¬F of a formula F expresses that there is no justification for adopting F in an answer set and thus F can be assumed false by default in the answer set; in contrast, the epistemic negation notF of F expresses that there is no evidence proving that F is true, i.e., F is false in some answer set. Justification in ASP is a concept defined over every individual answer set, while provability is a meta-level concept defined over a collection of answer sets, called a world view [Gelfond, 1991]. This means the two types of negation are orthogonal operations, where default negation works locally on each individual answer set, and epistemic negation works globally at a meta level on each world view.

With both default and epistemic negation, ASP is enabled to reason with different incomplete knowledge. For example, we can use the rule innocent(X) ← not guilty(X) to express the presumption of innocence, which states that one

∗This paper is an extended abstract of the article [Shen and Eiter, 2016] in Artificial Intelligence, 237:115-135, 2016.

Thomas Eiter

Institut f¨ur Informationssysteme, Technische Universit¨at Wien, Favoritenstraße 9-11, A-1040 Vienna, Austria

eiter@kr.tuwien.ac.at

is presumed innocent if there is no evidence proving s/he is guilty. We can also use rules of the form ¬p(X) ← not p(X) to explicitly state Reiter's closed-world assumption (CWA) [Reiter, 1978], i.e., if there is no evidence proving p(X) is true we jump to the conclusion that p(X) is false.

However, observe that most of the existing answer set semantics, such as those defined in [Gelfond and Lifschitz, 1991; Pearce, 2006; Pelov et al., 2007; Truszczynski, 2010; Bartholomew et al., 2011; Faber et al., 2011; Ferraris et al., 2011; Shen et al., 2014], only support default negation and they do not allow for epistemic negation.

Epistemic negation and specifications. In fact, the need for epistemic negation was long recognized in ASP by Gelfond in the early 1990s [Gelfond, 1991; 1994] and recently revisited in [Gelfond, 2011; Truszczynski, 2011; Kahl, 2014; Kahl et al., 2015; del Cerro et al., 2015]. In particular, [Gelfond, 1991] showed that formalization of CWA using default and strong negations with rules of the form ∼p(X) ← ¬p(X) as presented in [Gelfond and Lifschitz, 1991], is problematic. He then proposed to address the problem using two epistemic modal operators K and M. Informally, for a formula F , KF expresses that F is true in every answer set, and MF expresses that F is true in some answer set; here MF can be viewed as shorthand for ¬K¬F .

In the sequel, by an object literal we refer to an atom A or its strong negation ∼A; a default negated literal is of the form ¬L, and a modal literal is of the formKL, ¬KL, ML or ¬ML, where L is an object literal.

[Gelfond, 1991] considered disjunctive logic programs with modal literals, called epistemic specifications, which consist of rules of the form

where each L is an object literal and each G is an object literal, a default negated literal, or a modal literal. A normal epistemic specification consists of rules of the above form with m = 1. Given a collection A of interpretations as an assumption, a logic program Π is transformed into a modal reduct ΠA w.r.t. A by first removing all rules with a modal literal G that is not true in A, then removing the remaining modal literals. The assumption A is defined to be a world view of Π if it coincides with the collection of answer sets of ΠA under the semantics of [Gelfond and Lifschitz, 1991].

The problem with recursion through K. More recently, [Gelfond, 2011] addressed the problem that applying the above approach to handle modal literals may produce unintuitive world views due to recursion through K. For example, consider a logic program Π = {p ← Kp}. The rule expresses that for any collection A of answer sets of Π and any I ∈ A, if p is true in all answer sets in A, then p is true in I. This amounts to saying that if p is true in all answer sets, then p is always true (in particular in all answer sets). Obviously, this rule is not informative and does not contribute to constructively building any answer set; thus it can be eliminated from Π, leading to Π = ∅. As a result, Π is expected to have a unique answer set ∅. However, {p} would be an answer set of Π when applying the approach of [Gelfond, 1991]. To illustrate, consider an assumption A = {{p}}, i.e., p is assumed to be true in all interpretations in A. Then, Kp is true in A and we obtain the modal reduct ΠA = {p}. This reduct has a unique answer set {p}, which coincides with the assumption A. Thus A is a world view of Π under [Gelfond, 1991]. Observe that this world view has an epistemic circular justification that can be expressed as

where the arrow ⇐ stands for "is due to." That is, p being true in an interpretation I = {p} of the world view A is due to Kp being treated true in the program transformation for the modal reduct ΠA (via the rule p ← Kp), which in turn is due to p being assumed to be true in all interpretations of A.

In general, a world view A is said to have an epistemic circular justification if some object literal L being true in some interpretation I ∈ A is due to KL (or its equivalent modal literals expressing that L is true in every interpretation J ∈ A) being treated true in the program transformation for the modal reduct of Π w.r.t. A. This means that L being true in some interpretation of A is due to L being assumed to be true in all interpretations of A.

The problem with recursion through M. In addition to the problem of unintended world views due to recursion through K, the approaches of [Gelfond, 2011; 1991] may also have unintended world views due to recursion through M. Consider the logic program Π = {p ← Mp}, which expresses that for any world view A and any I ∈ A, if p is true in some answer set in A, then p is true in I. This amounts to saying that if p is true in some answer set, then p is true in every answer set. Under the approaches of [Gelfond, 2011; 1991] this program has two world views, {{p}} and {∅}. Naturally, the question is whether both are intuitive; ideally, we have only one world view. If, for example, p expresses "something goes wrong," then the program could be viewed as a paraphrase of Murphy's law: "if something can go wrong, it will go wrong," and accordingly, the intuitive world view is {{p}}.

Recent advance. Recent work of [Kahl, 2014; Kahl et al., 2015; del Cerro et al., 2015] suggests that indeed {{p}} should be the only world view of the program Π = {p ← Mp}. In fact, Kahl [2014] and later Kahl et al. [2015] extensively studied the problems of unintended world views due to recursion through K and M and proposed a new program transformation by appealing to nested expressions defined by [Lifschitz et al., 1999]. However, our careful study reveals that applying the approach to some logic programs with recursion through M may also produce unintended world views.

Our contributions. In this paper, we address the above problems of unintended world views and provide a satisfactory solution to epistemic negation as well as epistemic specifications of [Gelfond, 1991]. Our main contributions are briefly summarized as follows:

1. We use modal operator not to directly express epistemic negation and define general logic programs consisting of rules of the form H ← B, where H and B are arbitrary first-order formulas possibly containing epistemic negation. Modal formulas KF and MF are viewed as shorthands for ¬notF and not¬F, respectively, and thus epistemic specifications of [Gelfond, 1991] are a special class of general logic programs.
2. We propose to apply epistemic negation to minimize the knowledge in world views of a general logic program Π, i.e., we apply epistemic negation to arbitrary closed first-order formulas F with respect to a world view and assume not F in Π to be true in the world view whenever possible; we refer to this idea as knowledge minimization with epistemic negation. It is analogous to applying default negation to minimize the knowledge in answer sets, i.e., one applies default negation to arbitrary ground atoms A with respect to an answer set and assumes ¬A to be true in the answer set whenever possible (CWA or minimal models); this is referred to as knowledge minimization with default negation. To this end, we introduce a novel and very simple program transformation based on epistemic negation and present a new definition of world views, which is free of both the problem of unintended world views due to recursion through K and the problem due to M. The proposed approach to evaluating epistemic negation can be used to extend any existing answer set semantics with epistemic negation.
3. We show that deciding whether a propositional program has epistemic answer sets based on the well-known FLP answer set semantics [Faber et al., 2011] is Σp3 -complete and whether a propositional formula is true in every epistemic answer set of some world view is Σp4 -complete in general.

2 Logic Programs with Epistemic Negation

We take a first-order logic language LΣ with equality. By NΣ we denote the set of all ground terms of Σ, and by HΣ the set of all ground atoms. Formulas are constructed from atoms using the connectives ¬, ∧, ∨, ⊃, ⊤, ⊥, ∃, ∀ as usual. Closed formulas contain no free variables. An interpretation I is a subset of HΣ such that for any ground atom A, I satisfies A if A ∈ I, and ¬A if A ̸∈ I. The notion of satisfaction/models of a formula in I is defined as usual. T entails a closed formula F, denoted T |= F, if all models of T are models of F.

Epistemic formulas are formulas extended with epistemic negations of the form notF, where F is a formula.

Definition 1 A general logic program is a finite set of rules of the form H ← B, where H and B are epistemic formulas.

For a rule r : H ← B we refer to B and H as the body and head of r, denoted body(r) and head(r), respectively. A normal epistemic program consists of rules of the form

where n ≥ m ≥ 0 and each Ai is an atom without equality and function symbols except constants. A propositional program Π contains no variables, no function symbols except constants, and no equalities. The Herbrand base of Π is defined as usual. Any subset of the Herbrand base is a Herbrand interpretation of Π.

A closed instance of a rule in Π is the rule with all free variables replaced by constants occurring in Π. The grounding of Π, denoted ground(Π), is the set of all closed instances of all rules in Π. For every epistemic negation notF in ground(Π), we assume that F is a closed formula.

Definition 2 Let A be a set of interpretations and I ∈ A.

1. Let F be a closed formula. Then notF is true in A (or A satisfies notF) if F is false in some J ∈ A, and false, otherwise. I satisfies notF if notF is true in A.
2. I satisfies a closed epistemic formula E if I satisfies E as in first-order logic except that the satisfaction of epistemic negations in E is determined by (1).
3. I satisfies a closed instance r of a rule if I satisfies head(r) whenever I satisfies body(r).
4. A is a collection of models of a logic program Π if every I ∈ A satisfies all rules in ground(Π). A model I ∈ A is minimal if there is no model J ∈ A with J ⊂ I.

Proposition 1 Let Π be a logic program and Π¬ be Π with all epistemic negations notF replaced by default negations ¬F. For any interpretation I, A = {I} is a collection of models of Π iff I is a model of Π¬.

The following theorem lays a theoretical basis for our novel program transformation introduced in the next section.

Theorem 1 Let Π be a logic program such that for every notF in ground(Π) F is true in every model of Π. Let Π¬ be Π with every epistemic negation not F replaced by default negation ¬F . Then Π and Π¬ have the same models.

3 Epistemic ProgramTransformation

In ASP, a common technique for defining semantics is to transform a logic program into a reduct that is free of negation or modal operators. For a normal logic program Π, the seminal GL-reduct ΠI w.r.t. a given interpretation I is obtained from ground(Π) by removing first all rules whose bodies contain a default negation ¬A with A ∈ I, and then all ¬A from the remaining rules [Gelfond and Lifschitz, 1988]. Similarly, when Π is a logic program extended with modal operators K and M, transformations w.r.t. a given set A of interpretations are defined in [Gelfond, 1991; 2011; Truszczynski, 2011; Kahl, 2014] by eliminating/replacing all modal literals in ground(Π) in terms of whether or not they are true in A. Note that these existing definitions of program transformations are based on an assumption, which is either a given interpretation or a given set of interpretations, and default negations or modal literals in a logic program are evaluated against the assumption.

In this paper we aim to apply epistemic negation to minimize the knowledge in a world view of a logic program Π by assuming every epistemic negation notF in Π to be true in the world view whenever possible. To this end, we define program transformations in an alternative way, which is based on an assumption that is a given set of epistemic negations, instead of a given set of interpretations.

Definition 3 For a logic programΠ, let Ep(Π) denote the set of all epistemic negations notF in ground(Π). A guess of epistemic negations for Π is a subset Φ of Ep(Π).

Intuitively for every notF ∈ Φ, it is guessed that F couldn't be proved true, and for every notF ∈ Ep(Π) \ Φ, it is guessed that F would be proved true. Recall that an epistemic negation notF expresses that there is no evidence proving that F is true, where F is proved true if it is true in every answer set of some world view.

Once a guess Φ is given, we can transform program Π by replacing all epistemic negations in terms of Φ. There would be different replacements for epistemic negations, which would lead to different program transformations. The simplest yet unreflected one is to replace notF with ⊤ if notF ∈ Φ, andwith⊥, otherwise. It turns out that this transformation incurs both the problem of unintended world views due to recursion through K and the problem due to recursion through M, analogously to the cases in [Gelfond, 1991].

The key idea of our program transformation is that we first assume that the guess on all notF ∈ Φ is correct and thus replace them with ⊤. Then, for every notF ∈ Ep(Π) \ Φ, instead of replacing it with ⊥, we replace it with ¬F. The intuition and rationale for the latter replacement is: if Φ is a correct guess, once all epistemic negations notF ∈ Φ in ground(Π) are replaced with ⊤, which leads to a new programΠ⊤, for every notF in Π⊤, the formula F is supposed to be true in every answer set of Π⊤. Let ΠΦ be Π⊤ with each notF replaced by ¬F; then by Theorem 1, where model is analogously replaced by answer set, we expect that Π⊤ and ΠΦ have the same answer sets. This rational justification of the replacements for epistemic negations leads to the following novel program transformation.

Definition 4 Let Φ ⊆ Ep(Π) be a guess of epistemic negations for a logic program Π. The epistemic reduct ΠΦ of Π w.r.t. Φ is obtained from ground(Π) by replacing every not F ∈ Φ with ⊤, and every not F ∈ Ep(Π) \ Φ with ¬F . Π is consistent w.r.t. Φ if ΠΦ is consistent.

In the Introduction we mentioned that a world view A is said to have an epistemic circular justification if some object literal L being true in some interpretation I ∈ A is due to KL being treated true in the program transformation w.r.t. A. In our language, KL is shorthand for ¬notL, and in our program transformation w.r.t. a guess Φ, ¬notL will be either treated ¬⊤ (when notL ∈ Φ), which evaluates to false, or treated ¬¬L (when not L ∈ Ep(Π) \ Φ), which evaluates to L. This means that our program transformation would never incur epistemic circular justifications and thus guarantees that world views based on the epistemic reducts will be free of the problem with recursion through K.

4 AGeneral Epistemic Answer Set Semantics

Now that all epistemic negations have been removed from a logic program Π, leading to an epistemic reduct ΠΦ w.r.t. a guess Φ, we can apply any answer set semantics for logic programs without epistemic negation to compute all answer sets A of ΠΦ. For A to be a world view, it must agree with the guess Φ, i.e., every not F ∈ Φ is true and every not F ∈ Ep(Π)\Φ is false in A; and it should also satisfy the property of knowledge minimization with epistemic negation.

Definition 5 A world view A of a logic program Π has the property of knowledge minimization with epistemic negation if A satisfies a maximal set Φ of epistemic negations in Ep(Π) (i.e., no other world view satisfies Φ′ ⊃ Φ in Ep(Π)).

In this section, we present a general framework for defining epistemic answer set semantics, thus called a general epistemic answer set semantics, which is applicable to extend any existing answer set semantics with epistemic negation.

Definition 6 Let Φ be a guess such that ΠΦ is a consistent epistemic reduct. Let X be an answer set semantics for logic programs without epistemic negation. The collection A of all answer sets of ΠΦ under X is a candidate world view of Π w.r.t. Φ if (a) A is nonempty, (b) every notF ∈ Φ is true in A, and (c) every not F ∈ Ep(Π)\Φ is false in A. Candidate world view A w.r.t. Φ is a world view if Φ is maximal (i.e., there is no candidate world view w.r.t. a guess Φ′ ⊃ Φ).

The condition "Φ is maximal" implies that world views under the general epistemic semantics have the property of knowledge minimization with epistemic negation.

Definition 7 Let F be a closed formula. We say F is true in Π under the general epistemic semantics if Π has a world view A such that F is true in every answer set in A.

Now we are ready to introduce a formal definition of the problem of unintended world views with recursion through M, which was informally described in the Introduction.

Definition 8 An epistemic answer set semantics is said to have the problem of unintended world views due to recursion through M if its world views do not satisfy the property of knowledge minimization with epistemic negation.

Evidently, our general epistemic answer set semantics is free of the problem with recursion through M.

Remark 1 Default negation and epistemic negation are used to minimize the knowledge at the answer set level and the world view level, respectively. At the answer set level, for any ground atom A we assume its default negation ¬A to be true (or A to be false) in every answer set whenever possible (knowledge minimization with default negation); analogously at the world view level, for any epistemic negation notF occurring in a logic program, where F is a closed formula, we assume not F to be true (or F to be false) in every world view whenever possible (knowledge minimization with epistemic negation). Since epistemic negation is at a meta level, the minimization with epistemic negation has higher priority and is done before the minimization with default negation.

Note that if one intends to apply epistemic negation to a formula F by assuming not F to be true in every world view whenever possible, one must explicitly express the epistemic negation notF in a logic program. Thus the four programs Π1 = {p ∨ q }, Π2 = {p ∨ q, p ← not q }, Π3 = {p ∨ q, q ← not p}, and Π4 = {p ∨ q, p ← not q, q ← not p} are entirely different and have different world views: Π1 has a unique world view {{p}{q}}, Π2 has {{p}}, Π3 has {{q}}, and Π4 has two world views {{p}} and {{q}}.

In contrast, for any ground atom A, its default negation ¬A is implicitly assumed to be true in every answer set whenever possible, whether or not ¬A is present in a logic program. Thus the four programs Π1 = {p∨q}, Π2 = {p∨q, p ← ¬q}, Π3 ={p∨q, q ←¬p}, andΠ4 ={p ∨ q, p ←¬q, q ←¬p} have the same answer sets {p} and {q} under the standard answer set semantics of [Gelfond and Lifschitz, 1991].

5 Computational Complexity

The general framework of Definition 6 is applicable to extend any existing answer set semantics with epistemic negation, such as those in [Pearce, 2006; Pelov et al., 2007; Truszczynski, 2010; Bartholomew et al., 2011; Faber et al., 2011; Ferraris et al., 2011; Shen et al., 2014]. As a simple showcase we extend the FLP semantics of [Faber et al., 2011] (which for not -free rules of the form (1) amounts to the standard answer set semantics) with epistemic negation.

Definition 9 Let Π be a logic program without epistemic negation and I an interpretation. The FLP-reduct of Π w.r.t. I is fΠI = {r ∈ ground(Π) | I satisfies body(r)}, and I is an FLP answer set of Π if I is a minimal model of fΠI .

By replacing X with FLP semantics in Definition 6, we obtain an epistemic FLP semantics (EFLP semantics).

Example 1 Under EFLP semantics, we can directly formulate CWA using closed world rules of the form ¬p ← not p, which expresses that when failing to prove p to be true, we assert ¬p. Moreover, we can also state its opposite using rules p ← not ¬p, which expresses that when we fail to prove ¬p true, we assert p. We can further combine them, leading us to the interesting program Π = {¬p ←not p, p ←not¬p}. This program has two world views: A1 = {∅} w.r.t. the guess Φ1 = {not p} and A2 = {{p}} w.r.t. Φ2 = {not ¬p}. This conforms to our intuition that either ¬p or p can be concluded from Π, depending on whether we choose to apply CWA on p (rule r1) or on ¬p (rule r2).

Theorem 2 Deciding whether a propositional program Π has some world view, i.e., EFLP answer set existence, is Σp3 - complete, and deciding whether a propositional formula F is true in a propositional program Π under EFLP semantics is Σp4 -complete.

Acknowledgments

This work is supported in part by China National 973 program 2014CB340301 and NSFC grant 61379043, and the Austrian Science Fund (FWF) via the projects P24090 and P27730.