CODEWITHSUNDEEP
prologunificationprolog-dif
user3207838
user3207838

Reputation: 676

Prolog Unification with not()

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?

Upvotes: 1

Views: 294

Answers (2)

Will Ness
Will Ness

Reputation: 71070

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.

Upvotes: 1

mat
mat

Reputation: 40768

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.

Upvotes: 2

Related Questions