Konjunktív normálforma

A konjunktív normálforma, röviden KNF a matematikai logika egy területén, a nulladrendű logikán belül definiálható fogalom, egy logikai műveletet leíró olyan ítéletlogikai formulát jelent, mely a művelet változóinak vagy negáltjainak diszjunkcióinak konjunkciója:

$\bigwedge _{i}\bigvee _{j}(\neg )x_{ij}.$

A konjunktív normálformák tehát olyan nulladrendű logikai formulák, melyekben csak változók és az $\lnot ,\vee ,\wedge$ operátorok fordulnak elő (és egyéb megkötések is érvényesek). A pontos matematikai definíciót lásd lentebb.

Tehát, ha a logikai művelet az $X_{1}$, $X_{2}$,$...$,$X_{n}$ változókon van értelmezve, akkor egy konjunktív normálformája lehet például:

$\left(\lnot X_{1}\vee X_{2}\right)\wedge \left(\lnot X_{2}\vee X_{3}\right)\wedge ...\wedge \left(\lnot X_{n-1}\vee X_{n}\right)$

Fontosabb elnevezések

Tekintsük megint az alábbi, KNF alakú formulát:

$\left(\lnot X_{1}\vee \lnot X_{2}\right)\wedge \left(X_{2}\vee X_{3}\vee \lnot X_{4}\right)$

• a változókat a (normál)forma atomjainak nevezzük, a fenti példában atomok $X_{1},X_{2},X_{3},X_{4}$ ;
• a változókat vagy negáltjaikat közös néven a (normál)forma literáljainak nevezzük; a fenti példában literálok $\lnot X_{1},\lnot X_{2},X_{2},X_{3},\lnot X_{4}$ ; a negálatlan literálokat pozitívnak, míg a negáltakat negatívnak is szokás nevezni.
• a literálok diszjunkcióit pedig klózoknak (clause, ang. "mellékmondat"). Szokás ezeket elemi diszjunkcióknak is nevezni; a fenti példa klózai: $\lnot X_{1}\vee \lnot X_{2}$ és $X_{2}\vee X_{3}\vee \lnot X_{4}$ .

E formuláknak különféle alkalmazásai vannak például a számításelméletben, az automatikus tételbizonyítások elméletében (rezolúciós kalkulus, logikai programozás)

Rekurzív definíció

Legyen adott egy L nulladrendű nyelv. Ennek azon F formulái konjunktív normálalakúak, melyek az alábbi három szintaktikai alosztályba tartoznak:

1. vagy atomi formulák vagy ilyenek negáltjai (összességében, literálok).
2. vagy $K\vee L$ alakúak, ahol K,L literálok; összességében elemi diszjunkciók (az atomi formulákat is ide számítjuk),
3. $F=K\wedge L$ alakúak, ahol K,L elemi diszjunkciók, melyeket az F klózainak nevezünk.

Példák és ellenpéldák

Néhány logikai művelet, konjunktív normálformában:

$A\vee B$

$A\vee \lnot B$

$A\wedge \lnot B$

$\left(A\vee \lnot B\right)\wedge \left(\lnot A\vee \lnot B\right)$

A következő formulák viszont nem konjunktív normálformulák:

$\lnot (A\vee B)\wedge C$ , mert a negáció nem csak atomot köt, hanem egy összetett formulát;

$(A\wedge B)\vee C$ , mert nem konjunkciós formula (közvetlen részformulái nem konjunkcióval vannak összekapcsolva), és mert az egyik részformula nem elemi diszjunkció, hanem elemi konjunkció;

$(A\vee B)\rightarrow C$ mert előfordul nem megengedett operátor ( $\rightarrow$).

Viszont a fenti formulákkal (műveletekkel) ekvivalensek az alábbi, konjunktív normálforma alakú formulák:

$\lnot A\wedge \lnot B\wedge C$

$(A\vee C)\wedge (B\vee C)$

$(\lnot A\vee C)\wedge (\lnot B\vee C)$

