Пренексные нормальные формы исчисления предикатов

В исчислении высказываний были рассмотрены две нормальные формы высказываний – КНФ и ДНФ. В исчислении предикатов также имеется нормальная форма, так называемая пренексная нормальная форма (ПНФ).

Говорят, что формула F исчисления предикатов находится в ПНФ тогда и только тогда, когда ее можно представить в форме z₁х₁z₂х₂ … z_rх_r М, где каждый z_iх_i, i =1, 2, …, r есть либо "x_i, либо $x_i и М – бескванторная формула. Иногда z₁х₁z₂х₂ … z_rх_r называют префиксом, а М – матрицей формулы F.

Например, формула F₁= $x"y(Q(x,y)ÚØP(f(x))®R(x,g(y))) находится в ПНФ, а формула F₂ = "x(P(x) ® $yQ(x,y)) – не в ПНФ.

Существует простой алгоритм, преобразующий произвольную заданную формулу в равносильную ей формулу, имеющую пренексный вид. Алгоритм состоит из следующих шагов.

1. Исключение логических связок эквивалентности и импликации. Многократно (пока это возможно) применяется следующее правило: найти самое левое вхождение связок ® или « и сделать замены: F«Ф = (ØFÚФ)Ù(FÚØФ); F®Ф = ØFÚФ.

2. Продвижение знака отрицания до атома. Многократно (пока это возможно) делаются замены: ØØ F = F;

Ø(FÚФ) = ØFÙØФ;

Ø(FÙФ) = ØFÚØФ;

Ø"xF(x) = $x(Ø F(x));

Ø$x F(x) = "x(ØF(x)).

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

4. Удаление квантификаций, область действия которых не содержит вхождений квантифицируемых переменных.

5. Вынесение кванторов. Используются следующие равносильности:

zxF(x)ÚФ = zx(F(x)ÚФ);

zxF(x)ÙФ = zx(F(x)ÙФ);

"xF(x)Ù"xФ(x) = "x(F(x)ÙФ(x));

$xF(x)Ú $xФ(x) = $x(F(x)ÚФ(x));

z₁xF(x)Ú z₂xФ(x) =z₁x z₂y(F(x)ÚФ(y));

z₁xF(x) Ù z₂xФ(x) =z₁x z₂y(F(x) ÙФ(y));

где z, z₁, z₂ – кванторы либо $, либо ".

После выполнения пятого шага формула приобретает пренексный вид.