144
правки
Изменения
→КНФ в форме Хорна
<math> (\neg A \or \neg B \vee \cdots \or \neg C ) \and (A \or \neg B \vee \cdots \or \neg C)</math>
Каждая скобка состоит из,так называемых ''дизъюнктов Хорна''.Дизъюнкт с ровно одним положительным литералом называется ''определенным'' дизъюнктом.Дизъюнкт без положительных литералов иногда называется ''целью'' или ''запросом''(конкретно в логическом программировании).
Дизъюнкты Хорна могут быть пропозициональными формулами, либо формулами первого порядка, в зависимости от того, рассматриваются ли пропозициональные литералы(значением которых может быть логическое высказывание) или литералы первого порядка.
