Konjunktiv normal form - Conjunctive normal form

I boolsk logikk er en formel i konjunktiv normal form ( CNF ) eller klausulær normal form hvis det er en sammenheng av en eller flere ledd , der en klausul er en disjunksjon av bokstavene ; ellers sagt, det er et produkt av summer eller et OG av OR . Som en kanonisk normalform er den nyttig i automatisert teoremvisning og kretsteori .

Alle konjunksjoner av bokstaver og alle disjunksjoner av bokstavene er i CNF, ettersom de kan sees på som konjunksjoner av henholdsvis enbokstav og konjunksjoner av en enkelt klausul. Som i den disjunktive normale formen (DNF), er de eneste proposisjonelle forbindelsene en formel i CNF kan inneholde, og , eller , og ikke . Ikke -operatøren kan bare brukes som en del av en bokstavelig, noe som betyr at den bare kan gå foran en proposisjonsvariabel eller et predikatsymbol .

I automatisert teorem som beviser, brukes begrepet " klausulær normalform " ofte i en smalere forstand, noe som betyr en spesiell fremstilling av en CNF -formel som et sett med bokstaver.

Eksempler og ikke-eksempler

Alle følgende formler i variablene , og er i konjunktiv normal form: ${\ displaystyle A, B, C, D, E}$${\ displaystyle F}$

• ${\ displaystyle (A \ lor \ neg B \ lor \ neg C) \ land (\ neg D \ lor E \ lor F)}$
• ${\ displaystyle (A \ lor B) \ land (C)}$
• ${\ displaystyle (A \ lor B)}$
• ${\ displaystyle (A)}$

For klarhets skyld er de disjunktive klausulene skrevet inne i parentes ovenfor. I disjunktiv normal form med parenteserte konjunktivklausuler, er det siste tilfellet det samme, men det nest siste er . Konstantene sanne og usanne er angitt med den tomme konjunkten og en klausul bestående av den tomme disjunkten, men er normalt skrevet eksplisitt. ${\ displaystyle (A) \ lor (B)}$

Følgende formler er ikke i konjunktiv normal form:

• ${\ displaystyle \ neg (B \ lor C)}$, siden en OR er nestet i et NOT
• ${\ displaystyle (A \ land B) \ lor C}$
• ${\ displaystyle A \ land (B \ lor (D \ land E))}$, siden en OG er nestet i en OR

Hver formel kan skrives tilsvarende som en formel i konjunktiv normalform. De tre ikke-eksemplene i CNF er:

• ${\ displaystyle (\ neg B) \ land (\ neg C)}$
• ${\ displaystyle (A \ lor C) \ land (B \ lor C)}$
• ${\ displaystyle (A) \ land (B \ lor D) \ land (B \ lor E).}$

Konvertering til CNF

Hver proposisjonsformel kan konverteres til en ekvivalent formel som er i CNF. Denne transformasjonen er basert på regler om logiske ekvivalenser : eliminering av dobbel negasjon , De Morgans lover og distribusjonsloven .

Siden alle proposisjonsformler kan konverteres til en ekvivalent formel i konjunktiv normalform, er bevis ofte basert på antagelsen om at alle formler er CNF. Imidlertid kan denne konverteringen til CNF i noen tilfeller føre til en eksponentiell eksplosjon av formelen. For eksempel overfører følgende ikke-CNF-formel til CNF en formel med setninger: ${\ displaystyle 2^{n}}$

${\ displaystyle (X_ {1} \ kile Y_ {1}) \ vee (X_ {2} \ kile Y_ {2}) \ vee \ dots \ vee (X_ {n} \ kile Y_ {n}).}$

Spesielt er den genererte formelen:

