Výroková logika - normálne tvary

Výroková logika - normálne tvary

Jazyk výrokovej logiky obsahuje mnoho redundancií. Jednotlivé logické spojky sa dajú definovať pomocou iných logických spojok. Opakovaným aplikovaním istých ekvivalencií (zákonov výrokovej logiky) je možné transformovať formulu na jej normálny tvar (niekedy nazývaný aj normálna forma).

Vo všeobecnosti normálny tvar eliminuje isté logické spojky a využíva iba niektoré, v predpísanom a obmedzenom tvare. Takýto tvar formuly umožňuje jej následné jednoduchšie spracovanie, avšak normálny tvar môže byť omnoho väčší ako pôvodná formula.

Normálne tvary vo výrokovej logike:

• Negatívny normálny tvar.
• Disjunktívny normálny tvar.
• Konjunktúrny normálny tvar.

Základné pojmy

Literál (l) - je výroková premenná alebo jej negácia v tvare:  p   alebo   ¬p.

Literály sa nazývajú komplementárne, ak jeden je negáciou druhého.

Elementárna disjunkcia - disjunkcia literálov (nazývaná tiež klauzula) v tvare: $$ l_1 ∨ … ∨ l_n.$$

Elementárna konjunkcia - konjunkcia literálov v tvare: $$ l_1 ∧ … ∧ l_n.$$

Negatívny normálny tvar (NNF z ang. Negation Normal Form) je formula v ktorej sa vyskytujú len operátory konjunkcie, disjunkcie a zároveň operátor negácie môže byť aplikovaný len na atomické výroky.

Disjunktívny normálny tvar (DNF z ang. Disjunctive Normal Form) je formula v tvare disjunkcií elementárnych konjunkcií: $$ (l_1 ∧ … ∧ l_n) ∨ (l_1 ∧ … ∧ l_m) ∨ … $$

Konjunktívny normálny tvar (CNF z ang. Conjunctive Normal Form) je formula v tvare konjunkcií klauzúl: $$ (l_1 ∨ … ∨ l_n) ∧ (l_1 ∨ … ∨ l_m) ∧ … $$

Formuly ϕ, ψ sú sémanticky ekvivalentné (ϕ ≈ ψ) $$ ϕ(p_1, …, p_n) ≈ ψ(p_1, …, p_n) $$ ak pre každé pravdivostné ohodnotenie výrokových premenných platí, že $$ v(ϕ(p_1, …, p_n)) = v(ψ(p_1, …, p_n)).$$

Formula je v úplnom DNF ak každá elementárna konjunkcia obsahuje všetky výrokové premenné danej formuly.

Formula je v úplnom CNF ak každá elementárna disjunkcia obsahuje všetky výrokové premenné danej formuly.

Formula je v minimálnom DNF/CNF ak obsahuje najmenší počet literálov, elementárnych konjunkcií, alebo elementárnych disjunkcií.

Prepis formuly do normálneho tvaru

Každá formula môže byť prepísaná do ekvivalentného tvaru v NNF, DNF alebo CNF. Existuje viacero algoritmov pre prepis formuly do normálneho tvaru. V rámci tohto cvičenia sa budeme venovať tzv. naivnému prepisu formuly do NNF, DNF, CNF.

Naivný prepis formuly do NNF

je možné vykonať prostredníctvom nasledujúceho algoritmu:

Algoritmus: Prepis formuly $φ$ do NNF

Vstup: Formula výrokovej logiky

Výstup: Ekvivalentná formula výrokovej logiky v NNF

• 1. Odstránenie logických ekvivalencií ⇔ a implikácií ⇒ opakovaným aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} φ ⇔ ψ &≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ)\\ φ ⇒ ψ &≡ ¬φ ∨ ψ \end{align*} $$
• 2. Odstránenie dvojitej negácie, vloženie negácie do vnútra zátovriek aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} ¬¬φ &≡ φ\\ ¬(φ ∧ ψ) &≡ ¬φ ∨ ¬ψ\\ ¬(φ ∨ ψ) &≡ ¬φ ∧ ¬ψ \end{align*} $$

