7.2. ПРИМЕР

Рассмотрим следующую тривиальную задачу: «Если Майкл повсюду ходит за Джоном, а Джон находится в школе, то где Майкл?» Совершенно ясно, что в этой задаче сформулированы два «факта», а затем поставлен вопрос, который, по-видимому, можно вывести из этих двух фактов. Эти факты легко переводятся на язык п. п. формул и дают следующее множество формул:

и

где предикатному символу придана очевидная интерпретация («быть в определенном месте», соответствующая предлогу Перев.).

На вопрос «Где Майкл?» можно дать ответ, если сначала доказать, что п. п. формула

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

Рис. 7.1. Дерево опровержения для рассматриваемого примера.

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

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

Заметим, что отрицание п. п. формулы дает

или, в форме предложения, просто

Теперь из этого дерева опровержения извлечем ответ на вопрос «Где Майкл?» Это осуществляется следующим образом:

(1) К каждому предложению, вытекающему из отрицания предположения, добавляется его отрицание. Тогда принимает вид тавтологии

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

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

В нашем примере этот процесс порождает дерево, показанное на рис. 7.2, с предложением АТ (Майкл, школа) в его корне.

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

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

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

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