Műveletek és formulák előállítása KNF alakban

Tetszőleges ítéletlogikai műveletet és formulát elő lehet állítani KNF alakban. Néha többféleképp is, azaz az előállítás nem egyértelmű.

Szintaktikus módszerek

Egy nem-, és-, vagy-, implikáció- és ekvivalencia-jeleket tartalmazó nulladrendű formula mindig átalakítható KNF alakba, mégpedig szintaktikusan, azaz csak átalakítási szabályok segítségével; anélkül, hogy a formulát ki kellene értékelnünk.

A következő szabályokat lehet, érdemes alkalmazni egy formula KNF alakba hozásakor:

1. $A\leftrightarrow B\equiv \left(A\rightarrow B\right)\wedge \left(B\rightarrow A\right)$;
2. $A\rightarrow B\equiv \lnot A\vee B$;
3. $\lnot (A\vee B)\equiv \lnot A\wedge \lnot B$ (De Morgan-szabály I.);
4. $\lnot (A\wedge B)\equiv \lnot A\vee \lnot B$ (De Morgan-szabály II.);
5. $(A\wedge B)\vee C\equiv (A\vee C)\wedge (B\vee C)$ (disztributivitási törv.);
6. $\lnot \lnot A\equiv A$ (kettős tagadás);
7. $A\vee A\equiv A\wedge A\equiv A$ (idempotencia).

A KNF egyszerűsítésre sokszor még használhatóak az ún. adszorbciós szabályok:

1. $(A\wedge B)\vee A\equiv A$ ;
2. $(A\vee B)\wedge A\equiv A$ .

Szemantikus módszerek. A KKNF

Ha adott egy többváltozós logikai művelet, például értéktáblázattal, akkor ennek ismeretében megkonstruálható egy KNF, ami az illető műveletet leírja. Ez azt is jelenti, hogy az $\left(\lnot ,\vee ,\wedge \right)$ rendszer funkcionálisan teljes.

Egy konjunktív normálforma értéktáblázatát elkészítve, a formula adott sorban (interpretációban) pontosan akkor lesz igaz, ha abban az interpretációban minden elemi diszjunkció igaz, tehát pontosan akkor hamis, ha abban az interpretációban valamelyik elemi diszjunkció hamis. Márpedig egy elemi diszjunkció pontosan akkor hamis, ha minden literálja hamis abban az interpretációban, azaz negálatlan atomjai hamisak, a negáltak pedig igazak. Adott interpretációt tekintve, ha tehát az atomokat összediszjunkciózzuk úgy, hogy a diszjunkcióban negálatlanul szerepeljenek a h igazságértéket kapott atomok, és negáltan az igaz igazságértéket kapott atomok; akkor a diszjunkció értéke hamis lesz. Ezáltal pedig a diszjunkciók konjunkciója is hamis lesz ebben az interpretációban.

Ennek megfelelően a következőképp konstruálhatunk KNF-t tetszőleges művelethez: a művelet értéktáblázata minden olyan sorához (interpretációjához), melyben az f művelet a h (hamis) logikai értéket veszi fel, konstruálunk egy literálokból álló, elemi diszjunkciót, mégpedig úgy, hogy ha az X_k változónak abban a sorban i értéket adtunk, akkor ez a változó a diszjunkcióba mint negált atom kerül be, ha pedig h (hamis) értéket, akkor negálatlanul kerül be. Tehát minden olyan sorhoz/interpretációhoz, melyre f(X₁, … , X_n) = h , ily módon létrehozunk egy elemi diszjunkciót, mely pontosan ebben az interpretációban hamis. Majd képezzük ezek konjunkcióját: ez pontosan akkor hamis, ha minden elemi diszjunkciója hamis, azok meg pontosan akkor hamisak, ha f(X₁, … , X_n) hamis. Így egy KNF alakú formulát kapunk, és a fentiek alapján ez valóban "ekvivalens" az eredeti logikai függvénnyel. Az ezen algoritmus eredményeképp kapott KNF-t a logikai művelet/formula kitüntetett konjunktív normálformájának (KKNF) is nevezik.