Naivný prepis formuly do DNF

je možné vykonať prostredníctvom nasledujúceho algoritmu:

Algoritmus: Prepis formuly $φ$ do DNF

Vstup: Formula výrokovej logiky

Výstup: Ekvivalentná formula výrokovej logiky v DNF

• 1. Odstránenie logických ekvivalencií $⇔$ a implikácií $⇒$ opakovaným aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} φ ⇔ ψ &≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ)\\ φ ⇒ ψ &≡ ¬φ ∨ ψ \end{align*} $$
• 2. Odstránenie dvojitej negácie, vloženie negácie do vnútra zátvoriek aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} ¬¬φ &≡ φ\\ ¬(φ ∧ ψ) &≡ ¬φ ∨ ¬ψ\\ ¬(φ ∨ ψ) &≡ ¬φ ∧ ¬ψ \end{align*} $$
• 3. Vloženie konjunkcií do vnútra zátvoriek až kým nie sú aplikované na literály využitím nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} φ ∧ (ψ ∨ θ) &≡ (φ ∧ ψ) ∨ (φ ∧ θ)\\ (ψ ∨ θ) ∧ φ &≡ (ψ ∧ φ) ∨ (θ ∧ φ)\\ (φ ∨ ψ) ∧ (θ ∨ ω) &≡ (φ ∧ θ) ∨ (φ ∧ ω) ∨ (ψ ∧ θ) ∨ (ψ ∧ ω) \end{align*} $$
• 4. Zjednodušenie výslednej DNF:
  • Odstránením elementárnej konjunkcie, ktorá obsahuje komplementárne literály ($p$ a zároveň $¬p$), keďže takáto elementárna konjunkcia je ekvivalentná $⊥$.
  • Odstránením každej elementárnej konjunkcie, ktorá obsahuje inú elementárnu konjunkciu podľa zákona: $$(φ ∧ ψ) ∨ φ ≡ φ.$$
  • Dve elementárne konjunkcie v tvaroch $(φ ∧ ψ)$ a $(φ ∧ ¬ ψ)$ zjednodušíme na $φ$: $$(φ ∧ ψ) ∨ (φ ∧ ¬ψ) ≡ φ.$$

Naivný prepis formuly do CNF

je možné vykonať prostredníctvom nasledujúceho algoritmu:

Algoritmus: Prepis formuly $φ$ do CNF

Vstup: Formula výrokovej logiky

Výstup: Ekvivalentná formula výrokovej logiky v CNF

• 1. Odstránenie logických ekvivalencií $⇔$ a implikácií $⇒$ opakovaným aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} φ ⇔ ψ &≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ)\\ φ ⇒ ψ &≡ ¬φ ∨ ψ \end{align*} $$
• 2. Odstránenie dvojitej negácie, vloženie negácie do vnútra zátvoriek aplikovaním nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} ¬¬φ &≡ φ\\ ¬(φ ∧ ψ) &≡ ¬φ ∨ ¬ψ\\ ¬(φ ∨ ψ) &≡ ¬φ ∧ ¬ψ \end{align*} $$
• 3. Vloženie disjunkcií do vnútra zátvoriek až kým nie sú aplikované na literály využitím nasledujúcich zákonov výrokovej logiky: $$ \begin{align*} φ ∨ (ψ ∧ θ) &≡ (φ ∨ ψ) ∧ (φ ∨ θ)\\ (ψ ∧ θ) ∨ φ &≡ (ψ ∨ φ) ∧ (θ ∨ φ)\\ (φ ∧ ψ) ∨ (θ ∧ ω) &≡ (φ ∨ θ) ∧ (φ ∨ ω) ∧ (ψ ∨ θ) ∧ (ψ ∨ ω) \end{align*} $$
• 4. Zjednodušenie výslednej CNF:
  • Odstránením klauzúl, ktoré obsahuje komplementárne literály ($p$ a zároveň $¬p$), keďže takáto klauzula je ekvivalentná $⊤$.
  • Odstránením každej elementárnej konjunkcie, ktorá obsahuje inú elementárnu konjunkciu podľa zákona: $$(φ ∨ ψ) ∧ φ ≡ φ.$$
  • Dve elementárne disjunkcie v tvaroch $(φ ∨ ψ)$ a $(φ ∨ ¬ ψ)$ zjednodušíme na $φ$: $$(φ ∨ ψ) ∧ (φ ∨ ¬ψ) ≡ φ.$$

