Say I have the following theory:
a(X) :- \+ b(X).
b(X) :- \+ c(X).
c(a).
It simply says true, which is of course correct, a(X)
is true because there is no b(X)
(with negation as finite failure). Since there is only a b(X)
if there is no c(X)
and we have c(a)
, one can state this is true. I was wondering however why Prolog does not provide the answer X = a
? Say for instance I introduce some semantics:
noOrphan(X) :- \+ orphan(X).
orphan(X) :- \+ parent(_,X).
parent(david,michael).
Of course if I query noOrphan(michael)
, this will result in true
and noOrphan(david)
in false
(since I didn't define a parent for david
)., but I was wondering why there is no proactive way of detecting which persons (michael
, david
,...) belong to the noOrphan/1
relation?
This probably is a result of the backtracking mechanism of Prolog, but Prolog could maintain a state which validates if one is searching in the positive way (0,2,4,...) negations deep, or the negative way (1,3,5,...) negations deep.
\+
is based on two assumptions: negation as finite failure and the closed world assumption. However the binding is still valid under both assumptions as far as I know... – Numismatology\+
as well asnot
does not meannot
as in logic but simply not provable (under the cwa). This is the meaning of the negation as failure in the SLD. – Homemade