Основы программирования на языке Пролог



         

Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов


Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:

  1. пользуясь эквивалентностью A
    B
    ¬A
    B исключим импликацию;
  2. перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности:

    ¬(A

    B)
    ¬A
    ¬B ¬(A
    B)
    ¬A
    ¬B ¬(
    xA)
    x¬A ¬(
    xA)
    x¬A ¬¬A
    A

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

    QxA(x)

    B
    Qx(A(x)
    B), если B не содержит переменной x, а Q
    {
    ,
    }

    QxA(x)

    B
    Qx(A(x)
    B), если B не содержит переменной x, а Q
    {
    ,
    }

    xA(x)
    xB(x)
    x(A(x)
    B(x))
    xA(x)
    xB(x)
    x(A(x)
    B(x))

    Q1xA(x)

    Q2xB
    Q1xQ2y(A(x)
    B(y)), где Q
    {
    ,
    }

    Q1xA(x)

    Q2xB
    Q1xQ2y(A(x)
    B(y)), где Q
    {
    ,
    }

Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле кванторы существования. Для этого для каждого квантора существования выполним следующий алгоритм.

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

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

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм устранения кванторов существования придумал Сколем в 1927 году.

Имеет место теорема о том, что формула и ее сколемизация эквивалентны в смысле выполнимости.

Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости.

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

A

(B
C)
(A
B)
(A
C) A
(B
C)
(A
B)
(A
C)




Содержание  Назад  Вперед