8.4. ФОРМЫ ДОКАЗАТЕЛЬСТВА С ОТФИЛЬТРОВЫВАНИЕМ ПРЕДШЕСТВУЮЩИХ ВЕРШИН

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

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

Мы будем говорить, что граф доказательства имеет вид лозы, если каждая его вершина либо является базовым предложением, либо непосредственно следует из базового предложения. (Такой граф будет деревом, но не все деревья имеют вид

лозы. Это видно из примеров гл. 6, где граф рис. 6.3 имеет вид лозы, а граф, изображенный на рис. 6.4, нет.) Если граф опровержения, имеющий вид лозы, существует, то для его построения достаточно резольвент лишь тех пар предложений, из которых хотя бы одно принадлежит 5. Такое ограничение на резольвенции могло бы лечь в основу прекрасной стратегии очищения, если бы только быть уверенным, что для любого невыполнимого множества предложений существует граф опровержения, имеющий вид лозы. К сожалению, стратегия очищения, основанная на графах в виде лозы, не полна; но одна очень похожая на нее стратегия полна.

Чтобы убедиться, что для невыполнимого множества граф в виде лозы существует не всегда, рассмотрим множество

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

Из рис. 8.1 видно, что одна из резольвенций производится между предложениями Далее, в этом графе опровержения предложение предшествует предложению Граф рис. 8.1 служит примером графа с отфильтрованными предшествующими вершинами, или графа в -форме.

Мы будем говорить, что граф опровержения имеет -форму, если каждая вершина графа соответствует одному из следующих предложений:

1) базовому предложению;

2) предложению, непосредственно следующему за базовым;

3) предложению, непосредственно следующему за двумя небазовыми предложениями Л и В, из которых В предшествует А (отсюда термин — отфильтровывание предшествующих вершин).

Граф в виде лозы представляет собой частный случай графа в -форме: каждая из его вершин соответствует либо

предложению 1), либо предложению 2). Базовое предложение С в графе, имеющем -форму, называется концевой вершиной, если любая другая вершина дерева либо является базовым предложением, либо следует за С.

Рис. 8.1. (см. скан) Граф опровержения.

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

Теорема 8.1. Пусть -граф опровержения для невыполнимого множества предложений, некоторое предложение из появляющееся в Тогда для существует граф опровержения в -форме, для которого С служит концевой вершиной.

Для многих графов частный случай опровержения в -форме, имеющий вид лозы, существует. Дерево, изображенное на рис. 6.4, не имеет -формы, однако дерево опровержения для того же самого множества предложений с в качестве концевой вершины, показанное на рис. 8.2, имеет вид лозы.

Рис. 8.2. (см. скан) Дерево опровержения в виде лозы.

Читатель может попытаться построить для этого множества предложений, но с иными концевыми вершинами, другие графы в -форме.

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

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

Рис. 8.3. Поиск опровержения с использованием -стратегии.

К могут содержаться предложения, возникающие при отрицании теоремы, которую предстоит доказать). Тогда критерий, которому должна удовлетворять пара предложений для того, чтобы ее можно было подвергнуть резольвенции в отношении -стратегии, таков:

(см. скан)

Обозначим через объединение множества и множества всех резольвент всех пар из допускаемых -стратегией. Положим, как обычно,

Согласно теореме 8.1, если множество неудовлетворимо, то найдется такое что

На рис. 8.3 показан результат применения -стратегии к простому неудовлетворимому множеству предложений. (В этом

примере На уровнях 1 и 2 выполнялись все допустимые резольвенции до тех пор, пока не было выведено на уровне 3 пустое предложение. Образованный такой процедурой граф в -форме отмечен жирными линиями. Он оказался лозой.