6.11. ВЕРШИНЫ ВЫВОДА

Рассмотрим снова пример, приведенный на рис. 6.2. Каждая из неблагоприятных вершин этого дерева обладает тем свойством, что любое завершение части интерпретации, заданной вплоть до этой вершины, не удовлетворяет какому-то из предложений нашего множества. Ниже неблагоприятной вершины, отмеченной на рис. 6.2 цифрой 1, идут интерпретации, заведомо не удовлетворяющие предложению Ниже неблагоприятной вершины, отмеченной цифрой 2, идут интерпретации, заведомо не удовлетворяющие предложению Мы будем называть вершину 1 неблагоприятной для а вершину 2 неблагоприятной для Мы будем также говорить, что предложения терпят неудачу на вершинах 1 и 2 соответственно.

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

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

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

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

Любое замкнутое семантическое дерево для неудовлетворимого множества 5 непустых предложений должно иметь по крайней мере одну вершину вывода, так как иначе у каждой из вершин была бы по крайней мере одна дочерняя вершина, не являющаяся неблагоприятной, что противоречит предполагаемой замкнутости дерева. Пусть мы располагаем процессом вывода резольвенты С из двух предложений, терпящих неудачу ниже такой вершины вывода что С терпит неудачу на вершине или выше нее. Тогда можно образовать новое (все еще) неудовлетворимое множество предложений Семантическое дерево для 5 должно быть семантическим деревом для но только для вершина (или некоторая вершина над ней) будет неблагоприятной. Ясно, что число вершин, расположенных выше неблагоприятных вершин, в дереве для строго меньше, чем в дереве для . И тем не менее дерево для должно иметь по крайней мере одну вершину вывода,

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

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