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

   Теперь дадим определение ПНФ. Говорят, что формула F
исчисления предикатов находится в ПНФ тогда и только тогда, когда
ее можно представить в форме K 1 x 1 K 2 x 2 … K r x r M, где K i x i , i=1,2,
…,r есть либо ∀ x i , либо ∃ x i и М – бескванторная формула. Иногда
называют K 1 x 1 K 2 x 2 … K r x r префиксом, а М – матрицей формулы
F.
   Например, формула
           F 1 = ∃ х ∀ у (Q (х, у) ∨ ¬ Р (f (х)) → R (х, g (у)))
находится в ПНФ.
   Существует простой алгоритм, преобразующий произвольную
заданную формулу в равносильную ей формулу, имеющую
пренексный вид. Алгоритм состоит из следующих шагов.
   Шаг 1. Исключение логических связок ~ и → . Многократно (пока
это возможно) применяется следующее правило: найти самое левое
вхождение связки ~ или → и сделать замены:
                      F~ Ф = ( ¬ F ∨ Ф) & (F ∨ ¬ Ф),
                             F → Ф = ¬ F ∨ Ф.
   Результатом этого шага будет формула, равносильная исходной и
не содержащая связок ~ и → .
   Шаг 2. Продвижение знака отрицания ¬ до атома. Многократно
(пока это возможно) делаем замены:
                                  ¬ ¬ F = F,
                           ¬ (F ∨ Ф) = ¬ F ∨ ¬ Ф,
                           ¬ (F & Ф) = ¬ F& ¬ Ф,
                          ¬ ∀ xF[x] = ∃ x( ¬ F[x]),
                          ¬ ∃ xF[x] = ∀ x( ¬ F[x]).
   В результате выполнения этого шага получается формула, у
которой знаки отрицания стоят только перед атомами.
   Шаг 3. Переименование связанных переменных. Многократно
(пока это возможно) применяется следующее правило: найти самое
левое вхождение переменной такое, что это вхождение связано
(некоторым квантором), но существует еще одно вхождение этой же
переменной; затем сделать замену связанного вхождения на
вхождение новой переменной.
   Шаг 4. Вынесение кванторов. Для этого используем следующие
равносильности:
                      K x F[х] ∨ Ф =K x( F[х] ∨ Ф),
                      K x F[х] & Ф =K x( F[х] & Ф),
                 ∀ x F[х] & ∀ x Ф[х] = ∀ x( F[х] & Ф[х]),
                  ∃ x F[х] ∨ ∃ x Ф[х] = ∃ x( F[х] ∨ Ф[х]),
           K 1 x F[х] ∨ K 2 x Ф[х] = K 1 x K 2 y ( F[х] ∨ Ф[y]),
           K 1 x F[х] & K 2 x Ф[х] = K 1 x K 2 y ( F[х] & Ф[y]),

где K 1 , K 2 , K – кванторы либо ∀ , либо ∃ .



22