2015-04-12
1315
Для облегчения анализа сложных рассуждений формулы алгебры предикатов рекомендуется приводить к нормальной форме. Если в алгебре высказываний приняты две нормальные формы (ДНФ – дизъюнктивная и КНФ – конъюнктивная), то в алгебре предикатов – одна предваренная (пренексная) нормальная форма (ПНФ), суть которой сводится к разделению формулы на две части: кванторную и бескванторную. Для этого все кванторы формулы выносят влево, используя законы и правила алгебры предикатов.
В результате этих алгебраических преобразований может быть получена формула вида:  x 1  x 2 ¼Â xn (M), где ÂÎ{"; $}, а М – матрица формулы. Кванторную часть формулы  x 1  x 2 ¼Â xn иногда называют префиксом ПНФ.
В последующем матрицу формулы преобразуют к виду КНФ, что облегчает механизм вывода по методу резолюции.
Примеры.
1. F =$ x " y ((P 21.(х, y)Ú 
) Ù P 3 (y)) формула, приведенная к ПНФ; F =" x (P 21.(х, y)Ú$ x (P 2 (х)) Ù$ y (P 3 (y)) формула, неприведенная к ПНФ.
2. " x (P 1.(х))Ù" x (P 2(x))=" x (P 1.(х) Ù P 2(x)) слева от знака равенства формула, неприведенная к ПНФ, а справа, равносильная ей формула, но приведенная к ПНФ.
