Заперечення як відмова

Запере́чення як відмо́ва (англ. negation as failure, NAF) — це немонотонне правило висновування в логічному програмуванні, що застосовується для виведення ${\displaystyle \mathrm {not} ~p}$ (тобто припущення, що ${\displaystyle ~p}$ не витримується) з відмови виведення ${\displaystyle ~p}$. Зауважте, що ${\displaystyle \mathrm {not} ~p}$ може відрізнятися від твердження ${\displaystyle \neg p}$ логічного заперечення ${\displaystyle ~p}$ в залежності від повноти алгоритму висновування, і, таким чином, також і від системи формальної логіки.

Заперечення як відмова було важливою особливістю логічного програмування з найраніших днів як мови програмування Planner, так і мови програмування Пролог. У Пролозі воно зазвичай реалізується прологовими позалогічними конструкціями.

У Planner заперечення як відмову може бути реалізовано наступним чином:

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

що каже, що якщо вичерпний пошук доведення p завершився відмовою, то стверджувати ¬p.^[1] Зауважте, що наведений вище приклад використовує справжнє математичне заперечення, що не може бути виражено в Пролозі.

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

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

${\displaystyle q\leftarrow s}$

${\displaystyle q\leftarrow t}$

${\displaystyle t\leftarrow }$

заперечення як відмова виводить ${\displaystyle \mathrm {not} ~s}$, ${\displaystyle \mathrm {not} ~r}$ та ${\displaystyle ~p}$.

Семантика заперечення як відмови залишалася відкритим питанням, поки Кейт Кларк [1978] не показав, що воно є коректним по відношенню до повної логічної програми, де, грубо кажучи, «лише» та ${\displaystyle \leftarrow }$ інтерпретуються як «якщо і лише якщо» (англ. if and only if), що записується як «${\displaystyle \equiv }$» (або англ. «iif»).

Наприклад, повною системою для наведених вище чотирьох формул є

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

Правило висновування заперечення як відмови імітує міркування із явним застосуванням повноти, коли заперечуються обидва боки еквівалентності, і заперечення правого боку поширюється донизу аж до атомарних формул^[en]. Наприклад, щоби показати ${\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} }$

В не-пропозиційному випадку ця повна система потребує доповнення аксіомами еквівалентності, щоби формалізувати припущення, що об'єкти з відмінними назвами є відмінними. Заперечення як відмова імітує це відмовою уніфікації. Наприклад, якщо задано лише два твердження

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

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

то заперечення як відмова виводить ${\displaystyle \mathrm {not} ~p(c)}$.

Повною системою цієї програми є

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

доповнене аксіомами унікальності назв та аксіомами замкненості області визначення.

Семантика повноти тісно пов'язана як із обкреслюванням^[en], так і з припущенням про замкненість світу^[en].

Семантика повноти виправдовує інтерпретування результату ${\displaystyle \mathrm {not} ~p}$ висновування запереченням як відмовою як класичне заперечення ${\displaystyle \neg p}$ твердження ${\displaystyle p}$. Проте, Майкл Гельфонд^[en] [1987] показав, що ${\displaystyle \mathrm {not} ~p}$ також можливо інтерпретувати буквально як «${\displaystyle p}$ не може бути показано», «${\displaystyle p}$ є невідомим», «${\displaystyle p}$ не є переконливим», як в автоепістемній логіці^[en]. Автоепістемологічна інтерпретація була в подальшому розвинена Гельфондом та Ліфшицем^[en], і є основою програмування наборами відповідей (англ. answer set programming, ASP).

Автоепістемологічна семантика чистої прологової програми P з літералами заперечення як відмови отримується шляхом «розширення» P набором замкнених (таких, що не містять змінних) літералів заперечення як відмови Δ, що є стійким у тому сенсі, що

Δ = {${\displaystyle \mathrm {not} ~p}$ | ${\displaystyle p}$ не передбачається P ∪ Δ}

Іншими словами, набір припущень Δ про те, що не може бути показано, є стійким тоді й лише тоді, коли Δ є набором усіх речень, що дійсно не може бути показано програмою P, розширеною набором Δ. Тут, через простоту синтаксису чистих прологових програм, «не передбачається» можна розуміти дуже просто як вивідність із застосуванням самих лише modus ponens та універсальної конкретизації^[en].

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

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

Автоепістемологічну інтерпретацію заперечення як відмови можна поєднувати з класичним запереченням, як в розширеному логічному програмуванні та програмуванні наборами відповідей. Поєднуючи ці два заперечення, можна виразити, наприклад,

${\displaystyle \neg p\leftarrow \mathrm {not} ~p}$ (припущення про замкненість світу) та

${\displaystyle p\leftarrow \mathrm {not} ~\neg p}$ (${\displaystyle p}$ витримується за замовчуванням).

• Індетермінізм

• K. Clark [1978, 1987]. Negation as failure [Архівовано 23 вересня 2015 у Wayback Machine.]. Readings in nonmonotonic reasoning, Morgan Kaufmann Publishers, pages 311—325. (англ.)
• M. Gelfond [1987] On Stratified Autoepistemic Theories [Архівовано 24 серпня 2007 у Wayback Machine.] Proc. AAAI, pages 207—211. (англ.)
• M. Gelfond and V. Lifschitz [1988] The Stable Model Semantics for Logic Programming Proc. 5th International Conference and Symposium on Logic Programming (R. Kowalski and K. Bowen, eds), MIT Press, pages 1070—1080. (англ.)
• J.C. Shepherdson [1984] Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption, Journal of Logic Programming, vol 1, 1984, pages 51-81. (англ.)
• J.C. Shepherdson [1985] Negation as failure II, Journal of Logic Programming, vol 3, 1985, pages 185—202. (англ.)

• Звіт [Архівовано 23 вересня 2020 у Wayback Machine.] робочої групи W3C про мови правил для взаємодії. Включає зауваження стосовно заперечення як відмови (англ. NAF), та обмеженого заперечення як відмови (англ. scoped negation as failure, SNAF). (англ.)