Русская Википедия:Хорновский дизъюнкт
Хорновский дизъюнкт — дизъюнктивный одночлен с не более чем одним положительным литералом[1]. Изучены Шаблон:Нп2 в 1951 году в связи с их важной ролью в теории моделей и универсальной алгебре. Впоследствии стали основой для языка логического программирования Пролог, в котором программа являются непосредственно набором хорновских дизъюнктов, а также нашли важные приложения в конструктивной логике и теории сложности вычислений.
Конструкция и определения
Для положительных литералов <math>P, L_i, i \in \{1, 2,\dots n\}</math> хорновские дизъюнкты могут иметь один из следующих видов[1]:
- <math>L_1</math>
- <math>\neg L_1 \vee \neg L_2 \vee \dots \vee \neg L_n</math>
- <math>P \vee \neg L_1 \vee \neg L_2 \vee \dots \vee \neg L_n</math>
Дизъюнкт Хорна с ровно одним положительным литералом есть определённый дизъюнкт; в универсальной алгебре определённые дизъюнкты являются квазитождествами. Дизъюнкт Хорна без положительных литералов иногда называется целью или запросом, в частности в логическом программировании. Формула Хорна — конъюнкция дизъюнктов Хорна, то есть формула в конъюнктивной нормальной форме, все дизъюнкты которой являются хорновскими. Двойственным хорновским дизъюнктом называют дизъюнкцию с не более чем одним отрицательным литералом.
Пример (определённого) дизъюнкта Хорна:
- <math>\neg p \lor \neg q \vee \cdots \vee \neg t \vee u</math>.
Эта формула может быть преобразована в эквивалентную формулу с импликацией[1]:
- <math>(p \wedge q \wedge \cdots \wedge t) \rightarrow u</math>
или[1]:
- <math>(p \rightarrow u) \vee (q \rightarrow u) \vee \cdots \vee (t \rightarrow u)</math>.
Приложения
Хорновские дизъюнкты могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы или литералы первого порядка.
Дизъюнкты Хорна связаны с доказательством теорем через резолюции первого порядка, так как резолюция двух хорновских дизъюнктов является хорновским дизъюнктом. Кроме того, резолюция цели и определённого дизъюнкта также является хорновским дизъюнктом. В автоматическом доказательстве теорем, это может давать большую эффективность в доказательстве теоремы, представленной в виде цели.
Резолюция цели с определённым дизъюнктом для получения новой цели является основной для правила вывода в SLD-резолюции, используемого для реализации логического программирования и языка программирования Пролог. В логическом программировании определённый дизъюнкт используется как процедура редукции цели. Например, дизъюнкт <math>\neg p \lor \neg q \vee \cdots \vee \neg t \vee u</math> из примера выше работает как процедура: «чтобы показать <math>u</math>, показать <math>p</math>, <math>q</math>, <math>\cdots</math> и <math>t</math>».
Чтобы подчеркнуть это обратное применение дизъюнкта, часто используется оператор <math>\leftarrow</math>:
- <math>u \leftarrow (p \land q \land \cdots \land t)</math>
На Прологе это записывается в виде:
u :- p, q, ..., t.
Пропозициональные дизъюнкты Хорна также представляют интерес для теории сложности вычислений, где задача HORNSAT поиска множества истинностных значений, выполняющих конъюнкцию дизъюнктов Хорна, является P-полной. Это вариант из класса P для SAT — важнейшей NP-полной задачи. Задача выполнимости дизъюнктов Хорна первого порядка не разрешима.
Примечания
Литература
Ссылки
- ↑ 1,0 1,1 1,2 1,3 Шаблон:Книга
