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

      После выполнения четвертого шага формула приобретает
пренексный вид:
                    K 1 x 1 K 2 x 2 … K r x r M.


                     Сколемовские стандартные формы

     Ранее было показано, что отношение логического следования F 1 ,
F 2 , …, F n |- B равнозначно общезначимости формулы |- F 1 & F 2 &
…&F n → B или противоречивости (невыполнимости)          F1& F2&
…&F n & ¬ B. Так как в дальнейшем в процедурах доказательства мы
будем иметь дело только с невыполнимыми формулами, то без
потери общности ограничимся ими.
     Очевидно, что если формулы F и Ф равносильны, то F логически
невыполнима тогда и только тогда, когда логически невыполнима Ф.
     Благодаря этому утверждению и в силу того, что алгоритмы
приведения к ПНФ сохраняют равносильность невыполнимых
формул, мы ограничимся формулами, имеющими пренексный вид.
     Однако можно ограничиться еще более узким классом формул,
так называемых ∀ -формул.
     Формула F называется ∀ -формулой, если она представлена в
ПНФ, причем кванторная часть состоит только из кванторов
общности, т. е.

                          F= ∀ x 1 ∀ x 2 … ∀ x r M,

где M – бескванторная формула.
      Таким образом, возникает задача устранения кванторов
существования в формулах, представленных в ПНФ. Это можно
сделать путем введения сколемовских функций.
      Пусть формула F представлена в ПНФ:
      F= K 1 x 1 K 2 x 2 … K r x r M, где K j ∈ { ∀ , ∃ }.
      Пусть K i (1 ≤ i ≤ r) – квантор существования в K 1 x 1 K 2 x 2 … K r x r .
Если i=1, т.е. ни один квантор общности не стоит впереди квантора
существования, то выбираем константу c из области определения М,
отличную от констант, встречающихся в M, и заменяем х на с в М.
Из префикса квантор существования K 1 x 1 вычеркиваем. Если перед
квантором существования K i стоит K j , K j , …, K j
                                                   1   2         m
                                                                    кванторов
общности, то выбираем m-местный функциональный символ f,
отличный от функциональных символов в М, и заменяем х i на f
( x j , x j , …, x j ), называемую сколемовской функцией, в М. Квантор
     1   2    m


существования K i х i вычеркиваем из префикса. Аналогично
удаляются и другие кванторы существования в ПНФ. В итоге



23