6.14. ПРИНЦИП РЕЗОЛЬВЕНЦИИ

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

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

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

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

Рис. 6.3. Граф опровержения для невыполнимого множества

Этот результат позволяет пользоваться в процессе опровержения одним только правилом резольвенции без явной ссылки на семантические деревья. Пусть -объединение множества 5 с множеством всех резольвент всех пар его предложений. Пусть обозначает Если множество 5 неудовлетворимо, то мы гарантированы, что при некотором конечном (называемом уровнем, или глубиной, опровержения) в будет пустое предложение. Так как множество при любом конечно, если конечно 5, то эта простая стратегия нахождения опровержения является конечным (хотя, быть может, долгим) процессом.

Образование множеств соответствует полному перебору при поиске опровержения. В гл. 8 мы обсудим различные стратегии поиска, более эффективные, чем эта простая стратегия.

Опровержения, использующие резольвенции (иногда называемые доказательствами с помощью резольвенций), можно

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

Рис. 6.4. Граф опровержения для невыполнимого множества

Корнем графа опровержения с помощью резольвенции (эти графы обычно изображаются с корнем, расположенным внизу рисунка) служит пустое предложение (обозначаемое символом

На рис. 6.3 приведен пример графа опровержения для множества неудовлетворимых предложений. Здесь для опровержения необходимы 3 резольвенции. Другой пример приведен на рис. 6.4. (Заметим, что на рис. 6.4 предложение используется на графе дважды. Иногда эти графы изображают в виде деревьев, повторяя поддеревья, появляющиеся более одного раза.)