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

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

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

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

$L_{1}$ $L_{1}$
$\neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n}$ $\neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n}$
$P\vee \neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n}$ $P\vee \neg L_{1}\vee \neg L_{2}\vee \dots \vee \neg L_{n}$

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

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

\neg p\lor \neg q\vee \cdots \vee \neg t\vee u

\neg p\lor \neg q\vee \cdots \vee \neg t\vee u

.

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

(p\wedge q\wedge \cdots \wedge t)\rightarrow u

(p \wedge q \wedge \cdots \wedge t) \rightarrow u

или :

(p\rightarrow u)\vee (q\rightarrow u)\vee \cdots \vee (t\rightarrow u)

(p\rightarrow u)\vee (q\rightarrow u)\vee \cdots \vee (t\rightarrow u)

.

Приложения

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

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

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

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

u\leftarrow (p\land q\land \cdots \land t)

u\leftarrow (p\land q\land \cdots \land t)

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


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

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