Так, например, формула:
выходной(Х) # (работает(крис, X) & (сердитый (крис) # унылый(крис)))
(Для каждого Xлибо X– выходной день, либо Крис работает в день Xи при этом он либо сердитый, либо унылый) эквивалентна следующей:
выходной(Х) # (работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))
(Для каждого X, во-первых, Xявляется выходным днем или Крис работает в день X; во-вторых, либо X– выходной день, либо Крис сердитый или унылый).
Формула, имеющаяся к началу этого этапа, в общем случае представляет совокупность конъюнктивных членов, являющихся литералами или состоящих из литералов, соединенных дизъюнкцией. Давайте сначала рассмотрим структуру формулы на верхнем уровне, не вникая в детали организации конъюнктивных членов. Формула могла бы иметь, например, следующий вид:
(А & В) & (С & (D & Е))
где переменные обозначают, возможно, сложные высказывания (формулы), но при этом они не содержат внутри конъюнкций. На данном этапе нет никакой необходимости знать структуру вложенности, представляемую использованием скобок, так как все высказывания
(А & В) & (С & (D
обозначают одно и то же. И хотя
A & B & C & D & E
Далее, порядок записи этих формул также не имеет значения. Безразлично, как сказать: «
Аи
Вистинны» или «
Ви
Аистинны», так как оба эти высказывания имеют одно и то же значение. И наконец, нет необходимости указывать знак конъюнкции (&) между формулами, так как заранее известно, что на верхнем уровне формула является конъюнкцией составляющих ее частей. Поэтому, в действительности, значение представленной формулы можно выразить значительно короче, представив ее в виде
Давайте рассмотрим несколько подробнее, что представляют собой эти дизъюнкты. Как уже было сказано, они состоят из литералов, соединенных друг с другом с помощью дизъюнкции. В общем случае, дизъюнкт выглядит примерно так:
((V # W) # X) # (Y # Z)
где переменные являются литералами. Теперь те же самые рассуждения, которые были сделаны о структуре формулы на верхнем уровне, можно применить к дизъюнктам. Как и выше, скобки не влияют на значение дизъюнкта. Точно так же несуществен и порядок литералов. Таким образом, можно просто сказать, что дизъюнкт – это
Теперь исходная формула представлена в стандартной форме. Более того, использовавшиеся для преобразования правила не зависят от того, существует или нет интерпретация, при которой формула истинна. Стандартная форма состоит из совокупности дизъюнктов, каждый из которых представляет совокупность литералов. Литерал – это либо атомарная формула, либо отрицание атомарной формулы. Эта форма является достаточно лаконичной, так как в ней опущены логические связки конъюнкций, дизъюнкций и кванторы всеобщности. Но при этом, очевидно, следует помнить о принятых соглашениях. И каждый раз, имея дело со стандартной формой, понимать, где и что в ней опущено. Рассмотрим, что представляет собой стандартная форма некоторых формул (предполагается, что уже выполнены первые пять этапов преобразования). Прежде всего вернемся к уже рассматривавшемуся примеру:
(выходной(Х) # работает(крис,Х)) & (выходной(Х) # (сердитый(крис) # унылый(крис)))
Эта формула порождает два дизъюнкта. Первый дизъюнкт содержит литералы:
выходной(Х), работает(крис,Х)
а второй литералы:
выходной(Х), сердитый(крис), унылый(крис)
Другой пример. Формула
(человек(адам)& человек(ева))&
((человек(Х) # ~мать(Х,Y)) # ~человек(#))
дает три дизъюнкта. Два из них содержат по одному литералу каждый
человек (адам)
и
человек (ева)
Другой содержит три литерала:
человек(Х), ~мать(Х,Y), ~человек(Y)
В заключении этого раздела рассмотрим еще один пример, демонстрирующий все этапы приведения формулы к стандартному виду. Начнем с формулы
all(X, аll(Y,человек(Y) -› почитает(Y,Х) -› король(Х))