Шаг 7.
Основы логического программирования.
Этапы приведения формулы к стандартной форме записи

    На этом шаге мы рассмотрим этапы приведения формулы к стандартной форме записи.

    В логике предикатов первого порядка процесс приведения формул к стандартной форме записи включает в себя семь этапов.

  1. Исключение символов импликации, то есть следствия "если ..., то ...", с помощью формулы эквивалентности A®Bº ~AÚB. Например, ("x) (A(x)®В(x))º("x) (~А(х)ÚB(x)).

       

  2. Перенос символа отрицания внутрь формулы (только для формул, не являющихся атомарными). При этом область действия символа отрицания сужается. Каждый символ отрицания "~" может быть применен только к одной атомарной формуле. Например, ~(AÙ B) (~AÚ~B).

       

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

        Например, формула ("x)(A(x))Ù ($x)B(x) в результате разделения переменных, то есть замены переменной x после попадания ее под действие квантора существования $ на переменную y, преобразуется к виду ("x)(A(x)) Ù($y)B(y).

       

  4. Исключение кванторов существования из формулы. Переменная, связанная квантором существования, может быть заменена функцией, называемой сколемовской, а в частном случае константой (то есть сколемовской функцией без аргументов).

        Например, формула ($x)A(x) может быть заменена формулой A(b) при x=b, где b - константа.

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

        Например, если в формуле:
        ("x)(Человек(x) - ($y) Мать(x,y)),
    обозначающей, что каждый человек имеет мать, удалить квантор существования $ y и поставить y=Мария, то получим, что все люди имеют одну и ту же мать по имени Мария, а это неверно. Здесь при удалении квантора существования $ надо вводить не константу, а составной терм, то есть функциональный символ f(x), который каждому конкретному человеку ставит в соответствие его мать:
        ("x)(Человек(x)® Мать(x,f(x))).

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

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

        Так, после удаления кванторов всеобщности рассмотренная выше формула будет иметь следующий вид:
        Человек(x)®Мать(x,f (x)).

  6. Приведение формулы к конъюнктивной нормальной форме. Формулу записывают в виде последовательности соединенных между собой символами конъюнкции элементов, каждый из которых является литерой или состоит из нескольких литер, соединенных между собой символами дизъюнкции. Например, формулы A(x)ÙB(x) и (A(x) ÚB(x)ÚC(x)Ú(D(x)ÚE(x)Ú F(x) приведены к конъюнктивной нормальной форме.

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

        Следовательно, каждая формула исчисления предикатов эквивалентна совокупности дизъюнктов, состоящих из литералов и соединенных символами дизъюнкции. Слово "совокупность" подчеркивает, что порядок дизъюнктов не имеет значения. Например, формулу:
        A(x)ÙB(x)ÙC(x)
    можно представить в виде совокупности дизъюнктов (знак дизъюнкции опущен):
        {A(x), B(x), C(x)}.

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

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

    Метод резолюций является полным. Если некоторый факт следует из исходных гипотез, то всегда можно доказать его истинность методом резолюций.

    При рассмотрении логики высказываний было показано, что формула A является логическим следствием формул B1, B2, ..., Bn тогда и только тогда, когда формула B1ÚB2ÚÚBnÚ ~A противоречива, то есть доказательство того, что отдельная формула есть логическое следствие конечного множества формул, эквивалентно доказательству того, что некоторая связанная с ними формула общезначима или противоречива.

    Так же и в логике предикатов, если множество формул {B1, B2,…, Bn} непротиворечиво, то формула А является следствием формул {B1, B2, ..., Bn} тогда и только тогда, когда множество формул {B1, B2,…, Bn, ~А} противоречиво.

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

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

    Используя метод резолюций, можно автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь задать исходные высказывания, а следствие из них будет получено автоматически с помощью правил вывода.

    На следующем шаге мы рассмотрим хорновские дизъюнкты.




Предыдущий шаг Содержание Следующий шаг