Вместо доказательства этих утверждений опишем простую процедуру преобразования. Проиллюстрируем эту процедуру, преобразовав высказывание R2, или, в форму CNF. Ниже описаны соответствующие этапы.

1.    Устранить связку заменив высказывание высказыванием

2.    Устранить связкузаменив высказывание высказыванием

3.     Конъюнктивная нормальная форма требует, чтобы связкапоявлялась только перед литералами, поэтому, как принято называть эту операцию, "введем связкувнутрь выражения", повторяя операцию применения следующих эквивалентностей из листинга 7.4:

В данном примере требуется применение только одного, последнего правила:

4.    В результате получено высказывание, содержащее вложенные связки л и ν, которые применяются к литералам. Используем закон дистрибутивности, приведенный в листинге 7.4, распределяя связки ν по связкам л везде, где это возможно.

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

Алгоритм резолюции

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