How to understand negation as failure in ASP？

Question

Suppose we have the following program:

human(socrates).
day(tomorrow).
die(X) :- human(X).
may_go_to_school(Y) :- day(Y), 
                       not holiday(Y).

If we run clingo to aquire the answer set of the program, we get

Answer: 1
human(socrates) day(tomorrow) die(socrates) may_go_to_school(tomorrow)

We know the grounder will firstly instantiate all the variables into constants, so the program after grounding will be:

human(socrates).
day(tomorrow).
die(socrates) :- human(socrates).
may_go_to_school(tomorrow) :- day(tomorrow), 
                              not holiday(tomorrow).

I read in book from Gelfond it gives 3 rules to acquire the answer sets:

1. Satisfy the rules of Π. In other words, believe in the head of a rule if you believe in its body.

2. Do not believe in contradictions.

3. Adhere to the “Rationality Principle” which says: “Believe nothing you are not forced to believe.”

Here in the rule:

may_go_to_school(tomorrow) :- day(tomorrow), 
                              not holiday(tomorrow).

we got a negation as failure not holiday(tomorrow)

As is illustrated in this book:

Symbol not is a new logical connective called default negation, (or negation as failure); not l is often read as “it is not believed that l is true.” Note that this does not imply that l is believed to be false. It is conceivable, in fact quite normal, for a rational reasoner to believe neither statement p nor its negation, ¬p.

Then based on rule 1, believe in the head of a rule if you believe in its body, should I believe the body not holiday(tomorrow). since I should believe neither holiday(tomorrow). nor ¬holiday(tomorrow).?

According to the answer, I should believe ¬holiday(tomorrow).

• Then why do we need this negation as failure?
• Can we just use classical negation?

Telesthesia

Answer 1

Can we just use classical negation?

Well it seems we can't. The problem is that we can't implement logical negation. The main idea is that Prolog generates a model (Herbrand model) for your program-theory. When we add negation, semantics of the program change so that Prolog may not be able to find a model using sld resolution. So negation as failure has the advantage that we can have a negation (not exactly logical negation) and still not having problems with program semantics like we had with classical negation.

You can take a look in my relevant question: Logical Negation in Prolog. This question does not ask exactly the same thing as this question, but @j4n bur53 in his answer describes why we can't have logical negation.

Ranger

Thanks for the link. Prolog cannot implement classical negation. This is helpful. I read on another slides saying that "In practice we do not establish the innocence of X by proving the negation of “X is guilty” Instead, we establish it by finitely failing to prove “X is guilty”." This exactly gives another way to handle the problem where we need the classical negation. I think this is just symbolized by not and its semantics. – Telesthesia

Yes I agree, in your example since we can't prove negation of "X is guilty" with Negation as Failure we prove "X is innocent" by failing to prove "X is guilty". – Ranger

Answer 2

Suppose I write instead:

may_go_to_school(D) :- not holiday(D).

Which answers do you expect, i.e., what are the models of this? And what is actually given?

The key issue is that negation as failure is straight-forward to implement, but does not fully capture what we mean with ¬ in logic. For example, what about D = hello?

Bicephalous

I have an own comprehension on this but not sure if it is right. I think not is used to represent an uncertainty at the moment. Take not holiday(tomorrow). as an example, if in the program somewhere else, holiday(tomorrow) is derived based on other rules or just a fact, i.e, I am sure tomorrow is a holiday. Then the uncertainty disappears, and not holiday(tomorrow). is judged as not satisfied. Since the body of the rule is not satisfied, the head of it isn't necessarily to believe. may_go_to_school(tomorrow) will be removed from the answer set and holiday(tomorrow) will be added. – Telesthesia

(follow the above one)And if I can never ensure holiday(tomorrow), then I choose not to believe it(the book suggests also not to believe ¬holiday(tomorrow), but I can say not holiday(tomorrow) is satisfied, thus the head will also be in the answer set just like the results I got in my question. Is this understanding right? – Telesthesia

Answer 3

You can also use classical negation in the example, but you then need the supply negative information for the holiday predicate.

To use classical negation you need to switch sides of the predicate holiday, that is you need to go from G :- not A, H to G, A :- H, i.e. move it to the head, a classical sound transformation. The result is a disjunctive clause:

may_go_to_school(Y), holiday(Y) :- day(Y).

To provide negative information here, the easiest is to provide a constraint:

:- holiday(tomorrow).

You can now run the ASP program without any default negation, since you used classical negation and provided the negative information. Here is how you would translate it to Jekejeke Prolog ASP that uses Safe Forward Chaining:

:- reexport(library(minimal/asp)).

:- forward may_go_to_school/2.

choose([day(tomorrow)]) <= posted(init).
choose([may_go_to_school(Y), holiday(Y)]) <= posted(day(Y)).
fail <= posted(holiday(tomorrow)).

And here is an example run. The constraint helps here that in the present query no second model is generated:

Jekejeke Prolog 4, Runtime Library 1.4.1 (August 20, 2019)
(c) 1985-2019, XLOG Technologies GmbH, Switzerland

?- post(init), listing(may_go_to_school/1).
may_go_to_school(tomorrow).

Yes ;
No

A more thorough modelling would consider may_go_to_school/1 itself completed and add even some more clauses to the program so that other queries also make sense.

Gustavogustavus