${\ displaystyle (X_ {1} \ vee X_ {2} \ vee \ cdots \ vee X_ {n}) \ wedge (Y_ {1} \ vee X_ {2} \ vee \ cdots \ vee X_ {n}) \ kil (X_ {1} \ vee Y_ {2} \ vee \ cdots \ vee X_ {n}) \ wedge (Y_ {1} \ vee Y_ {2} \ vee \ cdots \ vee X_ {n}) \ wedge \ cdots \ wedge (Y_ {1} \ vee Y_ {2} \ vee \ cdots \ vee Y_ {n}).}$

Denne formelen inneholder setninger; hver klausul inneholder enten eller for hver . ${\ displaystyle 2^{n}}$${\ displaystyle X_ {i}}$${\ displaystyle Y_ {i}}$${\ displaystyle i}$

Det finnes transformasjoner til CNF som unngår en eksponentiell økning i størrelse ved å bevare tilfredsheten i stedet for ekvivalens . Disse transformasjonene vil garantert bare øke størrelsen på formelen lineært, men introdusere nye variabler. For eksempel kan formelen ovenfor transformeres til CNF ved å legge til variabler som følger: ${\ displaystyle Z_ {1}, \ ldots, Z_ {n}}$

${\ displaystyle (Z_ {1} \ vee \ cdots \ vee Z_ {n}) \ wedge (\ neg Z_ {1} \ vee X_ {1}) \ wedge (\ neg Z_ {1} \ vee Y_ {1} ) \ wedge \ cdots \ wedge (\ neg Z_ {n} \ vee X_ {n}) \ wedge (\ neg Z_ {n} \ vee Y_ {n}).}$

En tolkning tilfredsstiller denne formelen bare hvis minst en av de nye variablene er sann. Hvis denne variabelen er , så er begge deler og også sanne. Dette betyr at hver modell som tilfredsstiller denne formelen også tilfredsstiller den opprinnelige. På den annen side tilfredsstiller bare noen av modellene av den opprinnelige formelen denne: siden de ikke er nevnt i den opprinnelige formelen, er deres verdier irrelevante for å tilfredsstille den, noe som ikke er tilfelle i den siste formelen. Dette betyr at den opprinnelige formelen og resultatet av oversettelsen er equisatisfiable men ikke ekvivalent . ${\ displaystyle Z_ {i}}$${\ displaystyle X_ {i}}$${\ displaystyle Y_ {i}}$${\ displaystyle Z_ {i}}$

En alternativ oversettelse, Tseitin -transformasjonen , inkluderer også klausulene . Med disse klausulene innebærer formelen ; denne formelen blir ofte sett på som "definere" for å være et navn på . ${\ displaystyle Z_ {i} \ vee \ neg X_ {i} \ vee \ neg Y_ {i}}$${\ displaystyle Z_ {i} \ equiv X_ {i} \ kil Y_ {i}}$${\ displaystyle Z_ {i}}$${\ displaystyle X_ {i} \ kile Y_ {i}}$

Første ordens logikk

I første ordens logikk kan konjunktiv normal form tas videre for å gi den klausulære normalformen til en logisk formel, som deretter kan brukes til å utføre første ordens oppløsning . I oppløsningsbasert, automatisk teorem-bevising, en CNF-formel

${\ displaystyle (}$

${\ displaystyle l_ {11}}$

${\ displaystyle \ lor}$

${\ displaystyle \ ldots}$

${\ displaystyle \ lor}$

${\ displaystyle l_ {1n_ {1}}}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ ldots}$

${\ displaystyle \ land}$

${\ displaystyle (}$

${\ displaystyle l_ {m1}}$

${\ displaystyle \ lor}$

${\ displaystyle \ ldots}$

${\ displaystyle \ lor}$

${\ displaystyle l_ {mn_ {m}}}$

${\ displaystyle)}$

, med bokstavene, er vanligvis representert som et sett med sett ${\ displaystyle l_ {ij}}$

${\ displaystyle \ {}$

${\ displaystyle \ {}$

${\ displaystyle l_ {11}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle l_ {1n_ {1}}}$

${\ displaystyle \}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle \ {}$

${\ displaystyle l_ {m1}}$

${\ displaystyle,}$

${\ displaystyle \ ldots}$

${\ displaystyle,}$

${\ displaystyle l_ {mn_ {m}}}$

${\ displaystyle \}}$

${\ displaystyle \}}$

