3.8.4. Метод Сиклосси и Маринова

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

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

Пример 1. Исчисление высказываний

Пусть заданы шесть правил вывода:

и одна теорема, которую нужно доказать:

В первый момент используется экстенсивное правило 6. Поиск проводится таким образом, что к уже встречавшимся ранее выражениям правила вывода больше не применяются и они помечаются в качестве “мертвых”. Заключение доказываемой теоремы используется только в качестве условия остановки — сам поиск проводится перебором вслепую.

Дерево поиска показано на рис. 3.15. На нем узлы занумерованы в порядке их получения в процессе доказательства теоремы. Процесс идет вначале в ширину: выполняются все возможные преобразования на одном и том же уровне для того же самого выражения и лишь потом осуществляется переход на следующий уровень.

С исходным выражением Н (узел 1) может быть унифицировано в данном случае только правило 1.

Рис. 3.15. Порождающее дерево для теоремы

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

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

Пример 2. Элементарная теория групп

Заданы правил вывода:

С их помощью необходимо доказать следующую теорему:

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

Рис. 3.16. Порождающее дерево для теоремы .

Правило 1 полагается системой псевдоэкстенсивным, а правило 4 — экстенсивным. Впрочем, система будет неявным образом использовать следующую метатеорему: поскольку правило 4 не действует, могут применяться только правила 1 и 2. Решение получается за 11 шагов, причем используются только правила 1 и 2. Ход решения представлен на рис. 3.16.

При тех же правилах вывода доказательство более интересной теоремы

требует уже 351 шага или нескольких секунд работы процессора ЭВМ.

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

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

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

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