3.10.4. Примеры доказательств с помощью принципа Эрбрана

Приведем полное доказательство, которое могло бы быть получено программной системой Робинсона. Допустим, что мы хотели бы доказать утверждение: “кисть является частью человека”. Для этого нам придется использовать понятия

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

где в дальнейшем —Р заменяет последовательность символов — символ Р для всякого предиката Р, что позволяет избежать символов V в предложениях.

В гипотезах в нашем примере используются четыре константы т., обозначающие соответственно “кисть", “рука”, “тело”, “человек”. Итак, в нашем случае к гипотезам добавляется отрицание заключения: Таким образом, программа работает с пятью предложениями, неявно объединенными с помощью операции Д:

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

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

Рассмотрим теперь более сложный пример использования метода резолюции.

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

Для описания того факта, что некоторая композиция двух элементов данной группы по определенному закону приравнивается к третьему элементу этой группы, используется предикат

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

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

Если обозначает сколемовскую функцию, которая дает инверсное значение какого-то элемента у, то мы имеем

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

Теперь нам необходимо выразить ассоциативность правила о среднем члене пропорции в соответствующих обозначениях. Это выполняется в два этапа. Вначале рассмотрим ассоциативность слева

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

Таблица 3.7. (см. скан) Доказательство коммутативности в группе, в которой методом Эрбрана или методом резолюции

что соответствует

Аналогичным образом выводится и ассоциативность справа

Заданное свойство описывается выражением

Наконец, отрицание заключения записывается в виде

так как выражение

записывается в виде

Элементы с рассматриваются как три константы. Доказательство должно привести к выводу о невозможности их существования. Это отрицание представляется в виде двух предложений

Общая схема доказательства методом резолюции приведена в табл. 3.7.