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:
Satisfy the rules of Π. In other words, believe in the head of a rule if you believe in its body.
Do not believe in contradictions.
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 statementp
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).
“Negation as failure” (also known as “weak negation”) is a concept in logic programming that refers to treating the statement “not P” as true when we are unable to find or derive the statement “P”. This is the approach that RDFox takes when it comes to reasoning.
Actually, negation in Prolog is the so-called negation as failure, which means that to negate p one tries to prove p (just executing it), and if p is proved, then its negation, not(p), fails. Conversely, if p fails during execution, then not(p) will succeed.
Because of the problems of negation-as-failure, negation in Prolog is represented in modern Prolog interpreters using the symbol \+ , which is supposed to be a mnemonic for not provable with the \ standing for not and the + for provable.
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With