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

Логическая формула с НЕ только для переменных

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

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

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

${\displaystyle {\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}}}$

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

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

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

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

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

${\displaystyle {\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}}}$

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

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

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

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

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

Смотрите также

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

Примечания

1. Робинсон и Воронков 2001, с. 204.

Ссылки

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

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

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