Глава 12. ДОКАЗАТЕЛЬСТВО ТЕОРЕМ

12.0. Доказательство теорем, основанное на эрбрановской процедуре

12.0.1. Общие понятия

Для машинного решения задач нужен формальный прием, позволяющий представить в машине элементы решаемой задачи; кроме того, должно быть задано множество механизируемых операций для работы с таким формальным представлением. Изложенный в гл. 11 подход, основанный на пространстве состояний, дает формализм, который часто можно считать „естественным"; во всяком случае, он легко понимается людьми. К сожалению, из-за сложности выбора нужного правила из большого числа возможных правил вывода машинное решение задачи может стать неосуществимым. Другой подход состоит в применении некоторого способа представления, возможно, менее понятного для людей, однако приводящего к более непосредственному машинному представлению и к более простым операциям над символами. Оказалось, что необычно мощный эффект дает представление всех „задач" в широком смысле слова в виде теорем, доказываемых в рамках исчисления предикатов первого порядка. Дж. Робинсон (1965, 1967) предложил простой метод для работы с соответствующими выражениями, легко реализуемый на ЭВМ. Для объяснения работы этого метода обсудим сначала сущность доказательства теорем.

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

новые. Например, если и - ранее полученные п. п. в., то запись

указывает, что можно получить из с помощью правила вывода Рассмотрим теперь последовательность множеств образованную из некоторого множества аксиом по правилу

где — множество выражений, которое можно получить из множества применяя к каждому его элементу все возможные правила вывода из конечного множества правил Говорят, что высказывание В следует из аксиом, принадлежащих если для некоторого Продукции из гл. 11 можно интерпретировать как правила вывода. Трудность там возникала из-за того, что множество было относительно большим и приводило к быстро растущему числу членов последовательности (2). Этой трудности не было бы, если бы множество было мало. Например, пусть состоит из единственного правила вывода

Этого достаточно для доказательства любой теоремы в исчислении предикатов первого порядка. Правило (3) составляет основу для доказательства теорем с использованием принципа резолюции.

12.0.2. Обозначения

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

множество состоящее из двух элементов: И — истина, Л — ложь. Другими словами, любое -местное отношение либо истинно, либо ложно.

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

Атомной формулой, или атомом, называется предикат со своими аргументами:

Литерал — это атомная формула или ее отрицание. Когда структура атомных формул не существенна, будем обозначать их а их отрицания — Когда структура литерала не существенна, будем обозначать -литерал через

Таблица 12.1 (см. скан) Простые высказывания о неравенствах в обозначениях предикатов

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

В табл. 12.1 приведены некоторые простые высказывания относительно неравенств, выраженные в описанных обозначениях. Здесь константы должны интерпретироваться как любые два вещественных числа, а функции следует рассматривать как однозначные функции вещественных чисел. Предикатами здесь являются три возможных отношения порядка для любой пары вещественных чисел (больше, меньше, равно). Очевидно, что любое высказывание о конкретном упорядочении данной пары либо истинно, либо ложно, в том числе и высказывание „Предложения принадлежат , которое означает, что эти предложения одновременно принимают значение истина.