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

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

В математичній логіці та логічному програмуванні диз'ю́нкт Го́рна (англ. 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 (PDF). Journal of the ACM[en]. 23 (4): 733—742. doi:10.1145/321978.321991. Архів оригіналу (PDF) за 3 березня 2016. Процитовано 31 січня 2016.