Пренексные нормальные формы

В исчислении предикатов имеется пренексная нормальная форма (ПНФ). Необходимость введения ПНФ будет обусловлена в дальнейшем упрощением процедуры доказательства теорем.

Сначала рассмотрим некоторые равносильные формулы в исчислении предикатов. Напомним, что две формулы F и Ф равносильны, т. е. F = Ф тогда и только тогда, когда истинностные значения этих формул совпадают при любой интерпретации F и Ф. Для подчеркивания факта, что переменная х входит в формулу F, будем писать F[х], хотя F может содержать и другие переменные.

Имеем следующие пары равносильных формул:

x F[х] Ф = x( F[х] Ф);

x F[х] & Ф = x( F[х] & Ф);

x F[х] Ф = x( F[х] Ф);

x F[х] & Ф = x( F[х] & Ф)

при условии, что переменная х не входит свободно в формулу Ф.

Равносильность этих формул очевидна, так как формула Ф не содержит свободно х и поэтому не входит в область действия кванторов.

Далее имеем

x F[х] & x Ф[х] = x( F[х] & Ф),

x F[х] Ф[х] = x( F[х] Ф[х]).

Теперь дадим определение ПНФ. Говорят, что формула F исчисления предикатов находится в ПНФ тогда и только тогда, когда ее можно представить в форме K₁ x₁ K₂ x₂ … K_r x_r M, где K_i x_i, i=1,2, …,r есть либо x_i , либо x_i и М – бескванторная формула. Иногда называют K₁ x₁ K₂ x₂ … K_r x_r префиксом, а М – матрицей формулы F.

Например, формула

F₁ = х у (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₁ x F[х] K₂ x Ф[х] = K₁ x K₂ y ( F[х] Ф[y]),

K₁ x F[х] & K₂ x Ф[х] = K₁ x K₂ y ( F[х] & Ф[y]),

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

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

K₁ x₁ K₂ x₂ … K_r x_r M.