Главная arrow Знания и рассуждения arrow Конъюнктивная нормальная форма
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Конъюнктивная нормальная форма Печать

Как было описано выше, правило резолюции применяется только к дизъюнкциям литералов, поэтому на первый взгляд оно распространяется только на базы знаний и запросы, состоящие из таких дизъюнкций. На каком же основании мы утверждаем, что это правило может служить основой процедуры полного логического вывода для всей пропозициональной логики? Ответ на этот вопрос состоит в том, что каждое высказывание пропозициональной логики логически эквивалентно конъюнкции дизъюнкций литералов.

Любое высказывание, представленное как конъюнкция дизъюнкций литералов, называется высказыванием, находящимся в конъюнктивной нормальной форме, или CNF (Conjunctive Normal Form). Кроме того, ниже будет показано, что целесообразно определить также ограниченное семейство высказываний в конъюнктивной нормальной форме, называемое высказываниями в форме k-CNF. Высказывание в форме k-CNF имеет точно 7с литералов в расчете на каждое выражение:

(l1,1 v … v l1,k) ^ …^ (ln,1 v … v ln,k)

Как оказалось, любое высказывание может быть преобразовано в высказывание в форме 3-CNF, которое имеет эквивалентное множество моделей. Вместо доказательства этих утверждений опишем простую процедуру преобразования. Проиллюстрируем эту процедуру, преобразовав высказывание R2, или B1,1 <=> (P1,2 v P2,1), в форму CNF. Ниже описаны соответствующие этапы.

  1. Устранить связку <=>, заменив высказывание α <=> β высказыванием (α => β) ^ (β <=> α): (B1,1 => (P1,2 v P2,1)) ^ ((P1,2 v P2,1) => B1,1)
  2. Устранить связку =>, заменив высказывание α => β высказыванием ¬α v β: (¬B1,1 v P1,2 v P2,1) ^ (¬(P1,2 v P2,1) v B1,1)
  3. Конъюнктивная нормальная форма требует, чтобы связка ¬ появлялась только перед литералами, поэтому, как принято называть эту операцию, "введем связку ¬ внутрь выражения", повторяя операцию применения следующих эквивалентностей из листинга
  4. В результате получено высказывание, содержащее вложенные связки ^ и v, которые применяются к литералам. Используем закон дистрибутивности, приведенный в листинге, распределяя связки v по связкам л везде, где это возможно.

Теперь первоначальное высказывание представлено в форме CNF, как конъюнкция трех выражений. Это высказывание стало более сложным для чтения, но зато его можно использовать в качестве входных данных для процедуры резолюции.