Диз'юнкт Горна

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

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

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

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

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

відповідає

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

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

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

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

Предикатні диз'юнкти Горна становлять інтерес у теорії складності обчислень. Задача знаходження таких присвоювань значень істинності, щоби зробити кон'юнкцію предикатних диз'юнктів Горна істинною, є P-повною, розв'язуваною за лінійний час,[2] й іноді званою задовільністю за Горном (англ. 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.

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

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

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