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?

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.