3.10.3. Практическая организация доказательств по принципу Эрбрана

Если все предложения представлены в стандартной форме, т. е. в виде конъюнкций, то использование знака Л становится лишним. Для порождения дерева достаточно хранить эти предложения, записанные непосредственно друг за другом. Во время выполнения резолюции предложение-резольвента добавляется к уже имеющимся (без изменения предшествующих предложений) так, чтобы сохранялись другие возможности подстановок, как это показано ниже. После выполнения подстановки в верхнюю часть всего набора предложений помещается элемент

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

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

Приведение к нормальной конъюнктивной форме

Необходимо показать теперь, каким образом любое выражение логики первого порядка может быть преобразовано в конъюнктивную нормальную форму. Алгоритм такого преобразования состоит из шести основных этапов.

1) Приведение к "пренексной” форме. На этом этапе переводятся в головную часть все кванторы. При этой операции

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

где — означает либо V, либо и * означает либо V, либо . Аналогичным образом

Например, если исходная формула Е имела вид

то после этого этапа она принимает следующую форму:

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

3) Удаление кванторов всеобщности. Теперь все переменные, которые имеются, подвержены действию кванторов всеобщности. Кванторы можно опустить и выражение Е записывается следующим образом:

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

4) Удаление символов и Здесь используются 2 теоремы:

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

Используются только три оператора: .

5) Уменьшение радиуса действия отрицаний. Теоремы

позволяют распространять действие оператора отрицания только на одиночные предикаты. Выражение Е имеет вид

6) Перевод выражения в конъюнктивную форму. Этот этап предназначен для приведения формул к следующему виду:

где предложения содержат уже только связки. V и П. Для этого используются теоремы дистрибутивности

Теперь выражение Е записывается следующим образом:

И наконец, получим

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

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

Первым реализовал на ЭВМ идеи Ж. Эрбрана Дж. Робинсон в 1963 г.