Choice Rules and the Belief-Based View of ASP, Part 2 ========= Date: 29 Oct 2010 From: Vladimir Lifschitz To: Pedro Cabalar I understand to some degree the objection to lparse-style choice rules based on the idea that a rule is a constraint on a set of beliefs of a rational agent (in Michael's words). But I have doubts about your assertion that > choice rules are quite difficult to explain to students, especially if > you have just introduced the traditional idea of reduct, which is very > intuitive and simple. Here is a way around this difficulty. Consider rules of the following form: the head is an atom; each member of the body is an atom possibly prefixed by one *or two* negations. The expression not not A in the body of the rule has the same truth value as A, but the definition of the reduct w.r.t. X treats it in the same as other expressions beginning with "not": a rule containing that expression is dropped if A is not in X. Once simple "1988-style" programs are generalized in this way, we can say that {p} <- Body is shorthand for p <- Body, not not p. I have never used this approach to choice rule in teaching, but I plan to do it next semester. I hope that students familiar with traditional reducts will find this easy to swallow. What do you think? Strong negation can be easily added to this, of course. A question to Michael: how is this generalization of the reduct philosophically different from the 1988 approach, without double negations in the body? ========= Date: 30 Oct 2010 From: Pedro Cabalar To: Vladimir Lifschitz I probably didn't explain myself: that's exactly what I was proposing! In my examples I was using default negations in the head instead, but as you know, this is strongly equivalent to move them as double negations in the body, yielding the same effect on the reduct. Yes, I agree that double negation provides a very natural way of describing choice rules like {p} :- Body You nicely capture this together with other general counting constructs in your joint paper with Lee and Palla "A reductive semantics for counting and choice in answer set programming " (AAAI'08) translating them to a first order language. Still, I have one question: how would you explain the semantics of a constraint like 1 {p(X):q(X)} 1 :- body if you just considered double negation as the only allowed syntactic extension? (say, for instance, if you had DLV plus double negations) I ask this because it probably constitutes one of the most frequent uses of cardinality constraints and I repeatedly use it in class examples. ========= Date: 29 Oct 2010 From: Michael Gelfond To: Vladimir Lifschitz To answer your question: > A question to Michael: how is this generalization of the reduct > philosophically different from the 1988 approach, without double > negations in the body? I do not think I ever made any philosophical claims! I am looking at ASP as a practical KR language. The ability to explain the semantics of such a language as simply as possible is one of the main requirements. (Since I do not want the language to have CWA built in its semantics I prefer to talk about our 1990 paper.) I explain answer sets as sets of literals which satisfy the rules of the program and the rationality principle. Formal definition captures this intuition. Anti-chain property is a simple intuitive consequence of rationality principle -- since I am told to believe as little as possible I chose {p} over {p,q}. (Of course {p,-q} and {p,q} are not comparable and hence both can be o.k.). If I follow this approach then to allow double NAF in the body I have to explain when a set S of literals satisfies not not p. "not p" means "p is not in S". So what is not (p is not in S)? The simplest explanation I see is (p is in S). You have a different interpretation which I cannot clearly articulate. Hence I cannot clearly explain what it means for S to satisfy the rule > p <- Body, not not p. The problem comes before the reduct is even mentioned. Since I find this difficult to swallow I have no reason to believe that my students will. I also have a more general problem with this discussion. I am not convinced that such extensions of 1990 language are important from the standpoint of KR. I am not specifically interested in lparse or other such languages. The particular decisions made there are often incidental. The role played by choice rule can (and in case of DLV is) successfully played by other constructs. (Pedro is of course right saying that my subset suggestion is different from one implemented in lparse. But is it in any way less suitable for KR?) It is true that lparse is not a sorted language and does not check sorts. It is also true that a program RSig -- a version of lparse with sorts -- was designed and implemented by Marcello long time ago. It was much easier to use than lparse for larger programs with modules written by different people. It can be found in Software on our KR lab page. I understand the theoretical desire to generalize. It is useful and should be guided by existing systems. But one possible outcome of such generalization can be discovery of better constructs, and building of better systems. ========= Date: 30 Oct 2010 From: Pedro Cabalar To: Michael Gelfond > If I follow this approach then to allow double NAF in the body I > have to explain when a set S of literals satisfies > > not not p. > > "not p" means "p is not in S". > > So what is > > not (p is not in S)? > > The simplest explanation I see is (p is in S). I think that a possible reading is: not F = assume falsity of (F) Then not not F = assume falsity of (assume falsity of (F)) = assume truth of F For me, this is quite different from saying that F is true. > You have a different interpretation which I cannot clearly articulate. > Hence I cannot clearly explain what it means for S to satisfy > the rule > >> p <- Body, not not p. > Using the reading above, I would say it corresponds to a normal default rule Body : p ----------- p That is: make some assumption M for a stable model. If Body holds, and p is being assumed in M, then p must also hold. Would you find this explanation more reasonable? ========= Date: 31 Oct 2010 From: Michael Gelfond To: Pedro Cabalar You write: > I think that a possible reading is: > > not F = assume falsity of (F) How do you read -F where - is classical negation? (My reading of it seems identical to your reading of not F) > Then > > not not F = assume falsity of (assume falsity of (F)) = assume truth > of F > > For me, this is quite different from saying that F is true. I agree that assuming truth of F (or believing in truth of F) is different from truth of F. That is why I normally do not talk about truth of F in ASP (except as a shorthand) Consider the rule: p :- not q Since the conclusion, p, is defeasible all we can conclude is that p is assumed (believed) to be true. We cannot conclude that it IS true. You further write that > using the reading above, I would say that p <- Body, not not p > corresponds to a normal default rule > > Body : p > ----------- > p > > That is: make some assumption M for a stable model. If Body holds, =20 > and p is being assumed in M, then p must also hold. If I am not mistaken, this default rule in LP looks like p :- Body, not -p. This is of course a typical closed world assumption which does not require NOT NOT. not -p is satisfied by a set S of literals if -p is not in S and hence the above rule causes no problem. Am I missing something? (BTW literals are of the form p, -p. NOT p is not a literal -- maybe this causes some confusion). p.s. I understand that you can express choice rules using disjunction p ; not p. But if you accept the rationality principle then { } (empty) is the only model one may expect. One is not forced to believe p and therefore he does not. Of course one is not required to interpret ASP as formalization of beliefs of an agent adhering to the rationality principle but it would be nice to hear some alternative. ========= Date: 31 Oct 2010 From: Pedro Cabalar To: Michael Gelfond > How do you read -F where - is classical negation? > (My reading of it seems identical to your reading of not F) Ok. Sorry, when I talked about true/false I was not considering explicit negation. Once we allow both p and -p we switch to a 3-valued situation where: p = I know p true -p = I know p false none of the two = p is unknown Accordingly, the reading when using explicit negation becomes: not F = assume not known (F) not not F = assume not known (assume not known (F)) = assume known F For instance, not not -p = assume known -p which again, I understand as something different from "plain" (-p). > Consider the rule: > > p :- not q > > Since the conclusion, p, is defeasible all we can conclude is that > p is assumed (believed) to be true. > We cannot conclude that it IS true. Sorry, we obviously use a different terminology for "truth" and "assumption". Your definition of "truth" is interesting, let me see if I understand it. Given the program p :- not q r would you say that p is just "believed true" whereas r IS "true"? Then, do you understand "truth" as anything that is not defeasible? Studying this distinction could be an interesting problem. >> Body : p >> ----------- >> p >> >> That is: make some assumption M for a stable model. If Body holds, >> and p is being assumed in M, then p must also hold. > > > If I am not mistaken, this default rule in LP looks like > > p :- Body, not -p. > ... Yes, forget the example, it was wrong. The above default rule is NOT equivalent to using (not not p) in logic programming. When Body holds and nothing else is known, the default rule will just add p but not lead to a second extension with p unknown. Furthermore one cannot build the "not not" effect with standard Default Logic, which is always rational. Bad example. > I understand that you can express choice rules using disjunction > > p ; not p. > > But if you accept the rationality principle then { } (empty) is the > only model one may expect. One is not forced to believe p > and therefore he does not. Ok. Let me try another (let's hope better) example. Suppose I have some program that acts in different ways depending on whether we include: (1) a fact asserting I know p; (2) a fact asserting I know - p; or (3) no fact at all about p. Suppose also that I'm interested in checking what conclusions (i.e. answer sets) I would get when the fact -p is not included, i.e. when we are in cases (1) or (3). This how I would solve it in DLV for instance. As I want to add p in one case, and leave it unknown in the other, I would generate the two alternatives as follows p :- not aux. aux :- not p. where aux is a new fresh auxiliary predicate (not mentioned in the rest of the program). aux would be disregarded (hidden) when looking at the obtained conclusions. I claim that this is exactly the same (i.e. is strongly equivalent modulo the original signature) to p :- not not p. ========= Date: 1 Nov 2010 From: Marcello Balduccini To: TAG > It is true that lparse is not a sorted language and does not check sorts. > It is also true that a program RSig -- a version of lparse with sorts > -- was designed and implemented by Marcello long time ago. It was much > easier to use than lparse for larger programs with modules written by > different people. It can be found in Software on our KR lab page. Just a quick note on rsig. While the original rsig was built upon lparse and only worked with it, a while ago I have written an implementation that aims at being grounder-independent. The software is called dlv_rsig (as it was originally meant to allow using signature declarations in dlv programs, but I routinely use it with other grounders, e.g. gringo), works as a pre-parser, and uses a simplified syntax for signature declarations. A simple example, p1, is: p(1). p(2). p(3). p(4). #sig a(p), b(p). a(X) :- not b(X). b(X) :- not a(X). The command "dlv_rsig p1" will produce the output program: p(1). p(2). p(3). p(4). a(X) :- p(X), not b(X). b(X) :- p(X), not a(X). To compute the answer sets of p1, one can use "dlv_rsig p1 | gringo | clasp 0". Contrary to the original specification of the rsig language (which can be found in my paper -- see the original RSig web page on the KRLab web site), the simplified specification used here does not distinguish between predicates and functions. As I mentioned above, dlv_rsig attempts at being grounder-independent. This was accomplished by developing a grammar definition that encompasses the various language dialects. I expect that people using it may find special cases that I have not considered, so feedback is welcome. If you would like to use it, you can download it from http://marcy.cjb.net/ezcsp/dlv_rsig-1.8.0.tgz. (In case the name dlv_rsig rings a bell -- dlv_rsig is used and required by my ezcsp. As a matter of fact, signature declarations can be used in ezcsp.) ========= Date: 1 Nov 2010 From: Michael Gelfond To: Pedro Cabalar You write that p :- not aux. aux :- not p. is strongly equivalent to p :- not not p I understand that. So we agree agree here. You also write: > Sorry, we obviously use a different terminology for "truth" and > "assumption". Your definition of "truth" is interesting, let me see > if I understand it. Given the program > > p :- not q > r > > would you say that p is just "believed true" whereas r IS "true"? > Then, do you understand "truth" as anything that is not defeasible? > > Studying this distinction could be an interesting problem. You basically right. But the main point is that from my standpoint ASP says nothing about truth -- only about beliefs. Hence I do not need to make the distinction between truth and assumption of truth. I agree that studying the distinction between belief and truth (or as I put it between belief and knowledge, understood as the true belief) is a very interesting problem. If p(X) is a property of an outside (say physical) world then one possible approach is as follows: An agent associated with program P knows Q if Q is a consequence of any program P + U where U is an update of the program. I suggested something like this in one of our discussions with Vladimir. He and his students quickly noticed that if updates consist of arbitrary consistent collections of literals then it is equivalent to derivability of Q from P in classical logic (with arrow turned into implication and NOT into classical negation). Different types of updates can also be studied. The real difficulty occur when the truth of Q is not fully determined by the outside world but instead depends on the program. Suppose the program contains a list of students defined as member(mike,l). member(john,l). -member(mary,l). and a rule no-info(X) :- student(X), not member(X,l), not -member(X,l). it seems that, assuming that Bob is a student, no-info(bob) is a true statement. Bob is simply not in the list. But of course it is defeasible. I do not know how to capture this kind of truth, but I think it is important and interesting to do so. ========= Date: 2 Nov 2010 From: Vladimir Lifschitz To: Pedro Cabalar In one of your messages to TAG, you asked, > how would you explain the semantics of a constraint like > > 1 {p(X):q(X)} 1 :- body > > if you just considered double negation as the only allowed syntactic > extension? If q is defined, say, by the facts q(a), q(b), q(c), then I would say that your example is shorthand for a :- body, not not a. b :- body, not not b. c :- body, not not c. :- body, not a, not b, not c. :- body, a, b. :- body, a, c. :- body, b, c. This can be made more compact using nested expressions, of course. By the way, a future version of gringo, as I understand, will allow us to rewrite your example 1 {p(X):q(X)} 1 :- body as a combination of a choice rule and a dlv-style aggregate: {p(X)} :- body, q(X). :- body, not #count{X:p(X),q(X)}=1. (Or something similar.) This formulation is less concise, but it avoids using conditional literals--a construct whose declarative semantics seems somewhat problematic. ========= Date: 8 Nov 2010 From: Marc Denecker To: TAG I have a strong sense that this discussion revolves around the following issue: there are 2 different methodologies in ASP; they differ in how an answer set relates to the (informal) problem domain. In one methodology, an answer set is a formal representation of a potential state of belief of some (relevant) agent; the agent could be the answer set programmer, or the knowledge base underlying an answer set program; the answer set is the set of believed literals in a possible state of belief of the agent. This is the methodology of the original papers of Michael and Vladimir and is still followed systematically by Michael (less by Vladimir I think). I call it the ASP-belief methodology. In a second methodology, an answer set is a formal representation of a possible state of affairs of the objective world, just like a structure(=interpretation) in classical logic. In this view, an answer set is really a Herbrand interpretation in which a missing atom means falsity of that atom in the world state. There is no reflecting epistemic agent involved. E.g., in the ASP encoding of a colorability problem, an answer set contains a correct coloring and this does not really represent a belief set of some relevant reflecting agent; it represents a possible world. I call this the ASP-world methodology. The impact on knowledge representation of using one or the other methodology is overwhelming. To illustrate this, consider the following example, a simplification of an example of Michael and Vladimir's 91 paper. Suppose that we want to represent an open database about minorities in ASP. Bob is a minority, Dave is not, and nothing is known about Ann. In the ASP-belief methodology, it will be represented as follows: (1) Minority(Bob). -Minority(Dave). % Nothing known about Ann Absence of Minority literals about Ann means that her minority status is unknown. Now, assume that we obtain complete knowledge and that Bob turns out to be the only minority person. We can represent this compactly by (2) Minority(Bob). % -Minority(Dave). This rule is now subsumed by the CWA rule. (3) -Minority(x) <- not Minority(x). % CWA rule This is the methodology followed in the 91 paper. At present, it is more common to model these two situations in a different style. The complete database would be modeled by: (4) Minority(Bob). % this entails that Ann and Dave are not minorities and the incomplete database by: (5) { Minority(x) } <- Person(x). %Choice rule (6) <- Minority(Dave). (7) <- not Minority(Bob). (8*) Person(..) <- ... This is the ASP-world methodology. What we see here is: that in the ASP-belief methodology, there is no CWA unless explicitly added. In the ASP-world methodology, the opposite holds: there is CWA, unless explicitly overwritten for a specific predicate by a choice rule. CWA is implicit in ASP-world, and to represent incomplete knowledge it must be overwritten explicitly, by rules that open up a predicate or a set of atoms. E.g., the choice rule (5). There are well-known alternative ways of opening up a predicate --relaxing the CWA on a predicate. E.g., (5') Minority(x) <- Person(x), not P(x) P(x) <- Person(x), not Minority(x) or (5") Minority(x) v P(x) <- Person(x). where P is some new predicate symbol. Now assume that we want somebody to be interviewed if it is unknown whether he or she is a minority. In the ASP-belief methodology, this is represented (confer the 91 paper): (9) Interview(x) <- not Minority(x) , not -Minority(x). Here the epistemic nature of negation as failure is exploited. This rule gives the intended solution to Interview in the two situations: {} in the complete database ({1+9}), and {Interview(Ann)} in the incomplete database ({2+3+9}. In the ASP-world methodology, this rule does not define Interview correctly. One can easily see that e.g., in the open database ({5+6+7+8*+9}), we will get answer sets where Interview(Ann) is true and others where it is false, and in all Interview(Dave) will be true. But we can represent Interview if we use the strong introspection operator introduced by Michael in 92 (which is not implemented in current ASP systems). (10) Interview(x) <- not K Minority(x) , not K not Minority(x). Now, {5+6+7+8*+10} would have a number of answer sets, but they all would be identical with respect to Interview: {Interview(Ann)}. In summary, we see really considerable differences in the way the same knowledge is to be encoded in the two methodologies. In fact, ASP behaves as a very different language depending on which methodology is used. It seems to me that the choice rule does not fit at all in the ASP-belief methodology. On the other hand, it fits well in the ASP-world methodology. We have written two papers about this issue: [1] Answer Set Programming's Contributions to Classical Logic - An analysis of ASP methodology, Michaels anniversary symposium, 2010, http://people.cs.kuleuven.be/~marc.denecker/ctc.pdf In this paper, we show that each sort of knowledge has a different encoding in both methodologies, we discuss the strong links between ASP-world and knowledge representation in FO(.), and we develop an extension of FO in which the advantages of ASP-belief and ASP-world are combined. [2] What's in a model? Epistemological analysis of logic programming, KR 2004. http://www.cs.kuleuven.ac.be/cgi-bin-dtai/publ_info.pl?id=41086 This paper is a study of the impact of modifying the relation of a model or an answer set with respect to the real world, on the informal semantics (the intuitive meaning) and the methodology. This is investigated not only in logic programming and answer set programming, but also in classical logic. ========= Date: 10 Nov 2010 From: Pedro Cabalar To: Michael Gelfond > An agent associated with program P knows Q if Q is a consequence of any > program P + U where U is an update of the program. Let me see if I understand: you mean (P knows Q) = for all U, M: if M is in SMs(P+U) then M |= Q where SMs is the set of stable models and |= is classical satisfaction. Is this right? > I suggested something like this in one of our discussions with Vladimir. > He and his students quickly noticed that if updates consist of arbitrary > consistent collections of literal then it is equivalent to derivability of > Q from P in classical logical (with arrow turned into implication and NOT > into classical negation). Different types of updates can also be studied. As far as I can see, if the definition I proposed above was what you meant (P knows Q) iff (P |= Q) i.e. Q is a classical consequence of P for any arbitrary formula Q. I can't see the need of restricting Q to collections of literals. > member(mike,l). > member(john,l). > -member(mary,l). > no-info(X) :- > student(X), > not member(X,l), > not -member(X,l). > > it seems that, assuming that Bob is a student, > no-info(bob) > is a true statement. > Let me know if this makes sense. > If it does not I'll elaborate further. I'm not sure I understand. I guess that you mean that in this case "not" is working just to check the absence of a literal and not as a real default related to the agent's belief. It's as if you were using two different types of negation. Does this make sense? ========= Date: 11 Nov 2010 From: Pedro Cabalar To: Vladimir Lifschitz > If q is defined, say, by the facts q(a), q(b), q(c), then I would say > that your example is shorthand for > > a :- body, not not a. > b :- body, not not b. > c :- body, not not c. > :- body, not a, not b, not c. > :- body, a, b. > :- body, a, c. > :- body, b, c. > > This can be made more compact using nested expressions, of course. Ok. I understand: I guess you meant p(a), p(b), p(c) instead of a,b,c. So, if we look at the program back in the non-ground level, the expression 1 {p(X): q(X)} 1 :- body. Is a shorthand for % choice {p(X)} :- body, q(X). % at least one somep :- body, q(X), p(X). :- body, not somep. % at most one :- body, q(X), p(X), q(Y), p(Y), X!=Y. Is this correct? The introduction of existential quantifiers could further simplify the "at least one" part, removing the auxiliary predicate "somep" % at least one :- body, not #exists X ( q(X), p(X) ). I've found existential quantifiers very useful for avoiding auxiliary predicates in many situations. Besides, they can be easily implemented without requiring a substantial change in the usual syntax of say, lparse or DLV. Some examples and a straightforward translation can be found in: P. Cabalar, "Existential Quantifiers in the Rule Body", WLP'09, Potsdam, Germany, 2009. http://www.dc.fi.udc.es/~cabalar/eqrb.pdf > By the way, a future version of gringo, as I understand, will allow > us to > rewrite your example > > 1 {p(X):q(X)} 1 :- body > > as a combination of a choice rule and a dlv-style aggregate: > > {p(X)} :- body, q(X). > :- body, not #count{X:p(X),q(X)}=1. > > (Or something similar.) This formulation is less concise, but it > avoids > using conditional literals--a construct whose declarative semantics > seems > somewhat problematic. Question: can we simulate an existential quantifier with #count? For instance, it occurs to me that :- body, not #exists X (q(X), p(X)). could be written as :- body, not #count{X: p(X), q(X)}>=1. ========= Date: 11 Nov 2010 From: Vladimir Lifschitz To: Pedro Cabalar I agree with your correction and with all your other points: extending my proposal to programs with variables and the use of existential quantifiers to eliminate auxiliary predicates. Thank you for letting me know about your WLP'09 paper, I was not aware of it. ========= Date: 16 Nov 2010 From: Vladimir Lifschitz To: Marc Denecker I am thinking about your distinction between two knowledge representation methodologies in ASP: > In one methodology, an answer set is a formal representation of a > potential state of belief of some (relevant) agent; the agent could be > the answer set programmer, or the knowledge base underlying an answer > set program; the answer set is the set of believed literals in a > possible state of belief of the agent. > I call it the ASP-belief methodology. > In a second methodology, an answer set is a formal representation of a > possible state of affairs of the objective world, just like a > structure(=interpretation) in classical logic. In this view, an answer > set is really a Herbrand interpretation in which a missing atom means > falsity of that atom in the world state. There is no reflecting > epistemic agent involved. > I call this the ASP-world methodology. I have two suggestions/questions. First: in the course of this discussion, we talked about USA-Advisor, which was created by Michael and his students. That program widely uses classical negation and is clearly based on the "ASP-belief methodology." On the other hand, several predicates in USA-Advisor rules (link/3, jet_of/2, direction/2, tank_of/2 and others) never occur with classical negation, and this is interpreted in the spirit of the closed world assumption--not as incompleteness of information. It occurs to me now that we can think of USA-Advisor as a combination of two kinds of ASP: it uses both "belief predicates" and "world predicates." This is similar to the distinction between "symmetric" and "asymmetric" predicates that I proposed in one of my messages. Would you agree with this interpretation? Second, about the use of strong introspection in the rule > (10) Interview(x) <- not K Minority(x) , not K not Minority(x) that you proposed as a possible replacement for > (9) Interview(x) <- not Minority(x) , not -Minority(x). Do you think this may be an instance of a general method that can allow us to eliminate classical negation in favor of strong introspection, under some conditions? There may be an interesting general theorem hidden here! ========= Date: 18 Nov 2010 From: Marc Denecker To: Vladimir Lifschitz > > Second, about the use of strong introspection in the rule > > > > >> >> (10) Interview(x) <- not K Minority(x) , not K not Minority(x) >> >> > > > > that you proposed as a possible replacement for > > > > >> >> (9) Interview(x) <- not Minority(x) , not -Minority(x). >> >> > > > > Do you think this may be an instance of a general method that can allow us > > to eliminate classical negation in favor of strong introspection, under > > some conditions? There may be an interesting general theorem hidden here! > > Do you really mean "classical negation", or is this a typo? I am asking this because your question surprises me, for the following reason. Classical negation is an objective boolean connective. As in "I have NOT eaten soup today (*)". Classical negation is not a connective to query the knowledge (or the absence of knowledge) of some knowledge base or epistemic agent. On the other hand, the strong introspection operator per definition serves to query the knowledge of a knowledge base/epistemic agent. As in "If I KNOW THAT my team has won, I'll drink champagne (**)". Or as in "If I DO NOT KNOW THAT my team has won, I'll watch the news on TV (***)". So there is striking semantical mismatch between classical negation and this operator. Therefore, I think that any attempt to replace classical negation by the strong introspection operator is bound to fail. Also, in the ASP-belief program in my original message on TAG, the rule (9) Interview(x) <- not Minority(x) , not -Minority(x). represents the informal rule: (9') "x will be interviewed if THE KNOWLEDGE BASE DOES NOT KNOW THAT x is a minority and THE KNOWLEDGE BASE DOES NOT KNOW THAT x is NOT a minority." In (9), the informal meaning of the classical negation symbol "-" is standard negation, as in the "soup" sentence (*). NAF is used in (9) as an epistemic operator, to query the knowledge of the knowledge base. As I showed (along the lines of earlier examples in Michaels original paper on strong introspection), this rule only works in the ASP-belief methodology, not in ASP-world. To represent the informal rule (9') in the ASP-world methodology, we need the strong introspection operator K. Hence, if there is a match, it is between negation as failure and the strong introspection operator: in ASP-world programs, we need the strong introspection operator K to express what is expressed through NAF in ASP-belief applications. PS. I might have confused a few people by encoding (9') in ASP-world as: (10) Interview(x) <- not K Minority(x) , not K not Minority(x) with three occurrences of NAF, of which the third one replaces the original classical negation. Recall that the rest of the ASP-world program is (5) { Minority(x) } <- Person(x). %Choice rule (6) <- Minority(Dave). (7) <- not Minority(Bob). (8*) Person(Bob). Person(Dave). ... The use of NAF in rule (10) instead of classical negation requires some explanation. As we have seen, NAF in this ASP-world program is NOT the epistemic operator of the knowledge base represented by this program. So, what is it then? We get a hint by looking in the semantics. In ASP-world, an answer set represents a possible world, hence it is just like an interpretation of a classical logic theory. In an answer set M, a NAF literal "not p" is satisfied iff p is absent from M. This is exactly how classical negation is defined. This suggests loud and clear than in ASP-world programs, NAF is really classical negation. That explains why e.g., (7) <- not Minority(Bob). really can be used to encode (7') It is not the case that Bob is NOT a minority. The "not" in this rule, and also the constraint operator ":-" are used here to represent standard (classical) negation. In summary, I have argued that in ASP-world, NAF is really classical negation. Therefore, the informal rule (9') is represented correctly by (10). --------- (See Part 3 for the continuation of this discussion.)