Disjunktiv normalform

Disjunktiv normalform (DNF) er en standardisert (eller normalisert) utsagnslogisk formel som er en disjunksjon av konjunksjoner av literaler. Den kan også beskrives som en ELLER av OG, eller en sum av produkt, eller (i filosofisk logikk) et kluster konsept. Som en normalform er formen viktig i automatisert theorem testing.

De eneste utsagnslogiske konnektivene i en DNF-formel er og, eller og ikke, og ikke kan bare forekomme i literalene. Følgende formler er på DNF:

$A\lor B$

$(A\land B)\lor C$

$(A\land \neg B\land \neg C)\lor (\neg D\land E)\lor F$

Følgende formler er ikke på DNF:

$\neg (A\lor B)$ – $\neg$ forekommer utenfor en $\lor$

$A\lor (B\land (C\lor D))$ – $\lor$ er nestet inne i en $\land$

Man kan omforme enhver utsagnslogisk formel til DNF ved å bruke logiske ekvivalenser som eliminering av dobbel negasjon, De Morgans lover og distribusjonsloven. I enkelte tilfeller kan imidlertid en omforming til DNF føre til en eksponensiell økning i størrelsen på formelen.

Normalformer i logikk er viktige for bl.a. automatisk teorembevising.

Se også

• Konjunktiv normalform