формула:
(
Смысл этой формулы таков: если из
Прежде чем начать применять процесс резолюции ('резолюционный процесс'), необходимо представить
отрицание нашей формулы в наиболее приспособленной для этого форме. Такой формой является
, имеющая вид
(
& (
Здесь
или их отрицания. Конъюнктивная нормальная форма есть конъюнкция членов, называемых
, например (
v
v ...) - это дизъюнкт.
Любую пропозициональную формулу нетрудно преобразовать в такую форму. В нашем случае это делается следующим образом. У нас есть исходная формула
(
Ее отрицание имеет вид
~ ( (
Для преобразования этой формулы в конъюнктивную нормальную форму можно использовать следующие известные правила:
(1)
(2)
(3)
(4)
Применяя правило 1, получаем
~ ( ~ ( (
