Search code examples
prologfirst-order-logic

Prolog query satisfiable but returns false

I have a simple example below of a prolog program I have written, which contains a satisfiable query that always returns false for searches.

male(william).
male(harry).

% parent(x,y) - the parent of x is y
parent(william, diana).
parent(william, charles).
parent(harry, diana).
parent(harry, charles).

% Brother - the brother of X is Y
brother(X,Y) :- X\=Y, parent(X,A), parent(Y,A), male(Y).

When I ask if two constants are brothers, that works fine, but if I try to find a brother of a constant prolog returns false.

?- brother(william,harry).
true

?- brother(william,X).
false.

What am I doing wrong?

Solution

  • The problem is here X\=Y this part lucks logical purity since \=/2 is non-monotonic. Simply to make it work change the order:

    brother(X,Y) :- X\=Y, parent(X,A), parent(Y,A), male(Y).

    to:

    brother(X,Y) :-  parent(X,A), parent(Y,A), male(Y), X\=Y.

    But a much better solution would be to use dif/2 which is preserves purity:

    brother(X,Y) :- dif(X,Y), parent(X,A), parent(Y,A), male(Y).