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

В математичній логіці, формула є запереченням нормальної форми, якщо заперечення утворене оператором (${\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}$

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

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

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

${\displaystyle (A\vee B)\wedge C}$

${\displaystyle (A\wedge (\lnot B\vee C)\wedge \lnot C)\vee D}$

${\displaystyle A\vee \lnot B}$

${\displaystyle A\wedge \lnot B}$

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

${\displaystyle A\Rightarrow B}$

${\displaystyle \lnot (A\vee B)}$

${\displaystyle \lnot (A\wedge B)}$

${\displaystyle \lnot (A\vee \lnot C)}$

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

${\displaystyle \lnot A\vee B}$

${\displaystyle \lnot A\wedge \lnot B}$

${\displaystyle \lnot A\vee \lnot B}$

${\displaystyle \lnot A\wedge C}$

Джерела

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

Посилання

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