7.4. ПРЕДПОЛОЖЕНИЯ, СОДЕРЖАЩИЕ ПЕРЕМЕННЫЕ, ОТНОСЯЩИЕСЯ К КВАНТОРУ ВСЕОБЩНОСТИ

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

Проиллюстрируем это на примере. Зададим аксиомы в виде предложений:

1) : каждый х является ребенком для (Иными словами, — функция, ставящая в соответствие ребенку индивида самого индивида.)

2) для всех если х — ребенок для у, то у — родитель для х.

Теперь мы задаем вопрос: «Для любого х кто является его родителем?» Предположение, соответствующее этому вопросу, имеет вид

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

а затем

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

Рис. 7.7. Модифицированное дерево доказательства для получения ответного утверждения.

(Отрицание предположения означает, что некоторой индивид, а не имеет родителей.) Модифицированное дерево доказательства, в корневой вершине которого находится ответное утверждение, изображено на рис. 7.7.

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

Можно показать (Лакхэм и Нильсон, 1971), что в процессе извлечения ответа всегда можно заменять любые сколемовы функции, возникающие при отрицании предположения, новыми переменными. В модифицированном доказательстве в эти новые переменные не будет делаться никаких подстановок, так что они пройдут через доказательство без изменения и появятся в окончательном ответном утверждении. Резольвенциями в модифицированном доказательстве по-прежнему будут лишь резольвенции, определяемые множествами унификации, соответствующими множествам унификации, появляющимся в ходе первоначального опровержения. В процессе некоторых резольвенций переменные могут быть переименованы, так что, возможно, некоторая переменная, использованная на месте сколемовой функции, окажется переименованной и станет, таким образом, «родоначальником» новых переменных в окончательном ответном утверждении.

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

Пример 3. Пусть 5 состоит из единственной аксиомы (в форме предложения)

Нам нужно доказать предположение

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

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

при переименовании в процесс резольвенции переменных в одном предложении.

Пример 4. Допустим, что нам нужно доказать то же самое предположение, что и в предыдущем примере, но теперь исходя из аксиомы .

Рис. 7.8. (см. скан) Деревья доказательства для примера 3.

Дерево опровержения изображено на рис. 7.9, а. В предложении, происходящем из отрицания предположения, содержится сколемова функция

На рис. 7.9, 6 изображено дерево модифицированного доказательства, в котором вместо сколемовой функции

использована переменная Мы получаем доказательство ответного утверждения

совпадающего (с точностью до наименований переменных) с исходной аксиомой.

Рис. 7.9. (см. скан) Деревья доказательства для примера 4.

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

В заключение перечислим этапы процесса извлечения ответа:

1. В ходе некоторого процесса поиска (перебора) строим граф опровержения на основе резольвенций и выделяем в нем множества унификации.

2. Вместо сколемовых функций, которые появляются в предложениях, происходящих из отрицания предположения, подставляем новые переменные.

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

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

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

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