.

Se et eksempel nedenfor .

Beregningskompleksitet

Et viktig sett med problemer i beregningskompleksitet innebærer å finne tildelinger til variablene i en boolsk formel uttrykt i konjunktiv normal form, slik at formelen er sann. Den k -SAT problem er problemet med å finne en tilfredsstillende tilordning til en boolsk formel uttrykt i CNF hvor hver motsetninger inneholder høyst k variabler. 3-SAT er NP-komplett (som alle andre k -SAT-problemer med k > 2) mens 2-SAT er kjent for å ha løsninger i polynomtid . Som en konsekvens er oppgaven med å konvertere en formel til en DNF , bevare tilfredsheten, NP-hard ; dobbeltkrum , konvertering til CNF, bevare gyldighet , er også NP-hard; Derfor er ekvivalensbevarende konvertering til DNF eller CNF igjen NP-hard.

Typiske problemer i dette tilfellet involverer formler i "3CNF": konjunktiv normalform med ikke mer enn tre variabler per konjunkt. Eksempler på slike formler som oppstår i praksis kan være veldig store, for eksempel med 100 000 variabler og 1 000 000 konjunkturer.

En formel i CNF kan konverteres til en equisatisfiable formel i " k CNF" (for k ≥3) ved å erstatte hver konjunkt med mer enn k variabler med to konjunksjoner og med Z en ny variabel, og gjenta så ofte som nødvendig. ${\ displaystyle X_ {1} \ vee \ cdots \ vee X_ {k} \ vee \ cdots \ vee X_ {n}}$${\ displaystyle X_ {1} \ vee \ cdots \ vee X_ {k-1} \ vee Z}$${\ displaystyle \ neg Z \ vee X_ {k} \ cdots \ vee X_ {n}}$

Konvertering fra første ordens logikk

For å konvertere første ordens logikk til CNF:

1. Konverter til negativ form .
   1. Eliminer implikasjoner og ekvivalenser: erstatt gjentatte ganger med ; erstatte med . Etter hvert vil dette eliminere alle forekomster av og .${\ displaystyle P \ rightarrow Q}$${\ displaystyle \ lnot P \ lor Q}$${\ displaystyle P \ venstrehøyre pil Q}$${\ displaystyle (P \ lor \ lnot Q) \ land (\ lnot P \ lor Q)}$${\ displaystyle \ rightarrow}$${\ displaystyle \ leftrightarrow}$
   2. Flytt NOTs innover ved gjentatte ganger å bruke De Morgans lov . Spesielt erstatt med ; erstatte med ; og bytt ut med ; erstatte med ; med . Etter det kan a bare oppstå umiddelbart før et predikatsymbol.${\ displaystyle \ lnot (P \ lor Q)}$${\ displaystyle (\ lnot P) \ land (\ lnot Q)}$${\ displaystyle \ lnot (P \ land Q)}$${\ displaystyle (\ lnot P) \ lor (\ lnot Q)}$${\ displaystyle \ lnot \ lnot P}$${\ displaystyle P}$${\ displaystyle \ lnot (\ forall xP (x))}$${\ displaystyle \ exist x \ lnot P (x)}$${\ displaystyle \ lnot (\ exist xP (x))}$${\ displaystyle \ forall x \ lnot P (x)}$${\ displaystyle \ lnot}$
2. Standardiser variabler
   1. For setninger som bruker samme variabelnavn to ganger, endrer du navnet på en av variablene. Dette unngår forvirring senere når du slipper kvantifiseringer. Den blir for eksempel omdøpt til .${\ displaystyle (\ forall xP (x)) \ lor (\ eksisterer xQ (x))}$${\ displaystyle \ forall x [\ exist y \ mathrm {Animal} (y) \ land \ lnot \ mathrm {Loves} (x, y)] \ lor [\ exist y \ mathrm {Loves} (y, x)] }$${\ displaystyle \ forall x [\ exist y \ mathrm {Animal} (y) \ land \ lnot \ mathrm {Loves} (x, y)] \ lor [\ exist z \ mathrm {Loves} (z, x)] }$
