Konjunktivní normální forma

Technology

12 hours ago

Author

Ve výrokové logice je formule v konjunktivní normální formě (KNF nebo CNF z anglického conjunctive normal form), pokud je ve tvaru konjunkcí klauzulí, kde klauzuli definujeme jako disjunkci literálů (a je-li x výroková proměnná, tak jí určené literály jsou právě x a \neg x). Jako normální forma se používá v automatickém dokazování vět. Podobná kanonická forma se používá v teorii obvodů.

Každá konjunkce literálů a také každá disjunkce literálů je KNF, protože je můžeme považovat za konjunkci klauzulí s jedním literálem, resp. za disjunkci jedné klauzule. +more Podobně jako v disjunktivní normální formě (DNF), jediné logické spojky v KNF jsou logická spojka a, nebo a negace. Negace může být pouze součástí literálu, tzn. že negovat lze pouze výrokovou proměnnou.

Platí, že pro každou formuli A lze sestrojit ekvivalentní formule K a D (tedy \vdash A ↔ K a \vdash A ↔ D), kde K je v KNF a D je v DNF. Toto tvrzení lze dokázat indukcí podle složitosti formule užitím De Morganových zákonů a distributivity.

Příklady

Příklady formulí, které jsou v KNF:

:\neg A \wedge (B \vee C) (negace smí stát jen před výrokovou proměnnou) :(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E) :A \wedge B (tato formule je zároveň i v DNF)

Příklady formulí, které nejsou v KNF:

:\neg (B \vee C) :(A \wedge B) \vee C :A \wedge (B \vee (D \wedge E))

Výše uvedené formule lze ovšem do KNF převést, tedy sestrojit k nim ekvivalentní formule, které jsou v KNF:

:\neg B \wedge \neg C :(A \vee C) \wedge (B \vee C) :A \wedge (B \vee D) \wedge (B \vee E)