Negatie-normaalvorm

In de logica is een formule in negatie-normaalvorm (NNV) als de negatie-operator (${\displaystyle \lnot }$, not) alleen wordt toegepast op atomaire formules en waarbij de enige andere toegestane booleaanse operatoren conjunctie (${\displaystyle \land }$, and) en disjunctie (${\displaystyle \lor }$, or) zijn.

Negatie-normaalvorm is geen standaardvorm: bijvoorbeeld ${\displaystyle a\land (b\lor \lnot c)}$ en ${\displaystyle (a\land b)\lor (a\land \lnot c)}$ 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^[1]:

${\displaystyle {\begin{aligned}A\to B&~\Rightarrow ~\lnot A\lor B\\\lnot (A\lor B)&~\Rightarrow ~\lnot A\land \lnot B\\\lnot (A\land B)&~\Rightarrow ~\lnot A\lor \lnot B\\\lnot \lnot A&~\Rightarrow ~A\\\lnot \exists xA&~\Rightarrow ~\forall x\lnot A\\\lnot \forall xA&~\Rightarrow ~\exists x\lnot A\end{aligned}}}$

In deze regels geeft het ${\displaystyle \to }$-symbool de logische implicatie aan van de formule die wordt herschreven. Het symbool ${\displaystyle \Rightarrow }$ 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 ${\displaystyle \land }$ En ${\displaystyle \lor }$ is ongewijzigd, en het aantal keren dat ${\displaystyle \lnot }$ 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-volledig. 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.

1. ↑ John Alan Robinson en Andrei Voronkov, Handbook of Automated Reasoning 1 (2001) ISBN 0444829490