3. Skolemize uttalelsen
   1. Flytt kvantifiserere utover: erstatt gjentatte ganger med ; erstatte med ; erstatte med ; erstatte med . Disse erstatningene bevarer ekvivalens, siden det forrige trinnet for standardisering av standardisering sørget for at det ikke forekommer i . Etter disse erstatninger, kan en kvantifiserings forekomme bare på den første prefiks av formelen, men aldri i en , eller .${\ displaystyle P \ land (\ forall xQ (x))}$${\ displaystyle \ forall x (P \ land Q (x))}$${\ displaystyle P \ lor (\ forall xQ (x))}$${\ displaystyle \ forall x (P \ lor Q (x))}$${\ displaystyle P \ land (\ eksisterer xQ (x))}$${\ displaystyle \ finnes x (P \ land Q (x))}$${\ displaystyle P \ lor (\ eksisterer xQ (x))}$${\ displaystyle \ finnes x (P \ lor Q (x))}$${\ displaystyle x}$${\ displaystyle P}$${\ displaystyle \ lnot}$${\ displaystyle \ land}$${\ displaystyle \ lor}$
   2. Gjentatte ganger erstatte med , hvor er et nytt -ary funksjonssymbol, en såkalt " Skolem -funksjon ". Dette er det eneste trinnet som bare bevarer tilfredshet fremfor ekvivalens. Det eliminerer alle eksistensielle kvantifikatorer.${\ displaystyle \ forall x_ {1} \ ldots \ forall x_ {n} \; \ finnes y \; P (y)}$${\ displaystyle \ forall x_ {1} \ ldots \ forall x_ {n} \; P (f (x_ {1}, \ ldots, x_ {n}))}$${\ displaystyle f}$${\ displaystyle n}$
4. Slipp alle universelle tall.
5. Fordel ORs innover ANDs: erstatt gjentatte ganger med .${\ displaystyle P \ lor (Q \ land R)}$${\ displaystyle (P \ lor Q) \ land (P \ lor R)}$

Som et eksempel, formelen sier "Alle som elsker alle dyr, er i sin tur elsket av noen" omdannes til CNF (og senere i klausul form i den siste linjen) som følger (utheving erstatning regel redexes i ): ${\ displaystyle {\ color {red} {\ text {red}}}}$

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ forall y}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ rightarrow}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ rightarrow}$

${\ displaystyle (}$

${\ displaystyle \ exist}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ forall y}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ rightarrow}$

${\ displaystyle (}$

${\ displaystyle \ exist}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

innen 1.1

${\ displaystyle \ forall x}$

${\ displaystyle \ color {red} \ lnot}$

${\ displaystyle (}$

${\ displaystyle {\ color {red} {\ forall y}}}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle (}$

${\ displaystyle \ exist}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

innen 1.1

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ finnes y}$

${\ displaystyle \ color {red} \ lnot}$

${\ displaystyle (}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle (}$

${\ displaystyle \ exist}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

innen 1.2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ finnes y}$

${\ displaystyle \ color {red} \ lnot}$

${\ displaystyle \ color {red} \ lnot}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle (}$

${\ displaystyle \ exist}$

${\ displaystyle y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

innen 1.2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle {\ color {red} {\ exist y}}}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle (}$

${\ displaystyle \ color {red} \ exist}$

${\ displaystyle \ color {red} y}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle y}$

${\ displaystyle, x)}$

${\ displaystyle)}$

innen 1.2

${\ displaystyle \ forall x}$

${\ displaystyle (}$

${\ displaystyle \ finnes y}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle (}$

${\ displaystyle \ color {red} \ exist}$

${\ displaystyle \ color {red} z}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

${\ displaystyle)}$

