Этапы получения предварённой формы.

1. Исключить связки эквивалентности и импликации.

2. Преобразовать все вхождения отрицания, состоящие непосредственно перед атомами. Многократно (пока это возможно) делаются замены:

3. Переименовать (если необходимо) связанные переменные таким образом, чтобы никакая переменная не имела бы одновременно свободных и связанных вхождений: " X A (X) º " T A (T) X, T Î M.

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

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

4. Удаление тех квантификаций, область действия которых не содержит вхождений квантифицированной переменной. Вынесение кванторов (перемещение всех квантификаций в начало формулы). Для этого используется правила:

(" X A & " X B) º" X (A & B),

(" X A (X) & B) º" X (A (X) & B), если В не содержит X,

(A & " X B (X)) º" X (A & B (X)), если A не содержит X,

($ X A (X) & B) º $ X (A (X) & B), если В не содержит X,

(A & $ X B (X)) º $ X (A & B (X)), если A не содержит X.

А также используются формулы эквивалентности для исчисления предикатов. Помимо эквивалентностей логики высказываний для логики предикатов справедливы следующие эквивалентности (А (х), В (х), Р (x, y) – предикаты, С – высказывание):

Комбинация кванторов:

1. " x " yP (x, y) = " y " xP (x, y),

2. $ x $ yP (x, y) = $ y $ xP (x, y),

3. " x $ yP (x, y) ≠ $ y " xP (x, y).

Комбинация кванторов и отрицаний:

;

;

.

Расширение области действия кванторов (С не зависит от х):

1. C &" xB (x) = " x [ C&B (x)],

2. C Ú" xB (x) = " x [ C Ú B (x)],

3. C →" xB (x) = " x [ C→B (x)],

4. " x [ B (x) →C ] = $ xB (x) →C,

5. $ x [ C Ú B (x)] = C Ú$ xB (x),

6. $ x [ C & B (x)] = C &$ xB (x),

7. $ x [ C → B (x)] = C → $ xB (x),

8. $ x [ B (x) → C ] = " xB (x) →C.

Расширение области действия кванторов:

1. " xA (x)&" xB (x) = " x [ A (x)& B (x)],

2. $ x [ A (x)Ú B (x)] = $ xA (x)Ú$ xB (x),

3. $ xA (x)&$ xB (x) = $ x $ y [ A (x) &B (y)],

4. $ x [ A (x)& B (x)] → $ xA (x)&$ xB (x),

5. " xA (x)Ú" xB (x) → " x (A (x)Ú B (x)).

 

После выполнения четвертого шага получаем ПНФ.

Одна формула может допускать много эквивалентных предварённых форм. Вид результата зависит от порядка применения правил, а также от произвола при переименовании переменных.