Korisnik:VisnjaNovakovic/Konjuktivna normalna forma

Konjuktivna normalna forma

Konjuktivna normalna forma je način izražavanja formule u Bulovoj logici. Formula je u KNF ako predstavlja konjukciju klauzula, gde svaka klauzula predstavlja disjunkciju literala. Jedini iskazi koje KNF može da sadrži su I (∧), ILI (∨) i NE (¬). Ima primenu u automatskom dokazivanju teorema.

Primeri KNF

Primeri formula u KNF:

• (A∨B)∧(¬A∨C)
• (A∨B∨C)∧(¬A∨¬B)∧(C∨¬C)
• ¬A∧(B∨C)

Konverzija formule u KNF

Svaka iskazna formula može da se transformiše u KNF.

Koraci u konverziji formule u KNF:

• Eliminisanje implikacija, ekvivalencija i isključivih disjunkcija

A→B прелази у ¬A∨B
A↔B прелази у (A∧B)∨(¬A∧¬B)
A⊕B прелази у (A∨B)∧¬(A∧B)

• Negacije se pomeraju unutar zagrada kako bi se javljale samo kao deo literala. Eliminišu se dvostruke negacije i primenjuju se De Morganovi zakoni.
• Skolemizacija formule
• Eliminacija univerzalnih kvantifikatora
• Primena zakona distributivnosti na konjukcije i disjunkcije

Дистрибутивност преко дисјункције: A∨(B∧C)≡(A∨B)∧(A∨C)
Дистрибутивност преко конјукције: A∧(B∨C)≡(A∧B)∨(A∧C)

Primer konverzije formule u KNF

Data je sledeća formula:

¬((¬A→¬B)∧¬C)

Eliminiše se implikacija:

¬((¬¬A∨¬B)∧¬C)

Eliminišu se dvostruke negacije:

¬((A∨¬B)∧¬C)

Negacija se pomera unutar zagrade primenom De Morganovih zakona:

¬(A∨¬B)∨¬¬C

Eliminišu se dvostruke negacije:

¬(A∨¬B)∨C

Negacija se pomera unutar zagrade primenom De Morganovih zakona:

(¬A∧¬¬B)∨C

Eliminišu se dvostruke negacije:

(¬A∧B)∨C

Primena zakona distributivnosti preko disjunkcije:

(¬A∨C)∧(B∨C)

Dobijena formula je u konjuktivnoj normalnoj formi.