Для этого используются законы
1) Q(x)B(x) Ú C º Q(x) (B(x) Ú C),
2) Q(x)B(x) & C º Q(x) (B(x) & C),
3) Q1(x)B(x) Ú Q2(x)D(x) º Q1(x)Q2(у) (B(x) Ú D(у)),
4) Q1(x)B(x) & Q2(x)D(x) º Q1(x)Q2(у) (B(x) & D(у)).
В формулах 1)-4) под Q(x) понимается любой из кван-торов " и $ , подформула С не должна содержать перемен-ную x. Для того, чтобы при вынесении в начало формулы не изменялись первоначальные области действия кванторов и не нарушалась эквивалентность преобразований, необходи-мо производить переименование связанных переменных так, как в формулах 3)-4). Смысл переименования заклю-чается в том, что фактически первое и второе вхождение связанных переменных независимы - переменные играют роль индексов, принимающих предписанные им значения.
Рассмотрим применение данного преобразования на примере. Для того, чтобы вынести вперед квантор $х, необ-ходимо заменить все вхождения переменной х в подфор-муле $ y((ØQ(x,у) Ú Р(х)) & (ØР(х) Ú Q(x,у))), иначе окажут-ся связанными все свободные вхождения х в нее. Заменяя в этой подформуле х на z и вынося квантор, получим:
А = $х((Ø Р(х) Ú $ y((ØQ(z,у) Ú Р(z)) & (ØР(z) Ú Q(z,у))) .
При вынесении квантора $ у изменения области дей-ствия квантора не происходит. В результате формула приоб-ретает следующий вид:
А = $х$ y ((Ø Р(х)) Ú ((ØQ(z,у) Ú Р(z)) & (ØР(z) Ú Q(z,у))) .
После вынесения кванторов в начало формулы её можно представить в виде:
А= (Q1 (x1) Q2 (x2)...Qn (xn))M(x1, x2 ,...,xn ).
Матрица M(x1, x2 ,...,xn ) не содержит кванторов и логи-ческих операций, помимо (Ø,Ú, &).
5. Раскрыть в матрице все конъюнкции, содержащиеся внутри дизъюнкций.
Цель операции - представить матрицу в виде конъ-юнкции дизъюнктов.
Для раскрытия применяем правило:
B Ú (C&D) º (BÚC) & (BÚD).
В примере применение этого правила к матрице при-водит её к виду:
M= ((Ø Р(х)) Ú ((ØQ(z,у) Ú Р(z)) & (ØР(z) Ú Q(z,у)))= (Ø Р(х) Ú ØQ(z,у) Ú Р(z)) & (Ø Р(х) Ú Ø Р(z) Ú Q(z,у)).
В итоге у рассмотренной формулы пренексная нор-мальная форма будет следующей:
А¢ =$х$ y ((ØР(х)ÚØQ(z,у)ÚР(z)) & (Ø Р(х)Ú Ø Р(z)Ú Q(z,у))).
Отметим, что пренексная нормальная форма с матри-цей в виде конъюнкции дизъюнкций с точностью до обо-значения переменных эквивалентна исходной формуле.