Заперечення нормальної форми

В математичній логіці, формула є запереченням нормальної форми, якщо заперечення утворене оператором ($\mathrm{\neg }$, не), який може бути записаний або сам, або з логічними операторами: кон'юнкції ($\wedge$, і) і диз'юнкція ($\vee$, або).

Заперечення нормальної форми не є канонічною формою: наприклад, $a\wedge (b\vee \mathrm{\neg }c)$ і $(a\wedge b)\vee (a\wedge \mathrm{\neg }c)$ є еквівалентними, і обидва знаходяться в запереченні нормальній формі.

У класичній логіці і багатьох видах модальної логіки, кожна формула може бути приведена в цю форму, замінивши наслідки і еквівалентності їх визначеннями, використовуючи закони де Моргана, щоб підштовхнути запереченням до середини, і усунення подвійних заперечень. Цей процес можна представити за допомогою наступних правил переписування (Handbook of Automated Reasoning 1, с 204.):

$A\Rightarrow B\to \mathrm{\neg }A\vee B$

$\mathrm{\neg }(A\vee B)\to \mathrm{\neg }A\wedge \mathrm{\neg }B$

$\mathrm{\neg }(A\wedge B)\to \mathrm{\neg }A\vee \mathrm{\neg }B$

$\mathrm{\neg }\mathrm{\neg }A\to A$

$\mathrm{\neg }\mathrm{\exists }xA\to \mathrm{\forall }x\mathrm{\neg }A$

$\mathrm{\neg }\mathrm{\forall }xA\to \mathrm{\exists }x\mathrm{\neg }A$

Формула заперечення нормальної форми може бути використана в більш сильному КНФ або ДНФ шляхом застосування дистрибутивності.

Приклади і контрприклади

Наступні формули усі в запереченні:

$(A\vee B)\wedge C$

$(A\wedge (\mathrm{\neg }B\vee C)\wedge \mathrm{\neg }C)\vee D$

$A\vee \mathrm{\neg }B$

$A\wedge \mathrm{\neg }B$

Перший приклад в кон'юнктивній нормальній формі, а останні два в обох КНФ і ДНФ, але другий приклад ні в одному. Наступні формули не в запереченні:

$A\Rightarrow B$

$\mathrm{\neg }(A\vee B)$

$\mathrm{\neg }(A\wedge B)$

$\mathrm{\neg }(A\vee \mathrm{\neg }C)$

Вони відповідно еквівалентні такими формулами з запереченням як:

$\mathrm{\neg }A\vee B$

$\mathrm{\neg }A\wedge \mathrm{\neg }B$

$\mathrm{\neg }A\vee \mathrm{\neg }B$

$\mathrm{\neg }A\wedge C$

Джерела

• Alan J.A. Robinson and Andrei Voronkov, Handbook of Automated Reasoning 1:203ff (2001) ISBN 0444829490.

Посилання

• Java applet for converting logical formula to Negation Normal Form, showing laws used