title: Forme normale négative
text: # Forme normale négative
  
  En logique mathématique, une formule est dite être en forme normale négative (abrégé FNN) si l'opérateur de la négation ($\lnot$, non) est appliqué uniquement aux variables, et les seuls opérateurs booléens autorisés sont la conjonction ($\land$, et) et la disjonction ($\lor$, ou).
  
  La forme normale négative n'est pas une forme canonique, par exemple, $a\land (b\lor \lnot c)$ et $(a\land b)\lor (a\land \lnot c)$ sont équivalentes, et sont toutes deux en forme normale négative.
  
  En logique classique et beaucoup de logiques modales, chaque formule peut être représentée dans cette forme, par le remplacement des implications et des équivalences par leurs définitions, en utilisant les lois de De Morgan, et en éliminant les doubles négations. Ce processus peut être représenté en utilisant les règles de réécriture suivantes (Handbook of Automated Reasoning 1, p. 204.):
  
      $A\Rightarrow B\to \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 \exists xA\to \forall x\lnot A$
      $\lnot \forall xA\to \exists x\lnot A$
  
  Une formule en forme normale négative peut être mise sous la forme normale conjonctive ou en forme normale disjonctive en appliquant la distributivité.
  
  ## Exemples et contre-exemples
  
  Les formules suivantes sont en forme normale négative:
  
      $(A\vee B)\wedge C$
      $(A\wedge (\lnot B\vee C)\wedge \lnot C)\vee D$
      $A\vee \lnot B$
      $A\wedge \lnot B$
  
  Le premier exemple est également sous forme normale conjonctive et les deux derniers sont à la fois en forme normale conjonctive et disjonctive, mais le second exemple ne l'est pas.
  
  Les formules suivantes ne sont pas en forme normale négative:
  
      $A\Rightarrow B$
      $\lnot (A\vee B)$
      $\lnot (A\wedge B)$
      $\lnot (A\vee \lnot C)$
  
  Celles-ci sont cependant respectivement équivalentes aux formules suivantes en forme normale négative :
  
      $\lnot A\vee B$
      $\lnot A\wedge \lnot B$
      $\lnot A\vee \lnot B$
      $\lnot A\wedge C$
  