Prolog Unification with not()

1
votes

I am just learning prolog and there is a thing I can't get my head over.

Suppose I have the following program

value(v).

a(X) :- not(value(X)).

So a(v). gives me false, as value(v) can be proved correct.

a(w) gives me true, as there is no fact value(w), therefore, even when trying, it can't be proved correct.

In my understanding, requesting a(X). should give me the first possible value that makes value(X) unproveable. There should be an infinite amount of possibilities, as only value(v) is correct.

But why does Prolog keep answering false?

2
prologunificationprolog-dif
It depends on how you view falsification, what is false? How do you prove that something is false? One view of it is that Everything that is not provable is false, which is a view where you imagine that you live in a world where everything that is true is provable (which is debatable ofcourse). In prolog the \+ operator works with negation as failure semantics, which was what I tried to describe above. Hope that gives some clues. – Limmen
Yes, If we define false as not proveable, then Prolog could achieve the goal by providing examples that it is unable to prove correct? – user3207838
But I guess the problem is that Prolog is always looking to make things true, and in this case, we would basically reverse the engine? – user3207838

2 Answers

2
votes

First of all, please use the ISO predicate (\+)/1 instead of not/1.

Second, please don't use (\+)/1 to denote disequality of terms: (\+)/1 is incomplete in Prolog, and thus not logically sound. It is not logical negation, but rather denotes "not provable".

In your case: ?- value(X). succeeds, so it is provable, so ?- \+ value(X). fails although there are instantiations that make the query succeed.

In particular, ?- \+ value(a). succeeds.

So we have:

?-        \+ value(V).
false.

But a more specific query succeeds:

?- V = a, \+ value(V).
V = a.

This obviously runs counter to logical properties we expect from pure relations. See .

To denote disequality of terms, use dif/2. If your Prolog system does not support dif/2, ask for its inclusion, or use iso_dif/2 as a safe approximation that is logically sound. See for more information.

1
votes

Prolog operates under "closed world assumption" – it only knows what we told it about. In particular, we've told it nothing about no w, u, or any other stuff, so how could it produce them to us? And why should w come before u, and not vice versa?

The only thing sensible could be to produce (X, dif(X,v)), but it would be the answer to a different question, namely, "how to make a(X) provable?", not the one Prolog is actually answering, namely "is a(X) provable?".

To ease up your cognitive burden, rename the Prolog prompt's replies in your head from true to Yes, and from false to No.

Yes would mean Prolog telling us "yes, I could prove it!", and No – "no, I couldn't prove it."

Also rename "not" to read \+ as not_provable, mentally.