Отрицание как неудача - Negation as failure

Отрицание как неудача (NAF, для краткости) является немонотонный правило вывода в логическое программирование, используется для получения ${\displaystyle \mathrm {not} ~p}$ (т.е. что ${\displaystyle ~p}$ предполагается, что не выполняется) из-за невозможности получить ${\displaystyle ~p}$. Обратите внимание, что ${\displaystyle \mathrm {not} ~p}$ может отличаться от утверждения ${\displaystyle \neg p}$ из логическое отрицание из ${\displaystyle ~p}$, в зависимости от полнота алгоритма вывода и, следовательно, также и в системе формальной логики.

Отрицание как неудача было важной чертой логического программирования с первых дней существования обоих. Планировщик и Пролог. В Прологе это обычно реализуется с использованием внелогических конструкций Пролога.

Семантика планировщика

В Planner отрицание как сбой может быть реализовано следующим образом:

если (нет (Цель п)), тогда (утверждать ¬p)

который говорит, что если исчерпывающий поиск, чтобы доказать п терпит неудачу, затем утверждать ¬p.^[1] Это утверждает, что предложение п будет считаться «неверным» при любой последующей обработке. Однако, поскольку Planner не основан на логической модели, логическая интерпретация предшествующего остается неясной.

Семантика пролога

В чистом Прологе литералы NAF вида ${\displaystyle \mathrm {not} ~p}$ может находиться в теле предложений и может использоваться для получения других литералов NAF. Например, учитывая только четыре пункта

${\displaystyle p\leftarrow q\land \mathrm {not} ~r}$

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

NAF является производным ${\displaystyle \mathrm {not} ~s}$, ${\displaystyle \mathrm {not} ~r}$ и ${\displaystyle ~p}$.

Семантика завершения

Семантика NAF оставалась открытым вопросом до 1978 года, когда Кейт Кларк показал, что это правильно в отношении завершения логической программы, где, грубо говоря, «только» и ${\displaystyle \leftarrow }$ интерпретируются как «если и только если», записываются как «если и только если» или${\displaystyle \equiv }$".

Например, завершение четырех пунктов выше

${\displaystyle p\equiv q\land \mathrm {not} ~r}$

${\displaystyle q\equiv s\lor t}$

${\displaystyle t\equiv \mathrm {true} }$

${\displaystyle r\equiv \mathrm {false} }$

${\displaystyle s\equiv \mathrm {false} }$

Правило вывода NAF явно имитирует рассуждения с завершением, где обе стороны эквивалентности отрицаются, а отрицание в правой части распределяется вниз до атомарные формулы. Например, чтобы показать ${\displaystyle \mathrm {not} ~p}$, NAF моделирует рассуждения с эквивалентностями

${\displaystyle \mathrm {not} ~p\equiv \mathrm {not} ~q\lor r}$

${\displaystyle \mathrm {not} ~q\equiv \mathrm {not} ~s\land \mathrm {not} ~t}$

${\displaystyle \mathrm {not} ~t\equiv \mathrm {false} }$

${\displaystyle \mathrm {not} ~r\equiv \mathrm {true} }$

${\displaystyle \mathrm {not} ~s\equiv \mathrm {true} }$

В непропозициональном случае завершение необходимо дополнить аксиомами равенства, чтобы формализовать предположение, что индивиды с разными именами различны. NAF моделирует это отказом от унификации. Например, учитывая только два пункта

${\displaystyle p(a)\leftarrow }$

${\displaystyle p(b)\leftarrow }$ т

NAF является производным ${\displaystyle \mathrm {not} ~p(c)}$.

Завершение программы

${\displaystyle p(X)\equiv X=a\lor X=b}$

дополнен аксиомами уникальных имен и аксиомами закрытия домена.

Семантика завершения тесно связана как с ограничение и к предположение о закрытом мире.

Аутоэпистемическая семантика

Семантика завершения оправдывает интерпретацию результата ${\displaystyle \mathrm {not} ~p}$ вывода NAF как классического отрицания ${\displaystyle \neg p}$ из ${\displaystyle p}$. Однако в 1987 г. Майкл Гельфонд показал, что можно также интерпретировать ${\displaystyle \mathrm {not} ~p}$ буквально как "${\displaystyle p}$ не может быть показано ","${\displaystyle p}$ не известно "или"${\displaystyle p}$ не верится ", как в аутоэпистемическая логика. Аутоэпистемическая интерпретация была развита Гельфондом и Лифшиц в 1988 году и является основой программирование набора ответов.

Семантика автоэпистемы чистой программы Пролога P с литералами NAF получается "расширением" P с помощью набора основных (без переменных) литералов NAF Δ, которые являются стабильный в том смысле, что

Δ = {${\displaystyle \mathrm {not} ~p}$ | ${\displaystyle p}$ не следует из P ∪ Δ}

Другими словами, набор предположений Δ о том, что нельзя показать, является стабильный тогда и только тогда, когда Δ - это множество всех предложений, которые действительно не могут быть показаны из программы P, расширенной на Δ. Здесь, из-за простого синтаксиса программ на чистом Прологе, «подразумевается» можно очень просто понимать как выводимость с использованием только modus ponens и универсального создания экземпляров.

Программа может иметь ноль, одно или несколько стабильных расширений. Например,

${\displaystyle p\leftarrow \mathrm {not} ~p}$

не имеет стабильных расширений.

${\displaystyle p\leftarrow \mathrm {not} ~q}$

имеет ровно одно устойчивое разложение Δ = {${\displaystyle \mathrm {not} ~q}$}

${\displaystyle p\leftarrow \mathrm {not} ~q}$

${\displaystyle q\leftarrow \mathrm {not} ~p}$

имеет ровно два устойчивых разложения Δ₁ = {${\displaystyle \mathrm {not} ~p}$} и Δ₂ = {${\displaystyle \mathrm {not} ~q}$}.

Аутоэпистемическая интерпретация NAF может сочетаться с классическим отрицанием, как в расширенном логическом программировании и программирование набора ответов. Комбинируя два отрицания, можно выразить, например,

${\displaystyle \neg p\leftarrow \mathrm {not} ~p}$(предположение о замкнутом мире) и

${\displaystyle p\leftarrow \mathrm {not} ~\neg p}$ (${\displaystyle p}$ по умолчанию).

Сноски

1. Кларк, Кит (1978). Логика и базы данных (PDF). Springer-Verlag. С. 293–322 (Отрицание как неудача). Дои:10.1007/978-1-4684-3384-5_11.

Рекомендации

• К. Кларк [1978, 1987]. Отрицание как неудача. Чтения в немонотонных рассуждениях, Издательство Морган Кауфманн, страницы 311-325.
• М. Гельфонд [1987] О стратифицированных автоэпистемических теориях Proc. AAAI 1987, страницы 207-211.
• М. Гельфонд и В. Лифшиц [1988] Семантика стабильной модели для логического программирования Proc. 5-я Международная конференция и симпозиум по логическому программированию (Р. Ковальский и К. Боуэн, ред.), MIT Press, страницы 1070-1080.
• Дж. К. Шепердсон [1984] Отрицание как неудача: сравнение завершенных данных Кларка и предположения о закрытом мире Рейтера, Журнал логического программирования, том 1, 1984 г., страницы 51–81.
• Дж. К. Шепердсон [1985] Отрицание как неудача II, Журнал логического программирования, том 3, 1985, страницы 185-202.

внешняя ссылка

• Отчет из семинара W3C по языкам правил для взаимодействия. Включает примечания по NAF и SNAF (отрицание с ограничением как отказ).