Дизъюнкт Хорна

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

В математической логике, дизъюнкт Хорна — дизъюнкция литералов с не более чем одним положительным литералом. Дизъюнкты Хорна названы по имени логика Альфреда Хорна, который впервые указал важность таких дизъюнктов в статье 1951 года «On sentences which are true of direct unions of algebras» (Journal of Symbolic Logic 16, 14-21).

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

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

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

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

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

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

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

Резолюция цели с определённым дизъюнктом для получения новой цели является основной для правила вывода в SLD-резолюции, используемого для реализации логического программирования и языка программирования Пролог. В логическом программировании определённый дизъюнкт используется как процедура редукции цели. Например, дизъюнкт Хорна из примера выше работает как процедура

чтобы показать u, показать p, q, \cdots и t.

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

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

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

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

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

Список литературы[править | править исходный текст]

  • Alfred Horn, (1951) «On sentences which are true of direct unions of algebras», Journal of Symbolic Logic, 16, 14-21.

Ссылки[править | править исходный текст]