Диз'юнкт Горна
В математичній логіці та логічному програмуванні диз'ю́нкт Го́рна (англ. Horn clause) — це логічна формула певного правилоподібного вигляду, який надає їй корисних властивостей для застосування в логічному програмуванні, формальних специфікаціях та теорії моделей. Диз'юнкти Горна названо на честь логіка Альфреда Горна[en], який першим 1951 року зазначив їхню важливість.[1]
Диз'юнкт Горна є диз'юнктом (диз'юнкцією літералів) зі щонайбільше одним ствердним, тобто, не заперечним, літералом.
І навпаки, диз'юнкція літералів зі щонайбільше одним заперечним літералом називається подві́йно-го́рновим диз'ю́нктом (англ. dual-Horn clause).
Диз'юнкт Горна із рівно одним ствердним літералом називається ви́значеним тве́рдженням (англ. definite clause); визначене твердження без заперечних літералів іноді називається фа́ктом (англ. fact); а диз'юнкт Горна без ствердного літералу іноді називається цільови́м тве́рдженням (англ. goal clause, зауважте, що порожнє твердження, яке не складається з жодного літералу, є цільовим твердженням). Ці три типи диз'юнктів Горна проілюстровано в наступному предикатному прикладі:
| Диз'юнктивний вигляд | Імплікативний вигляд | Інтуїтивно читається як | |
|---|---|---|---|
| Визначене твердження | ¬p ∨ ¬q ∨ … ∨ ¬t ∨ u | u ← p ∧ q ∧ … ∧ t | припустити, що, якщо p і q і … і t всі витримуються, то u також витримується |
| Факт | u | u | припустити, що u витримується |
| Цільове твердження | ¬p ∨ ¬q ∨ … ∨ ¬t | хиба ← p ∧ q ∧ … ∧ t | показати, що p і q і … і t всі витримуються [прим. 1] |
В не предикатному випадку всі змінні у твердженні є неявно загальнісно квантифікованими в межах усього твердження. Таким чином, наприклад,
- ¬ людина(X) ∨ смертна(X)
відповідає
- ∀X(¬ людина(X) ∨ смертна(X))
що є логічно рівнозначним
- ∀X (людина(X) → смертна(X))
Диз'юнкти Грона відіграють основу роль у конструктивній та обчислювальній логіці[en]. Вони є важливими в автоматичному доведенні теорем резолюцією першого порядку, оскільки резольвента двох диз'юнктів Горна сама є диз'юнктом Горна, а резольвента цільового твердження та визначеного твердження є цільовим твердженням. Ці властивості диз'юнктів Горна можуть приводити до підвищення ефективності у доведенні теорем (представлених як заперечення цільового твердження).
Предикатні диз'юнкти Горна становлять інтерес у теорії складності обчислень. Задача знаходження таких присвоювань значень істинності, щоби зробити кон'юнкцію предикатних диз'юнктів Горна істинною, є P-повною[en], розв'язуваною за лінійний час,[2] й іноді званою задовільністю за Горном[en] (англ. Horn-satisfiability, HORNSAT). (Проте не обмежена задача булевої задовільності є NP-повною.) Задовільність диз'юнктів Горна першого порядку є нерозв'язною.[джерело?]
Диз'юнкти Горна є також основою логічного програмування, де є звичним записувати визначені твердження у вигляді імплікації:
- (p ∧ q ∧ … ∧ t) → u
Фактично, резолюція цільового твердження визначеним твердженням для породження нового цільового твердження є основою правила виведення ВЛВ-резолюції, що використовується для реалізації логічного програмування мовою програмування Пролог.
В логічному програмуванні визначене твердження поводиться як процедура перетворення мети. Наприклад, записаний вище диз'юнкт Горна поводиться як процедура: щоби показати u, показати p і показати q і … і показати t.
Для підкреслення цього зворотного застосування твердження його часто записують у зворотному вигляді:
- u ← (p ∧ q ∧ … ∧ t)
Прологом це записується як
u :- p, q, ..., t.
В логічному програмуванні та Datalog обчислення та оцінка запитів виконуються представленням заперечення задачі для розв'язання як цільового твердження. Наприклад, задача розв'язання існувально квантифікованої кон'юнкції ствердних літералів
- ∃X (p ∧ q ∧ … ∧ t)
представляється запереченням цієї задачі (запереченням того, що вона має розв'язок), і представленням її в логічно рівнозначному вигляді цільового твердження
- ∀X (хиба ← p ∧ q ∧ … ∧ t)
Прологом це записується як
:- p, q, ..., t.
Розв'язання задачі зводиться до виведення спростування, яке представлено порожнім твердженням (або «хибою»). Розв'язком задачі є заміна термами змінних у цільовому твердженні, яку може бути виділено з доведення спростування. При застосуванні таким чином цільові твердження є подібними до кон'юнктивних запитів[en] у реляційних базах даних, а логіка диз'юнктів Горна за обчислювальною силою є еквівалентною до універсальної машини Тюрінга.
Прологовий запис насправді є неоднозначним, і термін «цільове твердження» іноді теж використовується неоднозначно. Змінні в цільовому твердженні можуть читатися як загальнісно або існувально квантифіковані, а виведення «хиби» може інтерпретуватися або як виведення заперечення, або як виведення успішного розв'язку розв'язуваної задачі.
Ван Емден та Ковальський 1976 року дослідили теоретико-модельні властивості диз'юнктів Горна в контексті логічного програмування, показавши, що кожен набір визначених тверджень D має унікальну мінімальну модель M. Атомарна формула A логічно випливає з D тоді й лише тоді, коли A є істинною в M. Звідси випливає, що задача P, представлена існувально квантифікованою кон'юнкцією ствердних літералів, логічно випливає з D тоді й лише тоді, коли P є істинною в M. Семантика мінімальної моделі диз'юнктів Горна є основою для семантики стійких моделей логічних програм.[3]
- ↑ Як і в резолюційному доведенні теорем, інтуїтивне значення «показати φ» та «припустити ¬φ» є синонімічним (непрямий доказ); вони обидва відповідають одній і тій самій формулі, тобто, ¬φ. Таким чином, інструмент механічного доведення потребує підтримки лише одного набору формул (припущень) замість двох (припущень та (під)цілей).
- ↑ Horn, Alfred (1951). On sentences which are true of direct unions of algebras. Journal of Symbolic Logic[en]. 16 (1): 14—21. doi:10.2307/2268661. (англ.)
- ↑ Dowling, William F.; Gallier, Jean H. (1984). Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming[en]. 1 (3): 267—284. doi:10.1016/0743-1066(84)90014-1. (англ.)
- ↑ van Emden, M. H.; Kowalski, R. A. (1976). The semantics of predicate logic as a programming language (PDF). Journal of the ACM[en]. 23 (4): 733—742. doi:10.1145/321978.321991. Архів оригіналу (PDF) за 3 березня 2016. Процитовано 31 січня 2016.
