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.)