В исчислении высказываний были рассмотрены две нормальные формы высказываний – КНФ и ДНФ. В исчислении предикатов также имеется нормальная форма, так называемая пренексная нормальная форма (ПНФ).
Говорят, что формула F исчисления предикатов находится в ПНФ тогда и только тогда, когда ее можно представить в форме z1х1z2х2 … zrхr М, где каждый ziхi, i =1, 2, …, r есть либо "xi, либо $xi и М – бескванторная формула. Иногда z1х1z2х2 … zrхr называют префиксом, а М – матрицей формулы F.
Например, формула F1= $x"y(Q(x,y)ÚØP(f(x))®R(x,g(y))) находится в ПНФ, а формула F2 = "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. Вынесение кванторов. Используются следующие равносильности:
1. zxF(x)ÚФ = zx(F(x)ÚФ);
2. zxF(x)ÙФ = zx(F(x)ÙФ);
3. "xF(x)Ù"xФ(x) = "x(F(x)ÙФ(x));
4. $xF(x)Ú $xФ(x) = $x(F(x)ÚФ(x));
5. z1xF(x)Ú z2xФ(x) =z1x z2y(F(x)ÚФ(y));
6. xF(x) Ù z2xФ(x) =z1x z2y(F(x) ÙФ(y));
где z, z1, z2 – кванторы либо $, либо ".
После выполнения пятого шага формула приобретает пренексный вид.