Предваренная нормальная форма

Для облегчения анализа сложных суждений формулы алгебры предикатов рекомендуется приводить к нормальной форме. Если в алгебре высказываний приняты две нормальные формы (ДНФ — дизъюнктивная и КНФ -конъюнктивная), то в алгебре предикатов — одна предваренная нормальная форма (ПНФ), суть которой сводится к разделению формулы на две части: кванторную  и безкванторную. Для этого все кванторы формулы выносят влево, используя законы и правила алгебры предикатов.

В результате этих алгебраических преобразова­ний может быть получена формула вида: Âx1 Âx2 ¼Âxn(M), где ÂÎ{«; $} , а М – матрица формулы. Кванторную часть формулы Âx1 Âx2 ¼Âxnиногда называют префиксом ПНФ.

В последующем матрицу форму­лы преобразуют к виду КНФ, что облегчает механизм по принципу резолюции.

Пример: 

F=$x»y((P21.(х; y)ÚùP2.(х))&P3(y)) формула, приведенная к ПНФ; F=»x(P21.(х; y)Ú$x(P2 (х))&$y(P3 (y)) формула, неприведенная к ПНФ.

«x(P1.(х)) &»x(P2(x))=»x(P1.(х) &P2(x)) слева от знака равенства формула, неприведенная к ПНФ, а справа, равносильная ей формула, но приведенная к ПНФ.

 

Логика - доступно для всех