Formálisan „polinommal” adhatjuk meg az f KKNF alakját:

$KKNF\left(f\left(X_{1},X_{2},...,X_{n}\right)\right)=\bigwedge _{I\in \left\{0,1\right\}^{n}\wedge f^{I}=0}\bigvee _{j=1}^{n}\left[(-1)^{X_{i}^{I}+1}X_{i}\right]$ .

Tehát a konjunkcióképzés az összes olyan interpretációra (kiértékelésre) terjed ki, mely hamissá teszi f-et; továbbá g^I-vel jelöltük a g függvény adott I kiértékelésbeli logikai értékét (például ha g=f vagy ha g=X_i), és -1-gyel való „szorzásként” a negálást.

Megjegyzés: e módszerrel nem lehet az azonosan igaz logikai függvényekhez KNF-t rendelni. És valóban, ezeknek nincs is, illetve esetleg azt szoktuk mondani, hogy KNF alakjuk az "üres konjunkció", amit 1-gyel (i-vel) is szokás jelölni.

Példa

KKNF konstruálása

E módszereket a következő, $f(A,B):=\lnot \left(A\rightarrow B\right)$ kétváltozós függvény példáján illusztráljuk:

A   B  f(A,B) elemi diszjunkció 0 0 0 $A\vee B$ 0 1 0 $A\vee \lnot B$ 1 0 1 - 1 1 0 $\lnot A\vee \lnot B$

Vagyis az $f(A,B)=\lnot \left(A\rightarrow B\right)$ függvényhez/formulához szemantikusan konstruált normálforma a következő lesz:

$\left(A\vee B\right)\wedge \left(A\vee \lnot B\right)\wedge \left(\lnot A\vee \lnot B\right)$     (*) .

Szintaktikus konstrukció

Szintaktikusan egy sokkal egyszerűbb, egyetlen elemi diszjunkcióból álló KNF-et tudunk konstruálni: $\lnot \left(A\rightarrow B\right)\equiv \lnot \left(\lnot A\vee B\right)$ $\equiv$ $A\wedge \lnot B$ érvényes ugyanis (a fentebb megadott 2. szintaktikai szabályt és a 3.-at, a De Morgan-törvényt használtuk).

A KKNF egyszerűsítése

A szemantikus módszerrel kapott KKNF-ből a következőképp, a (*) formula alábbi átalakításaival, egyszerűsítésével is eljuthatunk szintaktikus úton a fent leírt sokkal egyszerűbb KNF-hoz; a KKNF utolsó két klózának konjunkciójából álló részformuláját alakítgatjuk: $\left(A\vee \lnot B\right)\wedge \left(\lnot A\vee \lnot B\right)$ $\equiv$ $\left[\left(A\vee \lnot B\right)\wedge \lnot A\right]\vee \left[\left(A\vee \lnot B\right)\wedge \lnot B\right]$ $\equiv$ $\left[\left(A\wedge \lnot A\right)\vee \left(\lnot B\wedge \lnot A\right)\right]\vee \left[\lnot B\right]$ $\equiv$ $\left[0\vee \left(\lnot B\wedge \lnot A\right)\right]\vee \lnot B$ $\equiv$ $\left(\lnot B\wedge \lnot A\right)\vee \lnot B$ $\equiv$ $\left(\lnot A\wedge \lnot B\right)\vee \lnot B$ $\equiv$ $\left(\lnot A\wedge \lnot B\right)\vee \lnot B$ $\equiv$ $\lnot B$

Tekintetbe véve még az első klózt is; $f(A,B)=\lnot \left(A\rightarrow B\right)$ $\equiv$ $\left(A\vee B\right)\wedge \lnot B$ $\equiv$ $\left(A\wedge \lnot B\right)\vee \left(B\wedge \lnot B\right)$ $\equiv$ $\left(A\wedge \lnot B\right)\vee 0$ $\equiv$ $\left(A\wedge \lnot B\right)$

