Не равная операция в swi-прологе

Question

Я пытаюсь сравнить два числа Пеано в прологе, но некоторые результаты неверны.

Любой может помочь мне, это мой код:

%Not Equal
notequal(0,s(A),X).
notequal(s(A),0,X).
notequal(s(A),s(B),C):- A/=B .

ИЛИ ЖЕ

%Not Equal
notequal(0,s(A),X).
notequal(s(A),0,X).
notequal(s(A),s(B),C):- minus(A,s(0),S1),minus(B,s(0),S2),notequal(S1,S2,C) .

Выход:

?- notequal(s(0),s(s(0)),S).
false.

?- notequal(s(0),0,S).
true .

?- notequal(0,s(0),S).
true.

Первый вывод неверен

Спасибо.

Answer 1

Вам не нужно три аргумента для такого предиката, ведь вы хотите описать связь между двумя числами. И ваше последнее правило должно снова вызвать сам предикат:

notequal(0,s(_)).
notequal(s(_),0).
notequal(s(A),s(B)) :-  % s(A) and s(B) are not equal if
   notequal(A,B).       % A and B are not equal

Это дает желаемые ответы:

?- notequal(0,0).
false.

?- notequal(0,s(0)).
true.

?- notequal(s(0),s(0)).
false.

?- notequal(s(s(0)),s(0)).
true ;
false.

?- notequal(s(s(0)),0).
true ;
false.

Вы также можете использовать это только с одним аргументом:

?- notequal(s(0),B).
B = 0 ;
B = s(s(_G2450)).

?- notequal(A,s(0)).
A = 0 ;
A = s(s(_G2450)).

Как видите, все возможности покрыты этими двумя ответами. Даже самый общий запрос производит решения:

?- notequal(A,B).
A = 0,
B = s(_G2456) ;
A = s(_G2456),
B = 0 ;
A = s(0),
B = s(s(_G2460)) ;
A = s(s(_G2460)),
B = s(0) ;
A = s(s(0)),
B = s(s(s(_G2464))) ;
.
.
.

Answer 2

Если вам не нужно выяснять фактический порядок двух чисел, скажем, для сортировки на основе сравнения, а нужно только указать безопасный неравенство терминов, используйте широко доступный встроенный предикат dif/2!

Некоторые примеры запросов:

?- dif(0, 0).
false.

?- dif(0, s(0)).
true.

?- dif(s(0), s(0)).
false.

?- dif(s(s(0)), s(0)).
true.

?- dif(s(s(0)), 0).
true.

Это также безопасно работает в наиболее общем случае:

?- dif(A, B).
dif(A, B).             % residual goal indicates pending disequality constraint