Intel_Nils (526801), страница 38

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 38)

НЕБЛАГОПРИЯТНЫЕ ВЕРШИНЫ Наиболее важным фактом, связанным с семантическими деревьями, является возможность установить, не просматривая дерево неограниченно далеко вниз, что определенные интерпретации не удовлетворяют некоторому множеству предложений. В нашем примере на рис. 6.1 мы приписали атому Р(а), расположенному слева непосредственно под корневой вершиной, значение Т. Сразу же видно, что ни одна из возможных восьми интерпретаций, в которых Р(а) имеет значение Т, не удовлетворяет 5; чтобы удовлетворять 5, значением атома Р(а) должно быть Р.

Итак, нет необходимости просматривать дальше левую часть этого дерева. Пометим черными кружочками те вершины дерева на рис. 6.1, где впервсче было установлено, что эта интерпретация не может удовлетворять 5. Такие вершины будем называть неблагоприятными. Разумеется, если множество предложений неудовлетворимо, то, даже когда эрбрановская база бесконечна, каждая возможная интерпретация в конце концов должна оборваться на'какой-то неблагоприятной вершине. В самом деле, если бы хотя бы одна интерпретация не обрывалась на неблагоприятной вершине, то мы могли бы сколь угодно долго двигаться по этому пути, т, е. существовала бы интерпретация, удовлетворяющая множеству предложений, что противоречит неудовлетворимости этого множества. Семантическое дерево для множества предложений 5, все пути которого обрываются на неблагоприятных вершинах, называется замкнутым для 5.

Таким образом, мы получили ключевой результат, на котором основаны наши методы проверки выполнения свойства неудовлетворимости. Семантическое дерево для неудовлетворимого множества предложений 5 'в исчислении прсдикатов 190 Г . б. Доказательство теорем 'в р(Г(и)1 т)(Г(а 8 1 е ево длп иев евыполнимого множества Р и с 6.2 Замкнутое семантическое дер (- Р (к) Ч () (к), Р (( (у)), Я () (у))) замкнуто ля и с д 5 одержит конечное число вершин, располо- ами ' женньск над неблагоприятньсми вершинами ). знаменитой тео-. ') Можио показать, что э это утверждение эквивалентно реме Эрбраиа (1939). 6.1Е Вершили завода 191 На рис. 6.2 изображена часть семантического дерева для неудовлетворимого множества предложений Я=( Р(х) ~/ Я(х), Р(~(у)), Я(1 (у))).

Универсумом Эрбрана здесь будет множество Н (5) = (а, 1 (а), 1 (1 (а)), ) (1 () (а))), ...), а эрбрановскую базу можно упорядочить так: (Р (а), Я (а), Р () (а)), (г (1 (а)), Р () (1 (а))), ...). Хотя эрбрановская база бесконечна, так что любая полная интерпретация соответствует бесконечному пути по этому семантическому дереву, мы знаем, что, в случае когда Я неудовлетворимо, семантическое дерево замкнуто неблагоприятными вершинами.

На рис. 6.2 показана часть семантического дерева, расположенная выше неблагоприятных вершин и включающая их. На практике редко удается установить невыполнимость множества предложений построением семантического дерева. В последнее время на основе принципа резольвенций были разработаны практически приемлемые процедуры установления неудовлетворимости. В следующих разделах мы объясним суть этого принципа, воспользовавшись уже описанными представлениями, связанными с семантическими деревьями. 6.11. ВЕРШИНЫ ВЫВОДА Рассмотрим снова пример, приведенный на рис. 6.2. Каждая из неблагоприятных вершин этого дерева обладает тем свойством, что любое завершение части интерпретации, заданной вплоть до этой вершины, не удовлетворяет какому-то из предложений нашего множества. Ниже неблагоприятной вершины, отмеченной на рис.'6.2 цифрой 1, идут интерпретации, заведомо не удовлетворяющие предложению -Р(х) У 1г(х).

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