(E hosszadalmas eljárás egy lentebbi szakaszt kíván illusztrálni).

A KNF nem egyértelmű

Mindebből látható, hogy a KNF tényleg nem egyértelmű, sok esetben egyszerűsíthető a fent megadott ill. további szintaktikus szabályok (az ítéletlogika törvényei) segítségével.

Problémák és alkalmazások

A KNF-előállító eljárások sok algoritmikus, számításelméleti problémát vetnek fel.

Egyszerűsítő eljárások

Láttuk, hogy a KNF nem egyértelműen létezik egy adott Boole-függvényhez vagy formulához. Felmerül a kérdés, hogy definiálható-e és található-e mindegyikükhöz egy-egy valamilyen értelemben „legegyszerűbb” KNF?

Például a fent leírt szemantikus eljárással kapott KNF-k gyakorta exponenciális sok tagból állnak. Ezért a múlt században (az 1950-es évektől) az elektronikus számítógépek és az áramkörelmélet megjelenése után komoly kutatási terület volt a matematikai logikán belül a normálformák egyszerűsítése. Rengeteg egyszerűsítő eljárást fedeztek fel, a leggyakrabban idézett a Quine-McCluskey-algoritmus (ezt igazából diszjunktív normálformákra dolgozták ki).

Kielégíthetőség

Nevezetesek az alábbi egyszerűen megfogalmazható számításelméleti problémák:

• Kielégíthetőségi probléma ( SAT -probléma): Adott F formula KNF alakjáról állapítsuk meg, hogy kielégíthető-e, azaz változóinak adható-e olyan igazságérték (interpretáció), melyben F igaz lesz? Jelenleg nem tudjuk, erre a feladatra adható-e egy polinomidőben befejeződő determinisztikus megoldási algoritmus (azaz fogalmunk sincs arról, hogy SAT∈P igaz-e); noha azt tudjuk, hogy a probléma (exponenciális időben) megoldható, azaz SAT∈NP. Azt is tudjuk, hogy nemdeterminisztikus eljárással e probléma megoldható polinomidőben. A probléma egy könnyített alesete, a HORNSAT -probléma (melyben megköveteljük, hogy a KNF minden klóza legfeljebb egy pozitív literált tartalmazzon) viszont P-ben van, adható rá determinisztikus polinomidejű megoldóeljárás.
• A k-Kielégíthetőségi problémasereg ( k-SAT ): Adott F formula KNF alakjáról, melynek minden klóza pontosan k(∈ℕ⁺) literálból áll; állapítsuk meg, hogy kielégíthető-e, azaz változóinak adható-e olyan igazságérték (interpretáció), melyben F igaz lesz? Ezen problémák többsége NP-teljes, így nem oldható meg polinomidőben; a 2-SAT∈P viszont igen.

Alkalmazások

A konjunktív normálformák elmélete az egyik matematikai alapja a manapság a mesterségesintelligencia-kutatás által vizsgált automatikus tételbizonyító módszerek legdivatosabbjának, a rezolúciónak, mely Prolog néven a logikai programozás legfontosabb vagy legismertebb megvalósítása napjainkban.

Hivatkozások

Lásd még

• Diszjunktív normálforma
• Skolem-normálforma
• Horn-logika

Külső hivatkozások

• A KNF-t előállító szintaktikus algoritmus (PDF)
• A KNF-t előállító szintaktikus algoritmus (PDF)
• Cikk a páros KNF-ekről (PS)
• KNF-k homomorfizmusai (PDF)

Irodalom

• Papadimitriou, Christos H.: Számítási bonyolultság (Computational complexity). Egyetemi tankönyv. Novadat Bt., 1999. ISBN 963-9056-20-0 .
• Pásztorné Varga Katalin – Várterész Magda: A matematikai logika alkalmazásszemléletű tárgyalása, Panem, Bp., 2003. ISBN 963-545-364-7