12.5.2. Исключение моделей при помощи конечных деревьев конфликта

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

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

Аналогично для модели

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

Таким образом, все возможные модели для принадлежат множеству

Если каждая из этих моделей приписывает множеству значение ложь, то оно должно быть невыполнимым. Обобщим этот пример.

Рис. 12.15. Включение рассмотренного конечного дерева конфликта в большее дерево.

Расширим множество атомов, включив в него т. е. переопределим множество

Дерево, изображенное на рис. 12.14, можно включить в большее конечное дерево конфликта (рис. 12.15). Отметим, что оказалось на месте пустого предложения Аналогично переопределяются модели чтобы включить литерал поскольку соответствующий ему узел лежит на путях от всех концевых узлов к корню. Значение ложь для приписанное ему моделями свидетельствовало бы, что множество не может быть выполнимым ни при одной модели, содержащей но ничего не говорило бы о выполнимости при моделях, содержащих

Введем понятие терпит неудачу на узле Множество невыполнимо, если по крайней мере одно предложение принимает значение ложь при всех возможных моделях. Обозначим через модель, содержащую дополнения ко всем литералам, соответствующим узлам, расположенным на пути от корня к узлу а через множество этих литералов. Будем говорить, что предложение С терпит неудачу на узле если содержит все литералы этого предложения. Ясно, что если С терпит неудачу на узле то имеет значение ложь, и 5 невыполнимо для Это иллюстрируется самым правым концевым узлом дерева (рис. 12.15), для которого На этом узле потерпели бы неудачу предложения Заметим также, что должно включать в себя множество литералов, соответствующих любому из узлов, расположенных над Поэтому любое предложение, терпящее неудачу на также будет терпеть неудачу на Например, предложение потерпело бы неудачу на любом из правых концевых узлов (рис. 12.15).

Нас интересует самый высокий узел дерева, в котором может потерпеть неудачу. Узел назовем неблагоприятным для если найдется предложение которое терпит неудачу на но не терпит неудачу ни на одном из узлов, расположенных над В противном случае узел будет называться благоприятным для Предположим теперь, что терпит неудачу на корне, то означает, что невыполнимо при всех моделях, поскольку каждая модель соответствует некоторому узлу под корнем. Поэтому цель семантической процедуры — сделать так, чтобы терпело неудачу на корне. Это осуществляется в резолюции. Назовем узлом вывода, если — благоприятный для узел, но все узлы расположенные под ним, неблагоприятны. Если — узел вывода, то найдется предложение С, литералы которого содержатся в и которое, возможно, не принадлежит но может быть выведено из при помощи резолюции. Для того чтобы убедиться в этом, рассмотрим множество предложений

и соответствующее конечное дерево конфликта (рис. 12.16). Узлы соответствуют множествам

и неблагоприятны для поскольку присваивает значение ложь предложению — предложению Резольвентой будет

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

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

Рис. 12.16. Часть дерева с неблагоприятными узлами и узлом вывода для множества

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

и каждое предложение имеет вид

В (112) и (113) — непересекающиеся множества литералов. Далее, существует такая унификация, что

Из множества скрытого конфликта можно вывести предложение

Как и в гиперрезолюции, не может появиться в предложении и ни один из литералов множества не может оказаться в множестве

Приведем пример. Пусть

Подстановка

дает предложения

При помощи гиперрезолюции выводим предложение

и факторизуем его подстановкой

На рис. 12.17 показано соответствующее семантическое дерево. Сначала каждое предложение из (118) приписывается концевому узлу

Рис. 12.17. Семантическое дерево, построенное резолюцией скрытого конфликта.

Литерал также приписывается узлу Наконец, узлу приписываются предложение и литерал Узел определяется как узел, расположенный непосредственно над Построенное таким способом дерево удовлетворяет определению конечного дерева конфликта. Предложения терпят неудачу на соответствующих

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

Рис. 12.18. (см. скан) Построение семантического дерева резолюцией скрытого конфликта: а — первый этап; — второй этап.

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

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

таково:

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

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

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