Отрицание как неудача

Правило вывода, трактующее недоказуемость как ложность

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

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

В более общем смысле этот вид отрицания известен как слабое отрицание [ ^{1] [2]} в отличие от сильного (т. е. явного, доказуемого) отрицания.

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

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

if (not (goal p)), then (assert ¬p)

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

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

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

${\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}$ ${\displaystyle t}$ ${\displaystyle q}$

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

Семантика 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 явно имитирует рассуждение с завершением, где обе стороны эквивалентности отрицаются, а отрицание в правой части распространяется вплоть до атомарных формул . Например, чтобы показать , NAF имитирует рассуждение с эквивалентностями ${\displaystyle \mathrm {not} ~p}$

${\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 t}$

NAF происходит от . ${\displaystyle \mathrm {not} ~p(c)}$

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

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

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

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

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

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

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

Δ = {не p | p не подразумевается из P ∪ Δ}

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

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

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

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

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

имеет ровно одно устойчивое расширение Δ = {не q }

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

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

имеет ровно два устойчивых расширения Δ ₁ = {not p } и Δ ₂ = {not q }.

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

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

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

Сноски

1. Билкова, М.; Колачито, А. (2020). «Теория доказательств положительной логики со слабым отрицанием». Студия Логика . 108 (4): 649–686. arXiv : 1907.05411 . doi : 10.1007/s11225-019-09869-y. S2CID  195886568.
2. Вагнер, Г. (2003). «Web Rules Need Two Types of Negation» (PDF) . В Bry, F.; Henze, N.; Maluszynski, J. (ред.). Principles and Practice of Semantic Web Reasoning. PPSW3 2003. Lecture Notes in Computer Science. Vol. 2901. Lecture Notes in Computer Science: Springer. стр. 33–50. doi :10.1007/978-3-540-24572-8_3. ISBN 978-3-540-24572-8.
3. Кларк, Кит (1978). «Отрицание как неудача» (PDF) . Логика и базы данных . Springer-Verlag . стр. 293–322. doi :10.1007/978-1-4684-3384-5_11. ISBN 978-1-4684-3384-5.

Ссылки

• Кларк, К. (1987) [1978]. «Отрицание как неудача». В Гинзберге, М.Л. (ред.). Чтения по немонотонному рассуждению . Морган Кауфманн. стр. 311–325. ISBN 978-0-934613-45-3.
• Гельфонд, М. (1987). «О стратифицированных автоэпистемических теориях» (PDF) . AAAI'87: Труды шестой Национальной конференции по искусственному интеллекту . AAAI Press. стр. 207–211. ISBN 978-0-934613-42-2.
• Gelfond, M.; Lifschitz, V. (1988). "Семантика стабильной модели для логического программирования". В Kowalski, R.; Bowen, K. (ред.). Proc. 5-я международная конференция и симпозиум по логическому программированию . MIT Press. стр. 1070–80. CiteSeerX  10.1.1.24.6050 . ISBN 978-0-262-61054-4.
• Шепердсон, Дж. К. (1984). «Отрицание как неудача: сравнение теории завершенных данных Кларка и предположения о замкнутом мире Рейтера». Журнал логического программирования . 1 : 51–81. doi :10.1016/0743-1066(84)90023-2.
• Шепердсон, Дж. К. (1985). «Отрицание как неудача II». Журнал логического программирования . 2 (3): 185–202. doi :10.1016/0743-1066(85)90018-4.

Внешние ссылки

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