A three-line puzzle about what “not” means in logic programming. Alice loves Bob, nothing says she hates him, and from that absence the program concludes that she hates nobody, in a precise, limited sense.
Run it in the playground · Source
Prolog’s \+ Goal succeeds when Goal cannot be proved. That is not the same
as “Goal is false”: it means “false as far as this program knows”. This
example uses that kind of negation and makes its scope visible.
loves(alice, bob).
person(bob).
hates(alice, nobody) :-
person(X),
\+ hates(alice, X).
Read the rule as: Alice hates nobody if there is some person she cannot be
shown to hate. The only person is Bob, and no clause concludes
hates(alice, bob).
eyeprolog examples/snaf.pl
hates(alice, nobody).
step(hates(alice, nobody), rule(3), ['X' = bob], [person(bob), \+ hates(alice, bob)]).
step(person(bob), fact(2), [], []).
step(\+ hates(alice, bob), absent, [], []).
The conclusion rests on a person (Bob, fact 2) and an absence: the program
does not derive hates(alice, bob). The proof marks that step absent
rather than pretending it is a positive fact.
condition('C1', resolution, ok, 2).
obligation(absent, theory_scoped, \+ hates(alice, bob)).
verdict(checked_with_obligations).
The rule and the fact are verified. The absence cannot be: no proof can show that something is unprovable. The checker therefore lists it as an obligation, scoped to this theory. The verdict means: valid, provided this program really is the whole story about whom Alice hates.
hates(alice, bob). Now Bob is hated, and the run prints nothing.--warnings. EyeProlog reports hates/2 depends negatively on
hates/2: the predicate refers to its own negation. Why does it still give
a sensible answer here?person(carol). Does the answer change? Does the proof?Learn more in The Art of EyeProlog, Chapter 7.