Далее, правила 2 и 4 дают
(
Трижды применив правило 1, получаем
(
И наконец, после применения правила 2 получаем искомую конъюнктивную нормальную форму
(
состоящую из четырех дизъюнктов. Теперь можно приступить к резолюционному процессу
.
Элементарный шаг резолюции выполняется всегда, когда имеется два дизъюнкта, в одном из которых встретилось элементарное утверждение
Шаг резолюции порождает третий дизъюнкт:
Нетрудно показать, что этот дизъюнкт логически следует из тех двух дизъюнктов, из которых он получен. Таким образом, добавив выражение (
которые явно противоречат друг другу.
Рис. 16. 6. Доказательство теоремы (
резолюции. Верхняя строка - отрицание теоремы в конъюнктивной
нормальной форме. Пустой дизъюнкт внизу сигнализирует, что
отрицание теоремы противоречиво.
На рис. 16.6 показан процесс применения резолюций, начинающийся с отрицания нашей предполагаемой теоремы и заканчивающийся пустым дизъюнктом.
На рис. 16.7 мы видим, как резолюционный процесс можно сформулировать в форме программы, управляемой образцами. Программа работает с дизъюнктами, записанными в базе данных. В терминах образцов принцип резолюции формулируется следующим образом:
существуют два таких дизъюнкта
а
удалить
из
