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

• Формула имеет нормальную форму отрицания (NNF) в математической логике, если оператор отрицания применяется только к переменным и разрешены только conjunction и дизъюнкция. 
• Нормальная форма отрицания не является канонической формой, но эквивалентна другим формулам в NNF. 
• В классической логике и модальных логиках формулы могут быть приведены к NNF путем замены импликаций и эквивалентностей, использования законов Де Моргана и устранения двойных отрицаний. 
• Преобразование в NNF может увеличить размер формулы линейно, но количество повторений отрицания ограничено длиной исходной формулы. 
• Формулы в отрицательной NNF могут быть переведены в более сильную конъюнктивную или дизъюнктивную NNF с помощью дистрибутивности. 
• Повторное применение принципа распределения может привести к экспоненциальному увеличению размера формулы. 
• В классической логике высказываний преобразование в NNF не влияет на вычислительные свойства формул.