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

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

Нормальная форма отрицания не является канонической формой: например, и эквивалентны, и обе находятся в нормальной форме отрицания.${\ Displaystyle а \ земля (б \ лор \ lnot с)}$${\ Displaystyle (а \ земля Ь) \ лор (а \ земля \ lnot с)}$

В классической логике и многих модальных логиках каждая формула может быть приведена в эту форму, заменяя импликации и эквивалентности их определениями, используя законы Де Моргана, чтобы подтолкнуть отрицание внутрь, и исключив двойное отрицание. Этот процесс можно представить с помощью следующих правил перезаписи ( Handbook of Automated Reasoning 1, p. 204):

${\ Displaystyle {\ begin {align} A \ Rightarrow B ~ & \ к ~ \ 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 \ существует xA ~ & \ to ~ \ forall x \ lnot A \\\ lnot \ forall xA ~ & \ to ~ \ exists x \ lnot A \ end {выравнивается}}}$

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

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

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

Примеры и контрпримеры [ править ]

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

${\ Displaystyle (А \ Ви В) \ клин С}$

${\ Displaystyle (A \ клин (\ lnot B \ vee C) \ клин \ lnot C) \ vee D}$

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

${\ Displaystyle A \ клин \ lnot B}$

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

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

${\ Displaystyle A \ Rightarrow B}$

${\ Displaystyle \ lnot (А \ Ви Б)}$

${\ Displaystyle \ lnot (А \ клин В)}$

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

Ссылки [ править ]

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

Внешние ссылки [ править ]

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