med 2

${\ displaystyle \ forall x}$

${\ displaystyle \ exist z}$

${\ displaystyle (}$

${\ displaystyle {\ color {red} {\ exist y}}}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

innen 3.1

${\ displaystyle \ forall x}$

${\ displaystyle {\ color {red} {\ exist z}}}$

${\ displaystyle \ finnes y}$

${\ displaystyle (}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle z}$

${\ displaystyle, x)}$

innen 3.1

${\ displaystyle \ forall x}$

${\ displaystyle {\ color {red} {\ exist y}}}$

${\ displaystyle (}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle y}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ lor}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

innen 3.2

${\ displaystyle (}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ land}$

${\ displaystyle \ lnot}$

${\ displaystyle \ mathrm {Loves} (x,}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

med 4

${\ displaystyle (}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

${\ displaystyle)}$

${\ displaystyle \ color {red} \ land}$

${\ displaystyle (}$

${\ displaystyle \ lnot \ mathrm {Loves} (x, f (x))}$

${\ displaystyle \ color {red} \ lor}$

${\ displaystyle \ mathrm {Loves} (g (x), x)}$

${\ displaystyle)}$

med 5

${\ displaystyle \ {}$

${\ displaystyle \ {}$

${\ displaystyle \ mathrm {Animal} (}$

${\ displaystyle f (x)}$

${\ displaystyle)}$

${\ displaystyle,}$

${\ displaystyle \ mathrm {Loves} (}$

${\ displaystyle g (x)}$

${\ displaystyle, x)}$

${\ displaystyle \}}$

${\ displaystyle,}$

${\ displaystyle \ {}$

${\ displaystyle \ lnot \ mathrm {Loves} (x, f (x))}$

${\ displaystyle,}$

${\ displaystyle \ mathrm {Loves} (g (x), x)}$

${\ displaystyle \}}$

${\ displaystyle \}}$

( klausulrepresentasjon )

Uformelt kan Skolem -funksjonen betraktes som å gi personen som er elsket, mens den gir dyret (hvis noen) som ikke elsker. Den tredje siste linjen nedenunder leser så som " elsker ikke dyret , eller annet er elsket av " . ${\ displaystyle g (x)}$${\ displaystyle x}$${\ displaystyle f (x)}$${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle f (x)}$${\ displaystyle x}$${\ displaystyle g (x)}$

Den andre siste linjen ovenfra , er CNF. ${\ displaystyle (\ mathrm {Animal} (f (x)) \ lor \ mathrm {Loves} (g (x), x)) \ land (\ lnot \ mathrm {Loves} (x, f (x)) \ lor \ mathrm {Loves} (g (x), x))}$

Merknader

Se også

• Algebraisk normalform
• Disjunktiv normal form
• Hornklausul
• Quine - McCluskey algoritme

Referanser

• J. Eldon Whitesitt (24. mai 2012). Boolsk algebra og dens applikasjoner . Courier Corporation. ISBN 978-0-486-15816-7.
• Hans Kleine Büning; Theodor Lettmann (28. august 1999). Proposisjonell logikk: fradrag og algoritmer . Cambridge University Press. ISBN 978-0-521-63017-7.
• Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits . I: Holger H. Hoos, David G. Mitchell (red.): Theory and Applications of Satisfiability Testing, 7. internasjonale konferanse, SAT 2004, Vancouver, BC, Canada, 10. – 13. Mai 2004, reviderte utvalgte artikler. Forelesningsnotater i informatikk 3542, Springer 2005, s. 183–198
• GS Tseitin: Om kompleksiteten til avledning i proposisjonell beregning . I: Slisenko, AO (red.) Strukturer i konstruktiv matematikk og matematisk logikk, del II, seminarer i matematikk (oversatt fra russisk), s. 115–125. Steklov Mathematical Institute (1968)

Eksterne linker

• "Konjunktiv normal form" , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• Java -applet for konvertering til CNF og DNF, som viser brukte lover