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

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

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

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

$A\Rightarrow B\to \lnot A\lor B$

$\lnot (A\lor B)\to \lnot A\land \lnot B$

$\lnot (A\land B)\to \lnot A\lor \lnot B$

$\lnot \lnot A\to A$

$\lnot \exists xA\to \forall x\lnot A$

$\lnot \forall xA\to \exists x\lnot A$

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

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

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

$(A\vee B)\wedge C$

$(A\wedge (\lnot B\vee C)\wedge \lnot C)\vee D$

$A\vee \lnot B$

$A\wedge \lnot B$

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

$A\Rightarrow B$

$\lnot (A\vee B)$

$\lnot (A\wedge B)$

$\lnot (A\vee \lnot C)$

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

$\lnot A\vee B$

$\lnot A\wedge \lnot B$

$\lnot A\vee \lnot B$

$\lnot 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