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

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

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

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

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

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

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

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

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

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

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

q\leftarrow s

q\leftarrow t

t\leftarrow

НАФ выводит $\mathrm {not} ~s$ , $\mathrm {not} ~r$ и $p$ а также $t$ и $q$ .

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

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

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

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

q\equiv s\lor t

t\equiv \mathrm {true}

r\equiv \mathrm {false}

s\equiv \mathrm {false}

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

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

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

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

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

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

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

p(a)\leftarrow

p(b)\leftarrow t

НАФ выводит $\mathrm {not} ~p(c)$ .

Завершение программы является

p(X)\equiv X=a\lor X=b

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

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

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

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

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

Δ знак равно {не р | p не подразумевается из P \cup ∆}

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

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

p\leftarrow \mathrm {not} ~p

не имеет устойчивых расширений.

p\leftarrow \mathrm {not} ~q

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

p\leftarrow \mathrm {not} ~q

q\leftarrow \mathrm {not} ~p

имеет ровно два устойчивых разложения $∆ 1 = {not p}$ и $∆ 2 = {not q}.$

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

\neg p\leftarrow \mathrm {not} ~p

(предположение о закрытом мире) и

p\leftarrow \mathrm {not} ~\neg p

(

p

сохраняется по умолчанию).

Сноски

^ Билкова, М.; Колачито, А. (2020). «Теория доказательств положительной логики со слабым отрицанием» . Студия Логика . 108 (4): 649–686. arXiv : 1907.05411 . дои : 10.1007/s11225-019-09869-y . S2CID 195886568 .
^ Вагнер, Г. (2003). «Веб-правилам нужны два вида отрицания» (PDF) . В Бри, Ф.; Хенце, Н.; Малушинский Дж. (ред.). Принципы и практика семантического веб-рассуждения. ППСВ3 2003 . Конспекты лекций по информатике. Том. 2901. Конспекты лекций по информатике: Springer. стр. 33–50. дои : 10.1007/978-3-540-24572-8_3 . ISBN 978-3-540-24572-8 .
^ Кларк, Кейт (1978). «Отрицание как неудача» (PDF) . Логика и базы данных . Спрингер-Верлаг . стр. 293–322. дои : 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: Материалы шестой Национальной конференции по искусственному интеллекту . АААИ Пресс. стр. 207–211. ISBN 978-0-934613-42-2 .
Гельфонд, М.; Лифшиц, В. (1988). «Семантика стабильной модели для логического программирования». В Ковальском, Р.; Боуэн, К. (ред.). Учеб. 5-я Международная конференция и симпозиум по логическому программированию . МТИ Пресс. стр. 1070–80. CiteSeerX 10.1.1.24.6050 . ISBN 978-0-262-61054-4 .
Шепердсон, Дж. К. (1984). «Отрицание как неудача: сравнение завершенной базы данных Кларка и предположения о закрытом мире Райтера». Журнал логического программирования . 1 : 51–81. дои : 10.1016/0743-1066(84)90023-2 .
Шепердсон, Дж. К. (1985). «Отрицание как неудача II». Журнал логического программирования . 2 (3): 185–202. дои : 10.1016/0743-1066(85)90018-4 .

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

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

[1] Билкова, М.; Колачито, А. (2020). «Теория доказательств положительной логики со слабым отрицанием» . Студия Логика . 108 (4): 649–686. arXiv : 1907.05411 . дои : 10.1007/s11225-019-09869-y . S2CID 195886568 .

[2] Вагнер, Г. (2003). «Веб-правилам нужны два вида отрицания» (PDF) . В Бри, Ф.; Хенце, Н.; Малушинский Дж. (ред.). Принципы и практика семантического веб-рассуждения. ППСВ3 2003 . Конспекты лекций по информатике. Том. 2901. Конспекты лекций по информатике: Springer. стр. 33–50. дои : 10.1007/978-3-540-24572-8_3 . ISBN 978-3-540-24572-8 .

[3] Кларк, Кейт (1978). «Отрицание как неудача» (PDF) . Логика и базы данных . Спрингер-Верлаг . стр. 293–322. дои : 10.1007/978-1-4684-3384-5_11 . ISBN 978-1-4684-3384-5 .

[1]

[2]

[3]