6.10. НЕБЛАГОПРИЯТНЫЕ ВЕРШИНЫ

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

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

Рис. 6.2. (см. скан) Замкнутое семантическое дерево для невыполнимого множества

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

На рис. 6.2 изображена часть семантического дерева для неудовлетворимого множества предложений

Универсумом Эрбрана здесь будет множество

а эрбрановскую базу можно упорядочить так:

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

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