На рис. 6.2 вершина, отмеченная цифрой 3, является вершиной вывода, поскольку можно вывести новое предложение, логически следующее из предложений -Р(х) ~/ Я(х) и Я(1(у)), которые терпят неудачу на неблагоприятных вершинах, идущих сразу за ней. Кроме того, это новое предложение само терпит неудачу на вершине вывода или 192 Гл. 6. Доказательство теорем в исчислеиии оредикатов выше иее. (Конечно, этого нового предложения нет в 5, поскольку иначе вершина 3 или какая-нибудь вершина, ей предшествующая, была бы неблагоприятной.) Какое же предположение можно вывести из предложений Р(х)'l Я(х) и -Я(1(у))? Пусть 1 — произвольная интерпретация, удовлетворяющая обоим предложениям -Р(х) ~Г (1(х) и й1()(у)).

Так как интерпретация 1 удовлетворяет предложению -Р(х) ~l Я(к), она должна также удовлетворять любому предложению, получающемуся из него подстаиовкой другого выражения вместо х. В частности, 1 должна удовлетворять предложению -Р(1(у)) ~l с1(1(у)). Но литерал с1(1(у)) не может удовлетворяться этой интерпретацией, поскольку мы предположили, что интерпретацией 1 удовлетворяется его отрицание -(1(1(у)). Следовательно, если интерпретация 1 удовлетворяет предложению Р(Г'(у)) Ч Я(1(у)), то только потому, что 1 удовлетворяет предложению Р(1"(д)). Тогда из данных двух предложений можно вывести предложение Р(1(у)).

Кроме того, заметим, что приписывание значений истинности дополнительным литералам С1(1(а)) и -ь1(1(а)) ие изменяет означивания выведенного предложения Р(1(у)). Выведеиное предложение уже потерпело неудачу на вершине вывода (вершине 3). Выведенное предложение Р(1(у) ) называется Рвзольвенгой двух предложений — Р(х) ~l Я(х) и ьг(1(у)). Если у двух предложений есть резольвеиты (их может быть более одной), то процесс их получения зависит от возможности делать такие подстановки термов вместо переменных, чтобы предложения, возникающие в результате подстановок, содержали дополнительные литералы.

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

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

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

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

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

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

УНИФИКАЦИЯ Теперь мы должны обсудить процесс, называемый унификацией, являющийся основным в формальных преобразованиях, выполняемых при нахождении резольвент. Термы литерала могут быть переменными буквами, константными буквами и выражениями, состоящими из функциональных букв и термов. (Подстановочный) частный случай литерала получается при подстановке в литералы термов вместо переменных. Например, для литерала Р(х, ~(у), Ь) частными случаями будут Р (г> ~ (гс)> Ь), Р (х. ((а), Ь), Р(й(х), )'(а), Ь), Р(с, ) (а), Ь). »94 Гл 6. Доказательство теорем в иввввлвнви орвдикогов Первый частный случай называется алфавитным вариантолв исходного литерала, поскольку здесь вместо переменных, входящих в Р(х,г(у),Ь), подставлены лишь другие переменные. Последний из перечисленных четырех частных случаев называется константным частным случаем, или атомом, так как ни в одном нз термов этого литерала нет переменных.

В общем случае любую подстановку можно представить в виде множества упорядоченных пар О = (((ь о,), (»м оз), ... ..., (1, о„)). Пара (Ги о») означает, что повсюду переменная о» заменяется термам Г». Существенно, что переменная в каждом ее вхождении заменяется одним и тем же термам, т. е. из» ~1 следует, что о» Ф он», 1 = 1, ..., и. Для получения частных случаев литерала Р(х,г(у),Ь) были использованы четыре подстановки а=((г, х), (гс, у)), 6=((а у)) у = ((у (г), х), (а, у)), 6 = ((с, х), (а, у)). Обозначим через Рв частный случай литерала Р, получающийся при использовании подстановки О. Например, Р(з,((гс), Ь) = Р(х,»'(у), Ь)„.

Композицией ай двух подстаиовок а и р называется результат применения (1 к термам подстановки а с последующим добавлением любых пар из р, содержащих переменные, не входящие в число переменных из а. Например, (у (х, у), а)) Ца, х), (Ь, у), (с, го), (»(, х)) = = ((д (а, Ь), х), (а, х), (Ь, у), (с„гс).) Можно показать, что применение к литералу Р. последовательно подстановок а и р дает тот же результат, что и применение к Р подстановки ай, т. е. (Рв)а = Рвы Можно также показать, что композиция подстановок ассоциативна: (ар) у = а (Оу).

Характеристики

Список файлов книги