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