Problem 51

Date: Thu, 20 Apr 2000
From: Vladimir Lifschitz
To: TAG

I'd like to offer you, as a little exercise, one of the problems that we
are discussing these days in my answer set programming class.  We call it
"Problem 51," because this is the number that this question happened to
get in my list of homework problems.

===

PROBLEM 51. Let A be any logic program containing the rules

p <- q,
p <- not q.

Let A' be the program obtained from A by replacing these two rules with

p.

Then A' has the same answer sets as A.

True or false?

===

This is not a terribly difficult question, but I must tell you that, when
I started thinking about it, I couldn't decide for some time what to look
for -- a proof or a counterexample.  What does your intuition tell you?

===========

Date: Fri, 21 Apr 2000
From: Michael Gelfond
To: Vladimir Lifschitz

Tthanks, this is a nice problem.
You should send us more of these.

(To TAG members: If you do not know the answer yet you may think
more before reading any further.)

My intuition tells me that the programs are not equivalent.
Let me try to explain why (the explanation naturally ends by a proof).

The problem is related to a very important property of programs
which I call "strong equivalence" but which
is also known under other names (I do not remember them though).

P1 is strongly equivalent to P2 if for any
program T, T + P1 is equivalent (has the same answer 
sets) to T + P2. 

Programs (especially those with "not") are rarely 
strongly equivalent (even though Pearce and Herre
have something to say about when they are).

In your first program  "p" is only defeasibly true
while in the second it is "really" true which 
suggest that they are not strongly equivalent.

Of course the difficulty is caused by the fact
that "p" in the first program seems to be "really"
true. One is tempted to use reasoning by cases
to establish this. The argument does not work though
since it ignores the possibility for a defeasible 
program to be inconsistent while its "classical" counterpart
is not.

This observation immediately leads to the proof -  make p equivalent to q,

i.s. consider two programs:

q <- p
p <- q
p :- not q

and

q <-- p
p.

First has no answer sets while the second is consistent.

Even though strong equivalence is rare some weaker
but also important "equivalences" are more frequent.

One can study equivalences of programs under various types
of possible updates, e.g.

let P1 and P2 be two programs with the same signature \sigma.
We say that a program T is a definition (in terms of \sigma)
if heads of rules in T contain no elements of \sigma. 

We say that P1 and P2 are equivalent w.r.t. definitions
if for any definition T, P1 + T is equivalent to P2 + T.

So, a question: Are the above programs equivalent w.r.t.
definitions?

General questions like these were addressed by several people 
(including myself) but the papers on the subject are sporadic
at best. The question of discovering important "updates"
(or transformations)
and equivalence conditions under these updates is very important
and deserves very serious attention.


COMMENTS?