Intel_Nils, страница 49

Граф опровержеиия, удовлетворяющий модельной стратегии, в которой Я (х), Р (хД используется для определения модели. опровержения. Приведем без доказательства теорему, на основе которой можно построить еще одну стратегию очищения, связанную с моделями. Теорема 8.2. Пусть 5 — неудовлетворимое множество предложений и М вЂ” модель, заданная на его эрбрановской базе. Тогда существует такой граф опровержения для о, что каждая его вершина либо является предложением из о, либо имеет 846 Гл. д. Метода поиска докавательства в исчислении кредикатов в качестве одной из непосредственно предшествуюисих ей вершин предложение, которое не удовлетворяется моделью М, Стратегию, основанную на теореме 8.2, называют модельной стратегией.

Критерий, которому должна удовлетворять пара предложений (А,В) для того, чтобы ее можно было подвергнуть резольвенции в 'отношении модельной стратегии, таков, что по крайней мере одно из предложений пары (А, В) не удовлетворяется моделью. Мы будем обозначать через,Ям(5) объединение множества 5 и множества всех резольвент всех пар из 5, допускаемых модельной стпатегией. Положим Ям (Ф) Ям (Ф) Ям (Ям (~))' Согласно теореме 8.2, если множество 5 неудовлетворимо, то найдется такое и, что п1! еп Я" (5). На рис. 8А изображен граф опровержения для множества невыполнимых предложений, приведенного на рис. 8.1.

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

По теореме 8.2 существует такое опровержение, что для пар предложений, каждое из которых принадлежит 3 — К, ни одна из резольвенцнй не выполняется. Таким образом, модельная стратегия является усилением стратегии поддерживающего множества. 8.8. РгОПРОВЕРЖЕПИЯ Назовем предложение положительньем, если у всех его литералов нет знака отрицания.

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

Тогда предложенце в рамках этой модели принимает значение истинности Р тогда и только тогда, когда оно положительно. Если непротиворечивым образом переименовать литералы, в о, то получим просто вариант Роопровержения. Если в нашем примере на рис. 8.4 заменить 1г(х) на Р(х), а Р(х) на Т(х), то опровержение станет Р;опровержением для переименованного множества предложений. Р,-опровержение и его варианты важны, поскольку здесь легко реализовать проверку выполнения условия проведения резольвенции. 8.9.

КОМБИНИРОВАННЫЕ СТРАТЕГИИ Естественно возникает вопрос: приводит ли к полной стратегии комбинирование ограничений на резольвенции, определяемых АР-стратегией и модельной стратегией? Безусловно, такое комбинирование могло бы существенно уменьшить число требуемых резольвенций. К сожалению, эта комбинация не полна: не существует опровержения для невыполнимого множества ( 1((а), 1ч (а) Ч (г(а), Р(а) ~/1ч (а), Р(а) ~l Сг(а)) в АГ-форме, которое уловлетворяло бы также модельному ограничению с моделью (Р(а), чг(а), й(а)). Тем не менее, объединяя этн две стратегии эвристически, часто можно получить достаточно эффективный поиск опровержения.

8дв. СТРАТЕГИИ УПОРЯДОЧЕНИЯ На основе резольвенций, обеспечиваемых различными стратегиями очищения, иногда можно искать опровержение, упорядочив выполняемые резольвенции. В стратегиях упорядочения не запрещаются никакие типы резольвенций, а лишь даются указания. на то, какие из них надо выполнять в первую очередь. Стратегии упорядочения соответствуют рассмотренным в гл. 3 и 5 эвристическим стратегиям перебора для поиска на графах.

При хорошем упорядочении не обязательно вычислять все элементы множеств Я(5), ЯЯ(5) и т. д. Если пустое предложение появляется впервые на уровне п, то хочется думать, что перебор можно прямо направить на этот уровень, не заполняя нижние уровни. Две довольно эффективные стратегии упорядочения — это стратегия предпочтения одночленам и стратегия. наименьшего числа компонент. В стратегии предпочтения одночленам делается попытка сначала построить резольвенты между одно- членами„т. е. предложениями, содержащими единственный литерал. Если это удается, то сразу же получается опровержение. Если же не могут найти пару одночленов, у которых есть 948 Гл.

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

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

При введении граничных уровней для возможности использования и других резольвенцнй такая стратегия не препятствует нахождению опровержения (если оно существует в пределах заданной границы) и, как правило, сильно ускоряет процесс перебора. Стратегия наименьшего числа компонент упорядочивает резольвенции согласно длине получаемых резольвент. Так, два предложения, дающие наиболее короткую резольвенту, разрешаются в первую очередь. Эта стратегия в некотором смысле дороже, поскольку до выполнения резольвенции надо подсчитать длины потенциальных резольвент н упорядочить их. вНЕ БиБлиОГРАФические и истОРические зАмечАния Обсуждения стратегий перебора Проблема построения эвристически эффективных стратегий перебора (поиска) при условии сохранения логической полноты прекрасно изложена в статье Дж.

Робинсона (1967). Г. Робинсон и др. (1964) дали ясное описание нескольких стратегий и привели много примеров. Стратегии упрощения Проблема исключения подслучаев в процессе поиска доказательства оказывается тоньше, чем это может показаться. В статье Ковальского (1970а) указаны некоторые несоответствия в исследовании данной проблемы Ковальским и Хэйесом (1969); полностью этот вопрос рассмотрен в диссертации Ко. вальского (19706), 811.

оиблиаграфические и исторические аамечаиик 249 Стратегии очищения Стратегия формы с отфильтровандыми предшествующими вершинами (АГ-формы) является простейшей из семейства связанных между собой стратегий. В теореме 8.1 утверждается, что АГ-стратегия логически полна; доказательство этой теоремы приведено в работе Лакхэма (1969). Хотя мы здесь показали, что полнота стратегии поддерживающего множества следует из теоремы 8.1, на самом деле она была разработана раньше (Вос и др., 1965). Существуют разные пути дальнейшего усовершснствования АГ-стратегии. В некоторых случаях их объединяют со стратегией, предложенной Эндрюсом (1968), использующей слияния. Среди работ, в которых доказывается полнота.

АГ-формы со слиянием, укажем работы Киберца и Лакхэма (1971), Р(ейтса, Рафаэля и Харта (1970), Андерсона и Бледсоу (1970). В первой содержатся другие результаты, касающиеся свойств доказательств в АР-форме, а в двух последних применяются сравнительно новые методы доказательства полноты, представляющие самостоятельный интерес. Андерсон и Бледсоу доказали своим методом полноту и других стратегий. В статье Лавленда (1968) устанавливается полнота еще одного ограничения на АГ-стратегию.

Модельные стратегии представляют собой развитие Р,-дедукций, предложенных впервые Дж. Робинсоном (19656). Слейджл (1967) доказал полноту некоторых очень общих модельных стратегий. Теорема 8.2 взята у Лакхэма (1969); она является простым частным случаем одной из теорем Слейджла. Мельцер (1966, 1968) предлагает дополнительные результаты, касающиеся дедукцнй Рптипа. Стратегии упорядочения Стратегия предпочтения одночленам была предложена и оправдана Восом н др.