Основные понятия и методы теории формальных систем. Волохович А.В. - 24 стр.

   получаем ∀ -формулу. Опишем алгоритм                                     последовательного
исключения кванторов существования.

        Алгоритм Сколема
        Шаг 1. Формулу представить в ПНФ.
        Шаг 2. Найти наименьший индекс i такой, что K 1 , K 2 , … K i все
равны ∀ , но K i = ∃ . Если i = 1, т. е. квантор ∃ стоит на первом месте,
то вместо х 1 в формулу М подставить константу с, отличную от
констант, встречающихся в М. Если такого i нет, то СТОП: формула
F- является ∀ -формулой.
        Шаг 3. Взять новый (i – 1)-местный функциональный символ f i ,
не встречающийся в F. Заменить F на формулу
         ∀ x 1 ∀ x 2 … ∀ x i - 1 K i + 1 x i + 1 ,…, K r x r M[x 1 , x 2 , …, x i - 1 , f (x 1 , x 2 , …,
x i - 1 ), x i + 1 , …, x r ].
        Шаг 4. Перейти к шагу 2.

   Таким       образом,     алгоритм     Сколема,   сохраняя   свойство
невыполнимости, приводит произвольную формулу, имеющую
пренексный вид, к ∀ -формуле.
   Напомним, что атом или его отрицание называется литерой.
Литера вида А называется положительной, а вида ¬ А –
отрицательной.
   Рассмотрим         теперь   преобразование     бескванторной   части
(матрицы) к виду так называемых дизъюнктов. Дизъюнктом
называется формула вида
                               L1 ∨ L2 ∨ … ∨ Lk,
где L 1 ,L 2 ,…,L k – произвольные литеры.
   Дизъюнкты, соединенные знаком &, образуют конъюнктивную
нормальную         форму     (КНФ).    Существует    простой   алгоритм
равносильного          преобразования     произвольной    бескванторной
формулы в КНФ. Представим его в развернутом виде.

    Алгоритм приведения к КНФ
    Шаг 1. Начало: дана формула F, составленная из литер с
применением связок & и ∨ . Предполагается, что в формуле
исключены скобки между одинаковыми связками, т. е. нет
выражений вида
                    Ф 1 ∨ (Ф 2 ∨ Ф 3 ), (Ф 1 ∨ Ф 2 ) ∨ Ф 3
или
                   Ф 1 & (Ф 2 &Ф 3 ), (Ф 1 &Ф 2 ) &Ф 3 .
    Шаг 2. Найти первое слева в хождение двух символов ∨ ( (или
) ∨ ). Если таких вхождений нет, то СТОП: формула F находится в
КНФ.




24