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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

Запере́чення як відмо́ва (англ. negation as failure, NAF) — це немонотонне правило висновування в логічному програмуванні, що застосовується для виведення (тобто припущення, що не витримується) з відмови виведення . Зауважте, що може відрізнятися від твердження логічного заперечення в залежності від повноти алгоритму висновування, і, таким чином, також і від системи формальної логіки.

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

Семантика Planner[ред.ред. код]

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

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

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

Семантика Prolog[ред.ред. код]

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

заперечення як відмова виводить , та .

Семантика повноти[ред.ред. код]

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

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

Правило висновування заперечення як відмови імітує міркування із явним застосуванням повноти, коли заперечуються обидва боки еквівалентності, і заперечення правого боку поширюється донизу аж до атомарних формул[en]. Наприклад, щоби показати , заперечення як відмова імітує міркування еквівалетностями

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

t

то заперечення як відмова виводить .

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

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

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

Семантика автоепістемології[ред.ред. код]

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

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

Δ = { | не передбачається P ∪ Δ}

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

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

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

має строго одне стабільне розширення Δ = {}

має строго два стабільні розширення, Δ1 = {} та Δ2 = {}.

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

(припущення про замкненість світу) та
( витримується за замовчуванням).

Див. також[ред.ред. код]

Виноски[ред.ред. код]

  1. Clark, Keith (1978). Logic and Data Bases. Springer-Verlag. с. 293–322 (Negation as a failure). doi:10.1007/978-1-4684-3384-5_11.  (англ.)

Джерела[ред.ред. код]

  • K. Clark [1978, 1987]. Negation as failure. Readings in nonmonotonic reasoning, Morgan Kaufmann Publishers, pages 311—325. (англ.)
  • M. Gelfond [1987] On Stratified Autoepistemic Theories 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. (англ.)

Посилання[ред.ред. код]

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