Prepis formuly do úplného normálneho tvaru

Každú výrokovú formulu je možné prepísať na ekvivalentnú formulu v úplnom normálnom tvare. Úplný DNF aj CNF je možné vypísať z pravdivostnej tabuľky.

Prepis formuly do minimálneho normálneho tvaru

V ďalšom kroku sa budeme venovať určeniu čo najjednoduchšieho tvaru formúl. Takéto tvary sa nazývajú minimálne normálne tvary. K tomu budeme využívať Karnaughove mapy.

Karnaughove mapy predstavujú prehľadný spôsob zjednodušovania booleovských funkcií. Jedná sa o grafické znázornenie pravdivostnej tabuľky, pri ktorom sa využíva ľudská schopnosť rozpoznávať vizuálne objekty.

Karnaughova mapa booleovskej funkcie $n$ premenných je dvojrozmerná tabuľka, ktorá obsahuje $2^n$ buniek. Jednotlivé bunky sú indexované vstupnými premennými. Na základe toho, je možné každej bunke jednoznačne priradiť jeden riadok pravdivostnej tabuľky a vice versa. Ide teda o prehľadný spôsob zápisu príslušnej booleovskej funkcie do tabuľky (mapy). V prípade dvoch premenných sa jedná o mapu veľkosti 2x2, v prípade troch premenných je veľkosť mapy 2x4 a pri štyroch premenných je to 4x4.

Pri zložitejších formulách je vhodnejšie využiť Karnaughove mapy. V prvom kroku je potrebné zostrojiť pravdivostnú tabuľku formuly $φ = (x ∧ y) ∨ (x ∧ ¬y)$.

Na obrázku nižšie je zobrazená prázdna Karnaughova mapa formuly (booleovskej funkcie), ktorá obsahuje dve premenné, pričom:

• Horný index mapuje premennú $x$.
• Ľavý index mapuje premennú $y$.
• Pri indexoch je uvedené aké pravdivostné ohodnotenie v daných bunkách nadobúda príslušná premenná.

Pri výpise MDNF postupujeme nasledovne.

• Hľadáme združenia jednotiek a vpisujeme odpovedajúce konjunkty. Ak združenie zasahuje do celého rozsahu pravdivostného ohodnotenia danej premennej, danú premennú vypíšeme do konjunktu v tvare $\overset{\sim}{p} ∧ … ∧ \overset{\sim}{r}$, tak že:
  • ak $v(p) = 1$, potom $\overset{\sim}{p} = p$,
  • ak $v(p) = 0$, potom $\overset{\sim}{p} = ¬p$.
• V prípade, že združenie zasahuje do oboch pravdivostných ohodnotení danej premennej, túto premennú pri výpise vynechávame.

V našej mape na obrázku vyššie, máme iba jedno združenie jednotiek, ktoré zasahuje do pravdivostného ohodnotenia $1$ premennej $x$. To znamená, že MDNF formuly $φ$ bude obsahovať iba jeden konjunkt v tvare: $$x.$$

Pri výpise MCNF postupujeme nasledovne.

• Hľadáme združenia núl a vypisujeme odpovedajúce disjunkty. Ak združenie zasahuje do celého rozsahu pravdivostného ohodnotenia danej premennej, danú premennú vypíšeme do disjunktu v tvare $\overset{\sim}{p} ∨ … ∨ \overset{\sim}{r}$, tak že:
  • ak $v(p) = 1$, potom $\overset{\sim}{p} = ¬p$,
  • ak $v(p) = 0$, potom $\overset{\sim}{p} = p$.
• V prípade, že združenie zasahuje do oboch pravdivostných ohodnotení danej premennej, túto premennú pri výpise vynechávame.

