6.15. НЕПРОТИВОРЕЧИВОСТЬ И ПОЛНОТА РЕЗОЛЬВЕНЦИИ

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

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

Для того чтобы показать, что принцип резольвенции полон, достаточно показать, что он полон по отношению к вершинам вывода в семантических деревьях.

Обозначим через замкнутое семантическое дерево для невыполнимого множества предложений S, и пусть — такая вершина вывода в что — неблагоприятные вершины, расположенные непосредственно под но ни одно предложение из S не терпит неудачу ни на ни выше Предположим, что предложение из S терпит неудачу на а предложение из S терпит неудачу на Тогда в данном случае полнота принципа резольвенции означает существование резольвенты для скажем (СЛ, терпящей неудачу на вершине или выше нее.

Нетрудно видеть, что такая резольвента существует. В самом деле, пусть — элемент эрбрановской базы, значение истинности которого присваивается как раз под вершиной Пусть для определенности значение будет истинным для и ложным для Хотя ни ни не терпят неудачу на вершине терпит неудачу на — на Рассмотрим сначала предложение Так как оно терпит неудачу на оно должно содержать по крайней мере одно унифицируемое подмножество, скажем для которого будет «общим» константным частным случаем. Пусть а — такой унификатор, что Далее, предложение терпит неудачу на вершине (или выше нее), поскольку при переходе от к мы лишь определили значение истинности для а терпит неудачу на

Аналогично, поскольку предложение терпит неудачу на оно должно содержать унифицируемое подмножество,

скажем для которого будет «общим» константным частным случаем. Пусть такой унификатор, что Предложение также должно терпеть неудачу на вершине (или выше нее).

Теперь унификаторы можно скомбинировать, поскольку переменные в можно считать различными. Обозначим этот комбинированный унификатор через со. Таким образом, так как то имеют резольвенту

где X — наиболее общий унификатор для Так как X — наиболее общий унификатор, то — частный случай предложения частный случай предложения Тогда, так как оба предложения терпят неудачу на вершине вывода (или выше нее), то должны терпеть неудачу и предложения Очевидно, что их объединение — наша резольвента — также терпит неудачу.

Для иллюстрации связи между семантическими деревьями и резольвентными построениями обратимся снова к множеству предложений семантическое дерево которого изображено на рис. 6.2. Мы уже показали, что на вершине 1 терпит неудачу предложение на вершине 2 — предложение а их резольвента терпит неудачу на вершине 3 — вершине вывода. Далее, на семантическом дереве для множества неблагоприятными вершинами будут вершины 3 и 4. На вершине 4 терпит неудачу предложение Построение резольвенты для приводит, разумеется, к пустому предложению (терпящему неудачу на корневой вершине). Итак, доказательство невыполни-, мости заканчивается всего лишь после двух резольвенций.