12.1. Принцип резолюции

12.1.0. Введение

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

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

12.1.1. Резолюция для основного случая

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

Их конъюнкция имплицирует третье предложение

Будем говорить, что выводится из Предложение будет называться резольвентой предложений будут называться родительскими предложениями для Если бы предложение использовалось в последующей резолюции, скажем, при получении предложения то были бы предками для потомком предложений Для более общего определения будем считать предложения и такими множествами литералов, что если С, содержит литерал то содержит литерал Предложение являющееся резольвентой для , имеет вид

Множество предложений выполнимо, если существует модель, для которой конъюнкция предложений из истинна. Далее, если выполнимо, то любое множество состоящее из и предложений, выведенных из резолюцией, должно также быть выполнимым. Поэтому если невыполнимо, то должно было быть также невыполнимым. Конечно, это просто переформулировка применительно к резолюции того, о чем уже говорилось. Резолюция предоставляет легкий способ показать, что определенные множества невыполнимы для любой модели. Поскольку значение истинности предложения является дизъюнкцией значений истинности его литералов, оно не должно измениться, если добавить к предложению „всегда ложное" высказывание Поэтому любое предложение можно заменить на Множество высказываний построенное так из всегда имеет те же значения истинности, что и Предположим теперь, что после одного или нескольких „раундов» расширения множества при помощи резолюции получаются два предложения, которые (если

не считать являются одиночными литералами, дополнительными относительно друг друга. Резольвента этих двух предложений имеет вид

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

Для завершения доказательства непротиворечивости принципа резолюции нужно показать, что если невыполнимо, то всегда можно получить при помощи резолюции. Для этого применим синтаксическую процедуру, разработанную Андерсоном и Бледсоу (1970). Доказательство проводится индукцией по числу „лишних" литералов:

Например, высказывание

содержит три предложения и

Интересно отметить, что описывает структуру рассматриваемого высказывания и не зависит от присваивания его элементам значений истинности. Таким образом, доказательство Андерсона и Бледсоу служит примером синтаксического доказательства, при помощи которого показывается, что некоторое утверждение верно для всех возможных структур множества Его можно противопоставить семантическому доказательству, в котором показывается, что некоторое утверждение относительно верно для всех его возможных моделей. Наши предыдущие рассуждения носили, конечно, семантический характер.

Теорема. Если — невыполнимое множество основных предложений, то при помощи резолюции из можно вывести

Доказательство. Сначала предположим, что Тогда либо каждое предложение является одночленом (так что число

литералов равно числу предложений), либо одно предложение содержит два литерала, а другое пусто (так что „лишний" литерал компенсируется). Если содержит то теорема очевидна, поскольку ( ) „выводится", будучи одной из аксиом. Если все предложения в одночлены, то имеет вид

Другими словами, каждое предложение содержит точно один атом и каждое отдельное предложение истинно при любом присваивании, при котором его единственный литерал принимает значение истина. Поскольку по предположению множество невыполнимо, каждое полное присваивание должно приводить к значению ложь для Это означает, что в должна быть по крайней мере одна пара предложений, литералы которых дополняют друг друга так, что любое присваивание приводит к значению истина для одного и ложь для другого, гарантируя, таким образом, что для любой модели множество всегда содержит по крайней мере одно невыполнимое предложение. (В высказывании (20) эту роль играют второе и третье предложения). Если разрешить друг с другом такие два предложения, то получится например

Итак, теорема верна для Базис индукции доказан.

Для проведения индукции предположим, что теорема справедлива для множество предложений невыполнимо и Если уже содержит то теорема тривиальна. Предположим, что это не так. Так как то в по крайней мере одно предложение С содержит более одного литерала. Пусть таким предложением будет где — литерал и Запишем множество в виде

тогда определится как

Из можно получить два множества, расщепив С на компоненты:

Поскольку в то же число предложений, что и в содержит на один литерал меньше и содержит по крайней мере на один литерал меньше, то

так что по предположению при невыполнимости и из них можно получить Можно показать, что они должны быть невыполнимыми.

Пусть М — множество таких моделей, что для любого присваивания предложение С истинно. (Такое множество всегда существует.) Поскольку множество по предположению невыполнимо, то оно должно быть невыполнимо и для любой модели из М. Поэтому любая модель должна присваивать значение ложь некоторому предложению . В частности, все присваивания, для которых А или истинны, принадлежат М, и каждое из них должно придавать значение ложь некоторому предложению . С другой стороны, любая модель, не принадлежащая М, должна присваивать значение ложь как так и поскольку в противном случае С не было бы ложным. Это означает, что любое присваивание, принадлежит оно М или нет, должно присваивать значение ложь поскольку любое присваивание из М приводит к значению ложь для а любое присваивание не из М приводит к значению ложь как для так и для Таким образом можно вывести резолюцией или из или из

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

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

Теперь для вывода можно к как к подмножеству множества применить шагов резолюции, приведших к (25б). Теорема доказана.

Пример. Проиллюстрируем резолюцию простым, уже упоминавшимся, примером с неравенствами. Напомним аксиомы. (Их интерпретация, несущественная здесь, дана в предыдущем разделе.)

Разрешим сначала

Затем разрешим

пришли к противоречию.

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

(i) Упорядочить предложения от 1 до

(ii) Положить

(iii) Провести все возможные резолюции предложения с предложениями добавляя выведенные предложения в качестве предложений

(iv) Увеличить на 1, положить и перейти к шагу (iii). Этот процесс продолжают до тех пор, пока не выводят пустое предложение. Ясно, что этот алгоритм даст все резолюции, которые можно получить, включая многие совсем лишние. Для приведенного выше очень простого примера первые три резолюции таковы:

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