Хорновский дизъюнкт

Хорновский дизъюнкт — дизъюнктивный одночлен с не более чем одним положительным литералом. Изучены Шаблон:Нп2 в 1951 году в связи с их важной ролью в теории моделей и универсальной алгебре. Впоследствии стали основой для языка логического программирования Пролог, в котором программа являются непосредственно набором хорновских дизъюнктов, а также нашли важные приложения в конструктивной логике и теории сложности вычислений.

Конструкция и определения

Для положительных литералов $P,L_i,i\in \{1,2,\dots n\}$ хорновские дизъюнкты могут иметь один из следующих видов:

1. $L_1$
2. $\mathrm{\neg }{L}_1\vee \mathrm{\neg }{L}_2\vee \dots \vee \mathrm{\neg }{L}_n$
3. $P\vee \mathrm{\neg }{L}_1\vee \mathrm{\neg }{L}_2\vee \dots \vee \mathrm{\neg }{L}_n$

Дизъюнкт Хорна с ровно одним положительным литералом есть определённый дизъюнкт; в универсальной алгебре определённые дизъюнкты являются квазитождествами. Дизъюнкт Хорна без положительных литералов иногда называется целью или запросом, в частности в логическом программировании. Формула Хорна — конъюнкция дизъюнктов Хорна, то есть формула в конъюнктивной нормальной форме, все дизъюнкты которой являются хорновскими. Двойственным хорновским дизъюнктом называют дизъюнкцию с не более чем одним отрицательным литералом.

Пример (определённого) дизъюнкта Хорна:

$\mathrm{\neg }p\vee \mathrm{\neg }q\vee \cdots \vee \mathrm{\neg }t\vee u$.

Эта формула может быть преобразована в эквивалентную формулу с импликацией:

$(p\wedge q\wedge \cdots \wedge t)\to u$

или:

$(p\to u)\vee (q\to u)\vee \cdots \vee (t\to u)$.

Приложения

Хорновские дизъюнкты могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы или литералы первого порядка.

Дизъюнкты Хорна связаны с доказательством теорем через резолюции первого порядка, так как резолюция двух хорновских дизъюнктов является хорновским дизъюнктом. Кроме того, резолюция цели и определённого дизъюнкта также является хорновским дизъюнктом. В автоматическом доказательстве теорем, это может давать большую эффективность в доказательстве теоремы, представленной в виде цели.

Резолюция цели с определённым дизъюнктом для получения новой цели является основной для правила вывода в SLD-резолюции, используемого для реализации логического программирования и языка программирования Пролог. В логическом программировании определённый дизъюнкт используется как процедура редукции цели. Например, дизъюнкт $\mathrm{\neg }p\vee \mathrm{\neg }q\vee \cdots \vee \mathrm{\neg }t\vee u$ из примера выше работает как процедура: «чтобы показать $u$, показать $p$, $q$, $\cdots$ и $t$».

Чтобы подчеркнуть это обратное применение дизъюнкта, часто используется оператор $\leftarrow$:

$u\leftarrow (p\wedge q\wedge \cdots \wedge t)$

На Прологе это записывается в виде:

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

Пропозициональные дизъюнкты Хорна также представляют интерес для теории сложности вычислений, где задача HORNSAT поиска множества истинностных значений, выполняющих конъюнкцию дизъюнктов Хорна, является P-полной. Это вариант из класса P для SAT — важнейшей NP-полной задачи. Задача выполнимости дизъюнктов Хорна первого порядка не разрешима.

Литература

• Шаблон:Статья

Ссылки

• Шаблон:MathWorld