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

Я довольно много читал про Отрицание по ошибке в Prolog, где Prolog, чтобы доказать, что \+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 не привязано, это отличается от классической чистой логики.

\+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.

Мой вопрос:

Правильно ли вышесказанное толкование классического отрицания? (Есть ли какие-нибудь очевидные угловые случаи, которые он пропускает? Также меня беспокоит Logic Purity при использовании when/2, можно ли предположить, что вышесказанное чисто ??).


prolog prolog-coroutining logical-purity negation
person coder    schedule 09.12.2017    source источник
comment
ground/2 действительно не имеет значения.   -  person false    schedule 09.12.2017
comment
Значение отношения определяется его основной интерпретацией. Это набор основных условий, которые справедливы для этого отношения. Итак, ground/2 должно быть константой "истина". Нет ситуации, когда это ложно.   -  person false    schedule 09.12.2017
comment
О, понятно !!, значит, вы хотите написать что-то вроде: \\+(Goal) :- when(ground(Goal), \+Goal). ???   -  person coder    schedule 09.12.2017
comment
В этом есть смысл.   -  person false    schedule 09.12.2017
comment
Можно ли это считать чистым ??   -  person coder    schedule 09.12.2017
comment
Что ж, это форма немонотонного расширения. Несмотря на свои достоинства, он крайне ограничен настаиванием на обоснованности. В большинстве случаев ответом будет сбивающаяся цель, которая ничего вам не скажет. Подумайте о цели \\+( [] = [X|Xs]), которая не является заземленной, поэтому вы никогда не получите ответа, а dif([], [X|Xs]) просто добьетесь успеха.   -  person false    schedule 09.12.2017
comment
Очень хороший момент !! спасибо @false, это в значительной степени отвечает на мой вопрос, поскольку доказывает, что это неправильный подход. Вы имеете в виду какой-то подход, иначе логическое отрицание может быть невозможно ??   -  person coder    schedule 10.12.2017
comment
Кстати, ваш вопрос заслуживает гораздо более подробного ответа, который начнется с 1972 года и Prolog 0 и касается всего, что произошло до сих пор, включая ASP, а также чистое программирование в самом Prolog.   -  person false    schedule 10.12.2017
comment
Я понимаю вашу точку зрения, я думаю, что было проведено так много исследований, что поиск кажется бесконечным, спасибо за ваши ответы, ценю !!!   -  person coder    schedule 10.12.2017

Ответы (2)


arrow_upward
3
arrow_downward

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

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

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

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

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

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

   p <-> p

   loops

   loops

Завершение Кларка обращается к проблеме определений предикатов и отрицательной информации. См. Также раздел 5.2 Правила и их выполнение. С другой стороны, когда нет определений предикатов, CLP (X) иногда может выполнять оба закона, когда оператор отрицания определен в стиле деМоргана. Вот оператор отрицания для 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.

person Mostowski Collapse    schedule 18.01.2018
comment
Пролог не является классическим, но гораздо больше похож на эту интуиционистскую логику, где метка истинна означает доказуемость / есть свидетельство (в отличие от излучаемого Богом утверждения, истинного для классической логики) ситуации, охватываемой Лямбда-пролог. Я не понимаю, почему это не первое, что говорится в каждой книге по Прологу. - person David Tonhofer; 07.01.2020
comment
Интуиционистская логика требует закона непротиворечивости: ~ (p / \ ~ p), который доказуем в интуиционистской логике. Таким образом, Пролог находится ниже интуиционистской логики, можно показать, что это фрагмент так называемой минимальной логики. - person Mostowski Collapse; 18.06.2021

arrow_upward
1
arrow_downward

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

:- use_module(library(chr)).
:- chr_constraint is_true/1.
:- chr_constraint animal/2.
:- initialization(main).
:- set_prolog_flag('double_quotes','chars').

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).

Но эту формулу можно было бы решить более эффективно, используя другой алгоритм, например DPLL.

person Anderson Green    schedule 21.04.2021
comment
Я просто хотел бы спросить, как весь проект создания классического Пролога согласуется с тем фактом, что логика первого порядка неразрешима. - person tiffi; 22.04.2021