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

        Шаг 3. Пусть первым вхождением указанной пары символов
является ∨ (. Тогда взять наибольшие формулы Ф 1 , Ф 2 , …, Ф r , Ψ 1 , Ψ 2 ,
…, Ψ s такие, что в F входит формула F 1 = Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ∨ (Ψ 1 &
Ψ 2 & …& Ψ s ), которая связана с вхождением ∨ (. Заменить формулу F
на формулу ( Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ∨ Ψ 1 )& ( Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ∨ Ψ 2 ) & …&
( Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ∨ Ψ s ).
    Шаг 4. Пусть первым вхождением является ) ∨ . Тогда взять
наибольшие формулы Ф 1 , Ф 2 , …, Ф r , Ψ 1 , Ψ 2 , …, Ψ s такие, что в F
входит формула F 1 = (Ψ 1 & Ψ 2 & …& Ψ s ) ∨ Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ,
связанная с вхождением ) ∨ . Заменить F 1 на (Ψ 1 ∨ Ф 1 ∨ Ф 2 ∨ … ∨ Ф r )&
(Ψ2 ∨ Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ) & …& (Ψ s ∨ Ф 1 ∨ Ф 2 ∨ … ∨ Ф r ).
     Шаг 5. Перейти к шагу 2.

    Итак, последовательным применением алгоритма приведения к
ПНФ, алгоритма Сколема и алгоритма приведения к КНФ с
сохранением свойства невыполнимости любая формула F может
быть представлена набором дизъюнктов, объединенных кванторами
общности.        Такую     формулу         будем       называть    формулой,
представленной в Сколемовской стандартной форме (ССФ). В
дальнейшем формулы вида ∀ x 1 ∀ x 2 … ∀ x r [D 1 & D 2 & …& D k ] , где
D 1 , D 2 , …, D k - дизъюнкты, а x 1 , x 2 , …, x r - различные переменные,
входящие в эти дизъюнкты, будет удобно представлять как
множество дизъюнктов S ={ D 1 , D 2 , …, D k }.


       Принцип резолюции для логики предикатов первого порядка

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

                             С 1 : Р(х) ∨ ¬ R(х),
                          С 2 : ¬ Р(g(х)) ∨ Q(y),

то резольвента может быть получена только после применения к С 1
подстановки g(х) вместо х.
   Имеем
                      С 1 : Р(g(х)) ∨ ¬ R(g(х)),
                       С 2 : ¬ Р(g(х)) ∨ Q(y),
                       С: ¬ R (g(х)) ∨ Q(y).
   Однако для случая

                          С 1 : Р(f(х)) ∨ ¬ R(х),
                          С 2 : ¬ Р(g(х)) ∨ Q(y),


25