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

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

(l_1,1 v … v l_1,k) ^ …^ (l_n,1 v … v l_n,k)

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

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

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