Відкрити головне меню

В математичній логіці та логічному програмуванні диз'ю́нкт Го́рна (англ. Horn clause) — це логічна формула певного правилоподібного вигляду, який надає їй корисних властивостей для застосування в логічному програмуванні, формальних специфікаціях та теорії моделей. Диз'юнкти Горна названо на честь логіка Альфреда Горна[en], який першим 1951 року зазначив їхню важливість.[1]

ВизначенняРедагувати

Диз'юнкт Горна є диз'юнктом (диз'юнкцією літералів) зі щонайбільше одним ствердним, тобто, не заперечним, літералом.

І навпаки, диз'юнкція літералів зі щонайбільше одним заперечним літералом називається подві́йно-го́рновим диз'ю́нктом (англ. dual-Horn clause).

Диз'юнкт Горна із рівно одним ствердним літералом називається ви́значеним тве́рдженням (англ. definite clause); визначене твердження без заперечних літералів іноді називається фа́ктом (англ. fact); а диз'юнкт Горна без ствердного літералу іноді називається цільови́м тве́рдженням (англ. goal clause, зауважте, що порожнє твердження, яке не складається з жодного літералу, є цільовим твердженням). Ці три типи диз'юнктів Горна проілюстровано в наступному предикатному прикладі:

Диз'юнктивний вигляд Імплікативний вигляд Інтуїтивно читається як
Визначене твердження ¬p ∨ ¬q ∨ … ∨ ¬tu upq ∧ … ∧ t припустити, що,
якщо p і q і … і t всі витримуються, то u також витримується
Факт u u припустити, що
u витримується
Цільове твердження ¬p ∨ ¬q ∨ … ∨ ¬t хибаpq ∧ … ∧ t показати, що
p і q і … і t всі витримуються [прим. 1]

В не предикатному випадку всі змінні у твердженні є неявно загальнісно квантифікованими в межах усього твердження. Таким чином, наприклад,

¬ людина(X) ∨ смертна(X)

відповідає

∀X(¬ людина(X) ∨ смертна(X))

що є логічно рівнозначним

∀X (людина(X) → смертна(X))

Диз'юнкти Грона відіграють основу роль у конструктивній та обчислювальній логіці[en]. Вони є важливими в автоматичному доведенні теорем резолюцією першого порядку, оскільки резольвента двох диз'юнктів Горна сама є диз'юнктом Горна, а резольвента цільового твердження та визначеного твердження є цільовим твердженням. Ці властивості диз'юнктів Горна можуть приводити до підвищення ефективності у доведенні теорем (представлених як заперечення цільового твердження).

Предикатні диз'юнкти Горна становлять інтерес у теорії складності обчислень. Задача знаходження таких присвоювань значень істинності, щоби зробити кон'юнкцію предикатних диз'юнктів Горна істинною, є P-повною[en], розв'язуваною за лінійний час,[2] й іноді званою задовільністю за Горном[en] (англ. Horn-satisfiability, HORNSAT). (Проте не обмежена задача булевої задовільності є NP-повною.) Задовільність диз'юнктів Горна першого порядку є нерозв'язною.[джерело?]

Логічне програмуванняРедагувати

Диз'юнкти Горна є також основою логічного програмування, де є звичним записувати визначені твердження у вигляді імплікації:

(pq ∧ … ∧ t) → u

Фактично, резолюція цільового твердження визначеним твердженням для породження нового цільового твердження є основою правила виведення ВЛВ-резолюції, що використовується для реалізації логічного програмування мовою програмування Пролог.

В логічному програмуванні визначене твердження поводиться як процедура перетворення мети. Наприклад, записаний вище диз'юнкт Горна поводиться як процедура: щоби показати u, показати p і показати q і … і показати t.

Для підкреслення цього зворотного застосування твердження його часто записують у зворотному вигляді:

u ← (pq ∧ … ∧ t)

Прологом це записується як

u :- p, q, ..., t.

В логічному програмуванні та Datalog обчислення та оцінка запитів виконуються представленням заперечення задачі для розв'язання як цільового твердження. Наприклад, задача розв'язання існувально квантифікованої кон'юнкції ствердних літералів

X (pq ∧ … ∧ t)

представляється запереченням цієї задачі (запереченням того, що вона має розв'язок), і представленням її в логічно рівнозначному вигляді цільового твердження

X (хибаpq ∧ … ∧ t)

Прологом це записується як

:- p, q, ..., t.

Розв'язання задачі зводиться до виведення спростування, яке представлено порожнім твердженням (або «хибою»). Розв'язком задачі є заміна термами змінних у цільовому твердженні, яку може бути виділено з доведення спростування. При застосуванні таким чином цільові твердження є подібними до кон'юнктивних запитів[en] у реляційних базах даних, а логіка диз'юнктів Горна за обчислювальною силою є еквівалентною до універсальної машини Тюрінга.

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

Ван Емден та Ковальський 1976 року дослідили теоретико-модельні властивості диз'юнктів Горна в контексті логічного програмування, показавши, що кожен набір визначених тверджень D має унікальну мінімальну модель M. Атомарна формула A логічно випливає з D тоді й лише тоді, коли A є істинною в M. Звідси випливає, що задача P, представлена існувально квантифікованою кон'юнкцією ствердних літералів, логічно випливає з D тоді й лише тоді, коли P є істинною в M. Семантика мінімальної моделі диз'юнктів Горна є основою для семантики стійких моделей логічних програм.[3]

ПриміткиРедагувати

  1. Як і в резолюційному доведенні теорем, інтуїтивне значення «показати φ» та «припустити ¬φ» є синонімічним (непрямий доказ); вони обидва відповідають одній і тій самій формулі, тобто, ¬φ. Таким чином, інструмент механічного доведення потребує підтримки лише одного набору формул (припущень) замість двох (припущень та (під)цілей).

ВиноскиРедагувати

  1. 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.  (англ.)
  2. 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.  (англ.)
  3. van Emden, M. H.; Kowalski, R. A. (1976). The semantics of predicate logic as a programming language. Journal of the ACM[en] 23 (4): 733–742. doi:10.1145/321978.321991.