Логическое отрицание в прологе

Question

Я прочитал довольно много о Отрицании Пролога Отказом, где Пролог, чтобы доказать это \+Goal держит пытается доказать, что Goal выходит из строя.

Это тесно связано с CWA (предположение о близком мире), где, например, если мы запрашиваем \+P(a) (где P является предикатом арности 1), и у нас нет никаких подсказок, которые приводят к доказательству P(a) Пролог предполагает (из-за CWA), что not P(a) держит так \+P(a) преуспевает.

Из того, что я искал, это способ решить слабость классической логики, когда мы не имеем ни малейшего представления о P(a) тогда мы не могли ответить \+P(a) держит.

Описанное выше было способом введения немонотонных рассуждений в Пролог. Более того, интересная часть заключается в том, что Кларк доказал, что отрицание по неудаче совместимо / схоже с классическим отрицанием только для основных предложений. Я понимаю что например

X=1, \+X==1.: должен возвращать false в прологе (и в классической логике).

\+X==1, X=1.: должен возвращать false в классической логике, но это успешно в Прологе, так как время, когда NF проверяется, X не связано, это отличается от классической Pure Logic.

\+X==1.: не должен давать никакого ответа в классической логике до тех пор, пока X не будет связан, но в Прологе он возвращает false (возможно, чтобы устранить слабость классической логики), и это не то же самое / не совместимо с чистой логикой.

Моя попытка состояла в том, чтобы смоделировать классическое отрицание, благодаря предложениям @ false в комментариях, текущая реализация:

\\+(Goal) :- when(ground(Goal), \+Goal). 

Некоторое тестирование:

?- \\+(X==1).
when(ground(X), \+X==1).

?- X=1, \\+(X==1).
false.

?- \\+(X==1), X=1.
false. 

Мой вопрос:

Является ли приведенное выше правильной интерпретацией классического отрицания? (Существуют ли какие-либо очевидные случаи, когда он пропускает? Также я обеспокоен чистотой логики при использовании когда /2, безопасно ли предполагать, что вышеизложенное чисто??).

Answer 1

Пролог не может делать классическое отрицание. Так как он не использует классический вывод. Даже в присутствии завершения Кларка, он не может обнаружить следующие два классических закона:

Закон непротиворечивости: ~(p /\ ~p)

Закон исключенного среднего: p \/ ~p

Вот пример, возьмите эту логическую программу и эти запросы:

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

Завершение Кларком логической программы выглядит следующим образом, и отрицание как выполнение запроса на ошибку приводит к следующему:

   p <-> p

   loops

   loops

Завершение Кларка решает проблему определения предикатов и негативной информации. См. Также раздел 5.2 Правила и их завершение. С другой стороны, когда нет определений предикатов, CLP(X) может иногда выполнять оба закона, когда оператор отрицания определен в стиле deMorgan. Вот оператор отрицания для CLP(B):

?- listing(neg/1).
neg((A;B)) :-
    neg(A),
    neg(B).
neg((A, _)) :-
    neg(A).
neg((_, A)) :-
    neg(A).
neg(neg(A)) :-
    call(A).
neg(sat(A)) :-
    sat(~A).

И вот немного исполнения:

?- sat(P); neg(sat(P)).
P = 0 
P = 1.
?- neg((sat(P), neg(sat(P)))).
P = 0 
P = 1.

CLP (X) также будет иметь проблемы, когда отрицание влияет на домены, которые, как правило, конечны, и тогда они становятся бесконечными. Так, например, ограничение, такое как (#=)/2, ... не должно быть проблемой, так как его можно заменить на ограничение (#\=)/2, ... .

Но отрицание для CLP(FD) обычно не работает при применении к ограничениям (in)/2. Ситуацию можно слегка смягчить, если система CLP (X) предлагает реификацию. В этом случае дизъюнкция может быть сделана немного более разумной, чем просто использование обратной дизъюнкции Prolog.

Answer 2

В SWI-Prolog можно реализовать правила вывода для классической логики в правилах обработки ограничений , включая законы де Моргана и закон непротиворечивости:

      is_true(A),is_true(A) <=> is_true(A).
is_true(A=B) ==> A=B.
is_true(A\=B) ==> not(A=B).
is_true(not(A)),is_true(A) ==> false.
is_true(not((A;B))) ==> is_true((not(A),not(B))).
is_true(not((A,B))) ==> is_true((not(A);not(B))).
is_true((A,B)) ==> is_true(A),is_true(B).
is_true((A;B)) ==> is_true(A),(is_true(B);is_true(not(B)));is_true(B),(is_true(A);is_true(not(A))).
is_true(not(not(A))) ==> is_true(A).

Затем вы можете использовать решатель следующим образом:

      is_true(animal(X,A)),is_true(animal((Y,A))) ==> X \= Y,false;X==Y.
is_true((A->B)) ==> is_true(((A;not(A)),B));is_true(((not(A);A),not(B))).

main :- is_true(((X=cat;X=dog;X=moose),(not((animal(dog,tom);animal(moose,tom))),animal(X,tom)))),writeln(animal(X,tom)).

Эта программа печатает animal(cat,tom).