title: Negatie-normaalvorm
text: In de logica is een formule in negatie-normaalvorm (NNV) als de negatie-operator (, ) alleen wordt toegepast op atomaire formules en waarbij de enige andere toegestane Booleaanse operatoren conjunctie (, ) en disjunctie (, ) zijn.
  
  Negatie-normaalvorm is geen standaard vorm: bijvoorbeeld  en  zijn gelijkwaardig, en zijn beide in de negatie-normaalvorm.
  
  In de predicatenlogica en veel modale logica's kan elke formule in deze vorm worden herschreven door implicaties en equivalenties te vervangen met hun definities, door de wetten van De Morgan te gebruiken om de negaties naar binnen te werken en door dubbele negaties te elimineren. Dit proces kan worden weergegeven met behulp van de volgende herschrijfregels (Handbook of Automated Reasoning 1, p. 204):
   
  
  (In deze regels geldt de  symbool geeft de logische implicatie aan van de formule die wordt herschreven. Het symbool  geeft de herschrijfbewerking aan.)
  
  Transformatie naar een negatie-normaalvorm kan de grootte van een formule alleen lineair vergroten: het aantal keren dat atomaire formules voorkomen, blijft hetzelfde, het totale aantal keren dat  En  is ongewijzigd, en het aantal keren dat  in de normaalvorm wordt begrensd door de lengte van de oorspronkelijke formule.
  
  Een formule in de negatie-normaalvorm kan in de sterkere conjunctieve normaalvorm of disjunctieve normaalvorm worden geplaatst door distributiviteit toe te passen. Herhaalde toepassing van distributiviteit kan de grootte van een formule exponentieel vergroten. In de propositielogica heeft transformatie naar de negatie-normaalvorm geen invloed op de computationele eigenschappen: het vervulbaarheidsprobleem blijft NP-volledig, en het validiteitsprobleem blijft co-NP-compleet. Voor formules in de conjunctieve normaalvorm is het validiteitsprobleem oplosbaar in polynomiale tijd, en voor formules in disjunctieve normaalvorm is het vervulbaarheidsprobleem oplosbaar in polynomiale tijd.
  
  Voorbeelden en tegenvoorbeelden 
  De volgende formules zijn allemaal in negatie-normaalvorm:
   
  
  Het eerste voorbeeld is ook in de conjunctieve normaalvorm en de laatste twee zijn zowel in de conjunctieve normaalvorm als in de disjunctieve normaalvorm, maar het tweede voorbeeld is in geen van beide.
  
  De volgende formules zijn niet in de negatie-normaalvorm:
   
  
  Ze zijn echter respectievelijk gelijkwaardig aan de volgende formules in ontkenningsnormaalvorm:
  
  Referenties 
   John Alan Robinson en Andrei Voronkov, Handbook of Automated Reasoning 1:203ff  (2001) .
  
  Externe links 
   Java-applet voor het converteren van logische formules naar Negation Normal Form, waarbij de gebruikte wetten worden weergegeven
  
  Predicatenlogica
  Logica
  Theoretische informatica