Disjunktiv normalform

Fra Wikipedia, den frie encyklopedi
Gå til: navigasjon, søk

En utsagnslogisk formel er på disjunktiv normalform (DNF) hvis den er en disjunksjon av konjunksjoner av literaler. 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å[rediger | rediger kilde]