Výroková logika - opakování Formální zavedení
Výroková formule: Máme neprázdnou nejvýše spočetnou množinu A výrokových proměnných. 1. Každá proměnná je výroková formule 2. Když α, β jsou formule, potom (¬α), (α ∧ β), (α ∨ β), (α ⇒ β), (α ⇔ β), případně i (α ⊕ β), … jsou formule. 3. Nic jiného než to, co vzniklo pomocí konečně mnoha použití bodů 1 a 2, není výroková formule (Konvence: vnější závorky a závorky vyplývající z priorit ¬, ∧, ∨, ⇒, ⇔ lze vynechat) Tak zvaná rekurzivní či induktivní definice
Výroková logika Základní pojmy
Ohodnocení ≡DEF zobrazení A do {FALSE, TRUE}. Ohodnocení formule se řídí běžnými pravidly pro logické spojky. Výroková formule s n logickými proměnnými má 2n možných pravdivostních hodnot v závislosti na ohodnocení proměnných • Formule je tautologie právě tehdy, když je TRUE pro všechna možná ohodnocení proměnných. • Formule je kontradikce právě tehdy, když je FALSE pro všechna ohodnocení. • Formule je splnitelná právě tehdy, když existuje alespoň jedno ohodnocení, ve kterém je TRUE
Výroková logika Matematická logika
Matematická logika se zabývá otázkou, co lze z formulí odvodit bez ohledu na jejich význam, pouze podle struktury. • Formule ϕ je (sémantickým) důsledkem množiny formulí Ψ = {ψ1, ψ2, … , ψn} právě tehdy když ϕ má ohodnocení TRUE pro každé ohodnocení proměnných, kde každá z formulí v Ψ je TRUE. Značíme Ψ Í ϕ. • Formule ϕ a ψ jsou tautologicky ekvivalentní právě tehdy když ψ Í ϕ a ϕ Í ψ. Značíme ϕ ≡ ψ. Formule jsou pravdivé pro stejná ohodnocení.
Výroková logika
Úplný systém log. spojek
• • •
Nulární spojky TRUE (tautologie) a FALSE (kontradikce) Unární spojky Identita a Negace ¬ Pro log. funkce dvou proměnných máme celkem 24 možných log. funkcí (máme 22 řádků v tabulce pravdivostního ohodnocení), potřebujeme tedy vyjádřit 14 funkcí (zbylé dvě jsou opět tautologie a kontradikce). • Úplný systém log. spojek je množina log. spojek, pomocí které můžeme zapsat všechny logické funkce. Možný úplný systém log. spojek: ¬, ∨, ∧ Booleova algebra není minimální (de Morganova pravidla)
Všechny logické spojky x
y
F 0
F 1
F
∧
F 2
F 3
F 4
x
F 5
F 6
F 7
F 8
F 9
F 10
F 11
F 12
F 13
F 14
F 15
y
⊕
∨
↓
⇔
¬ x
⇐
¬ y
⇒
T
0
0
0
0
0
0
0
0
0
0
1
1
1
1
1
1
1
1
0
1
0
0
0
0
1
1
1
1
0
0
0
0
1
1
1
1
1
0
0
0
1
1
0
0
1
1
0
0
1
1
0
0
1
1
1
1
0
1
0
1
0
1
0
0
0
1
0
1
0
1
0
1
F0 = kontradikce F1 = AND, konjunkce F2 = (inhibice) F4 = (zpětná inhibice) F6 = XOR, vylučující nebo F7 = OR, disjunkce F8 = NOR, Peirceova šipka (arrow) F9 = ekvivalence F10 = negace x F11 = zpětná implikace F12 = negace y F13 = implikace F14 = NAND, Shefferův škrt (stroke) F15 tautologie
Jediné dvě logické spojky, které tvoří jednoprvkový úplný systém jsou NOR ↓ a NAND | . Častěji se užívají NOT, OR a AND (Booleova algebra) Jednu ze spojek OR a AND lze vynechat (de Morganova pravidla)
Výroková logika Normální formy
•
•
• •
Konjunktivní normální forma (CNF) = konjunkce jednoho nebo konečně mnoha formulí, kde každá z nich je literál nebo disjunkce literálů. Příklad: (x ∨ ¬ y) ∧ (¬ y ∨ z ) ∧ ( x ∨ ¬ r ∨ z ) Disjunktivní normální forma (DNF) = disjunkce jednoho nebo konečně mnoha formulí, kde každá z nich je literál nebo konjunkce literálů. Příklad: (x ∧ ¬ y) ∨ (¬ y ∧ z ) ∨ ( x ∧ ¬ r ∧ z ) Formule v konjunkci u CNF je nazývána klauzule. Je to tedy disjunkce literálů nebo literál. Zavádíme pojem prázdná klauzule, která neobsahuje žádný literál a není splnitelná. Pro každou log. formuli existuje tautologicky ekvivalentní DNF formule a také tautologicky ekvivalentní CNF formule. Pro každý Booleovský výraz existuje odpovídající CNF i DNF formule.
Výroková logika Přirozená dedukce
• • ¾ ¾ ¾ ¾
Odvozovací systém umožňující z dané množiny formulí (předpokladů) odvodit závěry. Pro každou logickou spojku máme I-pravidlo pro zavedení a Epravidlo pro eliminaci ¬ : I-pravidlo: (ϕ f α) f (¬α f¬ϕ); E-pravidlo: ¬(¬ϕ) f ϕ (pravidlo “dvojí negace”). ∧: I-pravidlo: {ϕ, ψ} f ϕ ∧ ψ. E-pravidla: ϕ ∧ ψ f ϕ; ϕ ∧ ψ f ψ. ∨: I-pravidla: ϕ f ϕ ∨ ψ; ϕ f ψ ∨ ϕ. E-pravidlo: ϕ ∨ ψ a ϕ f α a ψ f α) f α (“důkaz rozborem případů”). ⇒: I-pravidlo: (ϕ f ψ) f ϕ ⇒ ψ; E-pravidlo: (ϕ and ϕ ⇒ ψ) f ψ (pravidlo “modus ponens”).
Výroková logika Přirozená dedukce
•
• •
Operaci odvození nové formule z množiny formulí S značíme f . Touto operací obdržíme novou množinu formulí, která se skládá buď z předpokladů nebo z formulí odvozených pomocí některých odvozovacích pravidel. Říkáme, že odvozená formule β je log. důsledkem S a log. vyplývá z S. Značíme S f* β (tranzitivní uzávěr). Někdy pouze S f β Množina formulí S je nekonzistentní (rozporná) , právě tehdy když existuje formule α taková, že současně α a ¬α logicky vyplývají z S. Jinak říkáme, že množina S je konzistentní (bezrozporná, zdravá).
Úplnost výrokové logiky • Formule ϕ je sémantickým důsledkem množiny formulí S, pokud platí, že při každém pravdivostním ohodnocení při kterém jsou všechny formule v S pravdivé, je pravdivá také formule ϕ. • Formule ϕ je logickým důsledkem množiny formulí S, pokud platí lze odvodit pomocí odvozovacích pravidel (existuje její důkaz). Pokud je množina S bezrozporná, je vše, co je logickým důsledkem i sémantickým důsledkem (S Í ϕ ⇒ S f* ϕ). Pro výrokovou logiku to platí to i naopak. Vše co je sémantickým důsledkem je i logickým důsledkem (lze to dokázat – tedy S f* ϕ ⇒ S Í ϕ). Této vlastnosti se říká úplnost dedukčního systému.
Výroková logika Rezoluční princip
•
• • •
Mějme S množinu formulí v nějakém odvozovacím systému a nechť α je formule. Zajímá nás otázka, zda-li α je log. důsledkem S. Rezoluční princip je založen na faktu, že S f α právě tehdy když S ∪ {¬α} není splnitelná. Toto je ekvivalentní známému faktu, že α ⇒ β a ¬α ∨ β jsou tautologicky ekvivalentní. Rezoluční princip je základem logického programování.
Výroková logika Rezoluční princip
•
• • •
Budeme předpokládat CNF, budeme psát {x, ¬y, ¬z, v, ¬w} místo x ∧ ¬y ∧ ¬z ∧ v ∧ ¬w. Prázdná klauzule bude značena [], . Rezoluční princip spočívá v eliminaci dvou komplementárních literálů z klauzulí: (x ∨ y) ∧ (¬x ∨ z) ⇒ y ∨ z. Obecně budeme říkat, že D je rezolventa klauzulí C1 a C2 podle literálu p právě tehdy když existuje literál p takový, že p ∈ C1, ¬p ∈ C2 a D = (C1 ÷ {p}) ∪ (C1 ÷ {¬p}).
Výroková logika Rezoluční princip
•
Rezoluční princip spočívá v opakovaném vytváření rezolvent: R0(S) = S, Rj+1(S) = R(Rj(S)) pro j = 1, 2, ... .
• •
∞
Nechť R (Sˇ) = ∪ Rj(S). j =1 S = R0(S) ⊆ R1(S) ⊆ ... ⊆ Rk(S) ⊆ ... . Protože množina proměnných je konečná, lze vytvořit jen konečně mnoho disjunkcí a existuje takové n, že Rn+1(S) = Rn(S) = R*(S). Množina R*(S) obsahuje prázdnou klauzuli právě tehdy když S nebo nějaké Rk(S) obsahuje dvě klauzule {x} and {¬x} pro nějakou proměnnou x. Rezoluční princip: Množina klauzulí S je splnitelná právě tehdy když výsledek aplikování rezolvent neobsahuje prázdnou klauzuli []. Rozhodnutí, zda-li formule ϕ je sémantickým důsledkem množiny formulí S potom vede na ekvivalentní úlohu rozhodnout, zda S ∪ {¬ ϕ} je nesplnitelná, tj. zda z ní lze rezolučním postupem odvodit prázdnou klauzuli []. *
Výroková logika Rezoluční princip
Postup: 1. Pro každou formuli v S nalézt tautologicky ekvivalentní CNF formuli. Provedeme náhradu všech formulí z předpokladů. Získáme množinu disjunkcí, které mají platit současně. Tautologie vynecháme. Pokud je výsledná množina prázdná, potom se skládá jen z tautologií a je tedy splnitelná. Jinak aplikujeme rezoluce (hledáme komplementární literály). 2. Přidáváme postupně (v libovolném pořadí) resolventy. 3. Pokud během postupu nalezneme prázdnou klauzuli, je množina množina S nesplnitelná. Pokud se proces zastaví a R*(S) prázdnou klausuli neobsahuje, je množina S splnitelná.
Výroková logika
Rezoluční princip – příklad 1 • • • •
Množina S = {x ∨ y ∨ z, z ∨ t ∨ v, z ⇒ (x ∨ y), y ⇒ x, w ⇒ t, v ∨ w} Je x sémantickým důsledkem? Tj. je pravda, že S f x? Tuto úlohu převedeme na problém splnitelnosti množiny formulí S ∪ {¬ x} Postup: 1. Převedeme S na CNF: {x ∨ y ∨ z, z ∨ t ∨ v, ¬ z ∨ x ∨ y, ¬ y ∨ x, ¬ w ∨ t, v ∨ w}
Výroková logika Rezoluční princip – příklad
Odvodili jsme prázdnou formuli, množina tedy není splnitelná a tudíž x je sémantickým důsledkem daných klausulí
