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

Запере́чення як відмо́ва (Шаблон:Lang-en) — це немонотонне правило висновування в логічному програмуванні, що застосовується для виведення $\mathrm{n}\mathrm{o}\mathrm{t}p$ (тобто припущення, що $p$ не витримується) з відмови виведення $p$. Зауважте, що $\mathrm{n}\mathrm{o}\mathrm{t}p$ може відрізнятися від твердження $\mathrm{\neg }p$ логічного заперечення $p$ в залежності від повноти алгоритму висновування, і, таким чином, також і від системи формальної логіки.

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

Семантика Planner

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

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

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

Семантика Prolog

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

$p\leftarrow q\wedge \mathrm{n}\mathrm{o}\mathrm{t}r$

$q\leftarrow s$

$q\leftarrow t$

$t\leftarrow$

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

Семантика повноти

Семантика заперечення як відмови залишалася відкритим питанням, поки Кейт Кларк [1978] не показав, що воно є коректним по відношенню до повної логічної програми, де, грубо кажучи, «лише» та $\leftarrow$ інтерпретуються як «якщо і лише якщо» (Шаблон:Lang-en), що записується як «$\equiv$» (або Шаблон:Lang-en).

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

$p\equiv q\wedge \mathrm{n}\mathrm{o}\mathrm{t}r$

$q\equiv s\vee t$

$t\equiv \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$

$r\equiv \mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$

$s\equiv \mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$

Правило висновування заперечення як відмови імітує міркування із явним застосуванням повноти, коли заперечуються обидва боки еквівалентності, і заперечення правого боку поширюється донизу аж до Шаблон:Нп. Наприклад, щоби показати $\mathrm{n}\mathrm{o}\mathrm{t}p$, заперечення як відмова імітує міркування еквівалетностями

$\mathrm{n}\mathrm{o}\mathrm{t}p\equiv \mathrm{n}\mathrm{o}\mathrm{t}q\vee r$

$\mathrm{n}\mathrm{o}\mathrm{t}q\equiv \mathrm{n}\mathrm{o}\mathrm{t}s\wedge \mathrm{n}\mathrm{o}\mathrm{t}t$

$\mathrm{n}\mathrm{o}\mathrm{t}t\equiv \mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$

$\mathrm{n}\mathrm{o}\mathrm{t}r\equiv \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$

$\mathrm{n}\mathrm{o}\mathrm{t}s\equiv \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$

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

$p(a)\leftarrow$

$p(b)\leftarrow$ t

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

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

$p(X)\equiv X=a\vee X=b$

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

Семантика повноти тісно пов'язана як із Шаблон:Нп, так і з Шаблон:Нп.

Семантика автоепістемології

Семантика повноти виправдовує інтерпретування результату $\mathrm{n}\mathrm{o}\mathrm{t}p$ висновування запереченням як відмовою як класичне заперечення $\mathrm{\neg }p$ твердження $p$. Проте, Шаблон:Нп [1987] показав, що $\mathrm{n}\mathrm{o}\mathrm{t}p$ також можливо інтерпретувати буквально як «$p$ не може бути показано», «$p$ є невідомим», «$p$ не є переконливим», як в Шаблон:Нп. Автоепістемологічна інтерпретація була в подальшому розвинена Гельфондом та Шаблон:Нп, і є основою програмування наборами відповідей (Шаблон:Lang-en).

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

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

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

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

$p\leftarrow \mathrm{n}\mathrm{o}\mathrm{t}p$

не має стабільних розширень.

$p\leftarrow \mathrm{n}\mathrm{o}\mathrm{t}q$

має строго одне стабільне розширення Δ = {$\mathrm{n}\mathrm{o}\mathrm{t}q$}

$p\leftarrow \mathrm{n}\mathrm{o}\mathrm{t}q$

$q\leftarrow \mathrm{n}\mathrm{o}\mathrm{t}p$

має строго два стабільні розширення, Δ₁ = {$\mathrm{n}\mathrm{o}\mathrm{t}p$} та Δ₂ = {$\mathrm{n}\mathrm{o}\mathrm{t}q$}.

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

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

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

Див. також

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

Джерела

• K. Clark [1978, 1987]. Negation as failure Шаблон:Webarchive. Readings in nonmonotonic reasoning, Morgan Kaufmann Publishers, pages 311—325. Шаблон:Ref-en
• M. Gelfond [1987] On Stratified Autoepistemic Theories Шаблон:Webarchive Proc. AAAI, pages 207—211. Шаблон:Ref-en
• 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. Шаблон:Ref-en
• 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. Шаблон:Ref-en
• J.C. Shepherdson [1985] Negation as failure II, Journal of Logic Programming, vol 3, 1985, pages 185—202. Шаблон:Ref-en

Посилання

• Звіт Шаблон:Webarchive робочої групи W3C про мови правил для взаємодії. Включає зауваження стосовно заперечення як відмови (Шаблон:Lang-en), та обмеженого заперечення як відмови (Шаблон:Lang-en). Шаблон:Ref-en