V našej mape na obrázku vyššie, máme iba jedno združenie núl, ktoré zasahuje do pravdivostného ohodnotenia $0$ premennej $x$. To znamená, že MCNF formuly $φ$ bude obsahovať iba jeden disjunkt v tvare: $$x.$$

Tseitinová transformácia

Majme formulu $$φ_n = (p_1 ∧ q_1) ∨ (p_2 ∧ q_2) ∨ … ∨ (p_n ∧ q_n),$$ kde $n \in \mathbb{N}$. Prostredníctvom De Morganových zákonov a distributívneho zákona výrokovej logiky je možné previesť formulu $φ_n$ na $φ_n'$ v CNF. Avšak takýto prístup vytvorí formulu $φ_n'$, ktorá bude pozostávať z $2^n$ klauzúl, čo znamená exponenciálny nárast veľkosti formuly oproti pôvodnej formule $φ_n$. Napríklad ak $n=10$, potom $φ_{10}'$ pozostáva z $1024$ klauzúl, ak $n=20$ potom $φ_{20}'$ pozostáva z $1048576$ klauzúl. Inymi slovami, každá inkrementácia $n$ o jeden, vyústi do dvojnásobnej veľkosti výslednej formuly.

Algoritmus vyššie môže v najhoršom prípade zvačšiť formulu exponenciálne. Grigorij Samuilovitsch Tseitin (Григорий Самуилович Цейтин) navrhol algoritmus známy ako Tseitinová transformácia. Tento algoritmus berie ako vstup formulu $φ$ a vytvorí $φ'$ v CNF, ktorej veľkosť sa zväčší lineárne. Na rozdiel od predchádzajúceho algoritmu je však medzi $φ$ a $φ'$ slabšie spojenie. Vo všeobecnosti je zaručené $φ$ a $φ'$ budú ekvisplniteľné a nie ekvivalentné.

Ekvisplniteľnosť dvoch formúl: dve formuly sú ekvisplniteľné vtedy, ak prvá formula je splniteľná vtedy, tak aj druhá formula je splniteľná a vice versa. Inými slovami, buď sú splniteľné obidve formuly, alebo nie sú splniteľné obidve formuly. Avšak ekvisplniteľné formuly pri konkrétnom pravdivostnom ohodnotení premenných nemusia mať rovnakú výslednú pravdivostnú hodnotu. To znamená, že ekvisplniteľnosť je odlišná od logickej sémantickej ekvivalencie, keďže dve ekvivalentné formuly majú vždy rovnaké výsledné pravdivostné hodnoty, pri rovnakom pravdivostnom ohodnotení premenných.

Pri Tseitinovej transformácii platí, že pre akékoľvek formulu $φ \in Prop$ existuje formula $φ'$, taká že:

• $φ$ a $φ'$ su ekvisplniteľné,
• $φ'$ je v CNF,
• $size(φ')≤ 16 × size(φ)$ (výsledná formula nie omnoho vačšia),
• akékoľvek pravdivostné ohodnotenie $φ'$ je taktiež pravdivostné ohodnotenie pre $φ$.

To znamená, že z každého modelu výslednej formuly $φ'$ je možné extrahovať model formuly $φ$.

Tseitinová transformácia - algoritmus

Algoritmus: Tseitinová transformácia

Vstup: Formula výrokovej logiky $φ$

Výstup: Ekvisplniteľné formula výrokovej logiky $φ'$ v CNF

1. Výpočet abstraktného syntaktického stromu $ast(φ)$.

• Priradenie novej premennej každému internému uzlu.
• Označenie listov premennou, ktorú obsahuje daný list.

2. Formula $φ'$ bude konjunkcia klauzúl, pričom v každý vnútorný uzol bude obsahovať dve alebo tri klauzuly.

• Ak je uzol negácia v tvare:

• Ak uzol je konjunkcia v tvare:

• Ak uzol je disjunkcia v tvare:

• Ak uzol je implikácia v tvare:

3. V poslednom kroku pridáme do výslednej $φ'$ klauzulu, ktorá pozostáva z premennej priradenej koreňovému uzlu.

Tseitinová transformácia - príklad