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

Мы покажем, что резолюция обеспечивает полноту опровержения (refutation completeness), а это означает, что если множество высказываний является невыполнимым, то резолюция всегда позволяет прийти к противоречию. Резолюцию нельзя использовать для выработки всех логических следствий из множества высказываний, но она может применяться для подтверждения того, что данное конкретное высказывание следует из множества высказываний. Поэтому резолюция может служить для поиска всех ответов на данный конкретный вопрос с помощью метода отрицаемой цели, который был описан выше в настоящей главе.

Примем как истинное такое утверждение, что любое высказывание в логике первого порядка (без использования равенства) может быть перезаписано в виде множества выражений в форме CNF. Это можно доказать по индукции на основе анализа формы высказывания, применяя в качестве базового случая атомарные высказывания [336]. Поэтому наша цель состоит в том, чтобы доказать следующее: если S— невыполнимое множество выражений, то применение к S конечного количества этапов резолюции приведет к противоречию.

Схема нашего доказательства повторяет первоначальное доказательство, приведенное Робинсоном, с некоторыми упрощениями, которые были внесены Гене-зеретом и Нильссоном [537]. Основная структура этого доказательства показана на рис. 9.9; оно осуществляется, как описано ниже.

Рис. 9.9. Структура доказательства полноты резолюции

1. Вначале отметим, что если множество выражений S невыполнимо, то существует такое конкретное множество базовых экземпляров выражений S, что это множество также невыполнимо (теорема Эрбрана).

2.    Затем прибегнем к базовой теореме резолюции (ground resolution theorem), приведенной в главе 7, в которой утверждается, что пропозициональная резолюция является полной для базовых высказываний.

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