Negatie-normaalvorm

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

Negatie-normaalvorm is geen standaard vorm: bijvoorbeeld $a\land (b\lor \lnot c)$ en $(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 (Handbook of Automated Reasoning 1, p. 204):

${\begin{aligned}A\to B&~\Rightarrow ~\lnot A\lor B\\A\Leftrightarrow B&~\Rightarrow ~(\lnot A\lor B)\land (A\lor \lnot 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 geldt de $\to$ symbool geeft de logische implicatie aan van de formule die wordt herschreven. Het symbool $\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 $\land$ En $\lor$ is ongewijzigd, en het aantal keren dat $\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-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:

${\begin{aligned}(A&\vee B)\wedge C\\(A&\wedge (\lnot B\vee C)\wedge \lnot C)\vee D\\A&\vee \lnot B\\A&\wedge \lnot B\end{aligned}}$

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:

${\begin{aligned}A&\to B\\\lnot (A&\vee B)\\\lnot (A&\wedge B)\\\lnot (A&\vee \lnot C)\end{aligned}}$

Ze zijn echter respectievelijk gelijkwaardig aan de volgende formules in ontkenningsnormaalvorm:

${\begin{aligned}\lnot A&\vee B\\\lnot A&\wedge \lnot B\\\lnot A&\vee \lnot B\\\lnot A&\wedge C\end{aligned}}$

Referenties

• John Alan Robinson en Andrei Voronkov, Handbook of Automated Reasoning 1:203ff (2001) ISBN 0444829490.

Externe links

• Java-applet voor het converteren van logische formules naar Negation Normal Form, waarbij de gebruikte wetten worden weergegeven