Нормальная форма отрицания

В математической логике формула находится в нормальной форме отрицания (NNF), если оператор отрицания ( $\lnot$, not ) применяется только к переменным, а единственными разрешенными логическими операторами являются конъюнкция ( $\land$, и ) и дизъюнкцию ( $\lor$, или ).

Нормальная форма отрицания не является канонической формой : например, $a\land (b\lor \lnot c)$ и $(a\land b)\lor (a\land \lnot c)$ эквивалентны и оба находятся в отрицательной нормальной форме.

В классической логике и во многих модальных логиках каждую формулу можно привести к этой форме, заменив импликации и эквивалентности их определениями, используя законы Де Моргана для продвижения отрицания внутрь и устранения двойных отрицаний. Этот процесс можно представить с помощью следующих правил перезаписи :

${\begin{aligned}A\Rightarrow B&~\to ~\lnot A\lor B\\A\Leftrightarrow B&~\to ~(\lnot A\lor B)\land (A\lor \lnot 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\end{aligned}}$

(В настоящих правилах $\Rightarrow$ символ указывает на логическое значение переписываемой формулы, а $\to$ это операция перезаписи.)

Преобразование в нормальную форму отрицания может увеличить размер формулы только линейно: количество вхождений атомарных формул остается прежним, общее количество вхождений $\land$ и $\lor$ остается неизменным, а количество вхождений $\lnot$ в нормальной форме ограничена длиной исходной формулы.

Формулу в нормальной форме отрицания можно привести к более сильной конъюнктивной нормальной форме или дизъюнктивной нормальной форме, применив дистрибутивность . Повторное применение распределительности может экспоненциально увеличить размер формулы. В классической логике высказываний преобразование к нормальной форме отрицания не влияет на вычислительные свойства: проблема выполнимости продолжает оставаться NP-полной , а проблема достоверности продолжает быть ко-NP-полной . Для формул в конъюнктивной нормальной форме проблема применимости разрешима за полиномиальное время, а для формул в дизъюнктивной нормальной форме проблема выполнимости разрешима за полиномиальное время.

Примеры и контрпримеры

Все следующие формулы имеют отрицательную нормальную форму:

${\begin{aligned}(A&\vee B)\wedge C\\(A&\wedge (\lnot B\vee C)\wedge \lnot C)\vee D\\A&\vee \lnot B\\A&\wedge \lnot B\end{aligned}}$

Первый пример также находится в конъюнктивной нормальной форме , а два последних — как в конъюнктивной нормальной форме , так и в дизъюнктивной нормальной форме , но второй пример не находится ни в одной из них.

Следующие формулы не находятся в отрицательной нормальной форме:

${\begin{aligned}A&\Rightarrow B\\\lnot (A&\vee B)\\\lnot (A&\wedge B)\\\lnot (A&\vee \lnot C)\end{aligned}}$

Однако они соответственно эквивалентны следующим формулам в нормальной форме отрицания:

${\begin{aligned}\lnot A&\vee B\\\lnot A&\wedge \lnot B\\\lnot A&\vee \lnot B\\\lnot A&\wedge C\end{aligned}}$

См. также

• Конъюнктивная нормальная форма
• Дизъюнктивная нормальная форма

Ссылки

• Робинсон, Джон Алан ; Воронков, Андрей , ред. (2001). Справочник по автоматизированному рассуждению . Том. 1. Пресс-центр Массачусетского технологического института . стр. 203 и далее. ISBN  0444829490 .

Внешние ссылки

• Java-апплет для преобразования логической формулы в нормальную форму отрицания, показывающий используемые законы