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

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

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

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

${\displaystyle A\Rightarrow B\to \lnot A\lor B}$

${\displaystyle \lnot (A\lor B)\to \lnot A\land \lnot B}$

${\displaystyle \lnot (A\land B)\to \lnot A\lor \lnot B}$

${\displaystyle \lnot \lnot A\to A}$

${\displaystyle \lnot \exists xA\to \forall x\lnot A}$

${\displaystyle \lnot \forall xA\to \exists x\lnot A}$

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