(«каждый человек имеет мать») заменить каждое вхождение переменной V, связанной квантором существования, на константу g2 и удалить квантор существования, то получится:

all(X, человек(Х) -› мать(X,g2))

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

all(X, человек(Х) -› мать(Х, g2(Х)))

В этом случае функциональный символ g2 соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.

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

all(X, мужчина(Х) -› аll(Y,женщина(Y) -› нравится (X,Y)))

преобразуется в

аll(Х, аll(Y,мужчина(Х) -› (женщина(Y) -› нравится (X,Y))))

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

аll(Х,живой(Х) # мертвый(Х)& аll(Y,нравится(мэри,Y) #грязный(Y))

теперь можно представить так:

(живой(Х) # мертвый(Х))& (нравится(мэри,Y) # грязный (Y))

Эта формула значит, что, какие бы X и Y ни были выбраны, либо X живой, либо X мертвый, и либо Мэри нравится Y, либо Y – грязный.

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

(А&В) # С эквивалентно (А # С)&(В # С)

А # (В&С) эквивалентно (А # В)&(А # С)

Так, например, формула:

выходной(Х) # (работает(крис, X) & (сердитый (крис) # унылый(крис)))

(Для каждого X либо X – выходной день, либо Крис работает в день X и при этом он либо сердитый, либо унылый) эквивалентна следующей:

выходной(Х) # (работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))

(Для каждого X, во-первых, X является выходным днем или Крис работает в день X; во-вторых, либо X – выходной день, либо Крис сердитый или унылый).

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

(А & В) & (С & (D & Е))

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

(А & В) & (С & (D & Е)) А & (( В& С) & (D & Е)) (А & В) & ((С & D) & Е)

обозначают одно и то же. И хотя структурно эти формулы различны, они имеют один и тот же смысл. Это объясняется тем, что если установлена истинность всех высказываний из некоторого множества, то не имеет значения каким образом они группируются в сложное конъюнктивное высказывание. Не имеет значения, например, как сказать «А истинно и В и С также истинны» или «А и В истинны и С тоже истинно». Следовательно, скобки никак не влияют на смысл формулы. Можно просто написать (неформально):

A & B & C & D & E

Далее, порядок записи этих формул также не имеет значения. Безразлично, как сказать: «А и В истинны» или «В и А истинны», так как оба эти высказывания имеют одно и то же значение. И наконец, нет необходимости указывать знак конъюнкции (&) между формулами, так как заранее известно, что на верхнем уровне формула является конъюнкцией составляющих ее частей. Поэтому, в действительности, значение представленной формулы можно выразить значительно короче, представив ее в виде совокупности {А, В, С, D, Е}. Название «совокупность» подчеркивает, что порядок элементов не имеет значения. Совокупность {А, В, С, D, Е} в точности то же самое, что и {В, А, С, Е, D}, {Е, D, В, С, А} и так далее. Формулы, являющиеся элементами совокупности, полученной в результате преобразования некоторой формулы исчисления предикатов, называются дизъюнктами. Таким образом, каждая формула исчисления предикатов эквивалентна (в некотором смысле) совокупности дизъюнктов.

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

((V # W) # X) # (Y # Z)

где переменные являются литералами. Теперь те же самые рассуждения, которые были сделаны о структуре формулы на верхнем уровне, можно применить к дизъюнктам. Как и выше, скобки не влияют на значение дизъюнкта. Точно так же несуществен и порядок литералов. Таким образом, можно просто сказать, что дизъюнкт – это совокупность литералов (неявно соединенных дизъюнкцией). В последнем примере это будет {V, W, X, Y, Z}

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

(выходной(Х) # работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))

Эта формула порождает два дизъюнкта. Первый дизъюнкт содержит литералы:

выходной(Х), работает(крис,Х)

а второй литералы:

выходной(Х), сердитый(крис), унылый(крис)

Другой пример. Формула

(человек(адам)& человек(ева))&

((человек(Х) # ~мать(Х,Y)) # ~человек(#))

дает три дизъюнкта. Два из них содержат по одному литералу каждый