7.3. ПРОЦЕСС ИЗВЛЕЧЕНИЯ ОТВЕТА

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

Хотя этот метод и прост, но у него есть несколько тонких моментов, которые мы разъясним на примерах.

Пример 1. Рассмотрим правильно построенные формулы

Их можно интерпретировать так:

1) Для всех если х является родителем у и у является родителем то х является прародителем

2) Каждый индивид имеет своего родителя.

Будем считать эти формулы гипотезами и зададим такой вопрос: «Существуют ли такие индивиды что (Иными словами, существуют ли такие х и у, что х является прародителем у?)

Сформулируем этот вопрос в виде предположения, требующего доказательства:

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

Рис. 7.3. Дерево опровержения для примера 1.

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

Модифицированное дерево доказательства приведено на рис. 7.4. Отрицание предположения преобразовано в тавтологию, а резольвенции осуществляются те же самые, что и на рис. 7.3. Каждая резольвенция в модифицированном дереве опирается на множества унификации, которые в точности соответствуют множествам унификации графа опровержения. Множества унификации на рис. 7.4 подчеркнуты.

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

Рис. 7.4. Модифицированное дерево доказательства для примера 1.

Пример 2. Покажем, как преобразовать в тавтологии более сложные предложения, возникающие при отрицании предположения.

Рассмотрим следующее множество предложений:

Мы хотим доказать, исходя из этих аксиом, предположение

Отрицание его приводит к двум предложениям, каждое из которых содержит по два литерала:

Граф опровержения для нашего дополненного множества предложений приведен на рис. 7.5.

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

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

Рис. 7.5. Граф опровержении для примера 2.

Аналогично преобразуем предложение в тавтологию

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

Мы видим, - что здесь ответное утверждение имеет форму, несколько отличную от формы, в которой было сделано

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

Рис. 7.6. (см. скан) Модифицированный граф доказательства для примера 2.

Этот дизъюнкт похож; на один из дизъюнктов, содержащихся в предположении, причем вместо переменной х, относящейся к квантору существования, здесь стоит

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

использовать в качестве «ответа» на вопрос, представляемый исходным предположением.

Ситуацию, возникающую в общем случае, можно описать точно. Допустим, что нам нужно доказать предположение, имеющее вид

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

где переменные явным образом не указаны. Отрицание предположения приводит к предложениям

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

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