IB101.md

Výroková logika

• abeceda -- výroky + spojky
• dokazatelnost A ⊢ B -- B je dokazatelné z A
• důkaz -- je složen z nejméně 4 rezolučních kroků, musíme použít všechny vstupní klauzule
• evaluace -- vyhodnocení
• formule -- konjunkce množiny klauzulí
  • pravdivá formule (tautologie) -- pravdivá ve všech interpretacích (její pravdivostní funkce nabývá vždy hodnoty 1), značíme: ⊨ p ∨ ¬p nebo ⊨ A
  • splnitelná formule -- pravdivá alespoň v jedné interpretaci
  • nesplnitelná formule (kontradikce) -- není pravdivá v žádné interpretaci (její pravdivostní funkce nabývá vždy hodnoty 0), značíme: ⊨ ¬A
• interpretace -- funkce přiřazující všem atomickým formulím dané formule pravdivostní hodnoty
• klauzule -- disjunkce dvou a více literálů
  • Hornova klauzule -- obsahuje nanejvýš 1 pozitivní literál; každá splnitelná množina Hornových klauzulí musí obsahovat alespoň jeden fakt a cíl
    • fakta –- bez negativních literálů (jeden pozitivní literál)
    • pravidla –- s alespoň jedním negativním literálem
    • cíle -– bez pozitivního literálu
• literál -- výroková proměnná nebo její negace
• model -- interpretace, ve které je valuace formule pravdivá
• rezoluční pravidlo -- pravidlo, jež ze dvou klauzulí udělá jiné pravidlo
• valuace -- pravdivostní ohodnocení (přiřazení 0 nebo 1)
• vyplývání A ⊨ B -- B logicky vyplývá z A (B je logický důsledek A, A je premisa), tz. každý model A splňuje B
• výrok -- tvrzení, o jehož pravdivosti má smysl uvažovat; nulární predikát

Normální formy

konjunktivní normální forma -- závorky jsou spojeny konjunkcí

úplná konjunktivní normální forma -- v každé závorce jsou disjunkce všech proměnných, závorky jsou spojeny konjunkcí

disjunktivní normální forma -- závorky jsou spojeny disjunkcí

úplná disjunktivní normální forma -- v každé závorce jsou konjunkce všech proměnných, závorky jsou spojeny disjunkcí

Splnitelnost, úplnost a spornost

• T ... množina všech teorémů
• P ... množina všech tautologií
• V ... množina všech správně utvořených formulí

T ⊆ P ... korektnost (také: T ⊨ φ nebo A ⊢ B => A ⊨ B )

T ⊇ P ... úplnost (také: T ⊢ φ nebo A ⊢ B <= A ⊨ B )

T = V ... spornost

Úplné systémy logických spojek:

• ⋁ , ⋀ , ¬
• NOR (¬, )
• NAND (¬, )
• XOR, ⇒
• ¬, ⇒
• ⇔, NOR
• ⇔, ⋁ , XOR
• ⇔, ⋀, XOR
• ⇔, NAND

Predikátová logika

• atomická formule -- pokud P je predikát a t1..tn jsou termy pak P(t1..tn), t1=t2 jsou atomické formule
• generalizace -- náhrada konstanty proměnnou P ├ (∀x)P(x)
• Herbrandovo universum -- konstanty + funkce s konstantami + funkce s funkcemi s konstantami + ...
• Herbrandova báze -- predikáty s konstantami + predikáty s funkcemi a konstantami + ...
• predikát -- n-ární relace
• prenexová normální forma -- formule se všemi kvantifikátory na začátku, zachovává ekvivalenci i splnitelnost
• sentence -- uzavřená formule - má pouze vázané proměnné
• skolemizace -- odstranění ∃ (nahrazení funkcemi, nulární funkce jsou konstanty); zachová splnitelnost formulí
• specializace -- náhrada proměnné konstantou - (∀x)P(x) ├ P(a)
• substituce -- zobrazení z množiny proměnných do množiny termů (tohle/za_tohle), substituovat lze pouze za volné proměnné
  • přejmenování -- proměnné, např. x|x1: P(x) > P(x1)
  • unifikace -- substituce, po jejíž aplikaci na množinu termů dostaneme jeden term
  • nejobecnější unifikátor -- substituce, jejíž aplikací na dva či více výrazů získáme identitu; existuje jen jeden
• syntax -- jazyk predikátové logiky je složen ze:
  • logických symbolů -- spočetná množina objektových proměnných, výrokové logické spojky, obecný a existenční kvantifikátory
  • speciálních symbolů -- neprázdná množina predikátových symbolů, množina symbolů funkčních a množina symbolů konstantních
  • pomocných symbolů -- závorky, čárka: „( ) , [ ]"
• syntax formule -- definice
  • každá atomická formule je formule
  • jsou-li & a Ł formule pak (& ⋁ Ł) ,(& ⋀ Ł), ... jsou formule
  • je-li & formule a x proměnná pak (∀x &), (∃x &) jsou formule
  • nic jiného není formule
• teorém -- formule systému, která je v něm dokazatelná
• term -- konstanta, proměnná, funkce f pokud f(t1..tn) kde t1..tn jsou termy, nic jiného není term
  • nabývá hodnoty z dané domény
  • uzavřený term -- term neobsahující proměnnou
• věta o implikaci (modus ponens) -- když A a zároveň (A ⇒ B) ├ B

Kvantifikátory

∀ ... všeobecný kvantifikátor (pro všechna platí)

∃ ... existenční kvantifikátor (existuje alespoň jeden)

¬(∀xP(x)) ⇔ ∃x¬P(x)

¬(∃xP(x)) ⇔ ∀x¬P(x)

Rezoluce

obecná rezoluce -- můžeme si dělat, co chceme; pro predikátovou logiku je korektní a úplná

lineární rezoluce -- vždy rezolvujeme s předchozí rezolventou, můžeme použít dříve odvozené rezolventy; pro predikátovou logiku i výrokový počet je korektní a úplná

LI-rezoluce -- začínáme vždy cílovou klauzulí (s všemi negativními literály), právě odvozená klauzule musí být použita v bezprostředně následujícím rezolučním kroku, střední klauzule se nemůže později použít jako klauzule boční; pro výrokový počet je korektní, ale není úplná

LD-rezoluce -- používáme pouze Hornovy klauzule, klauzule jsou uspořádané (místo množiny použijeme seznam); právě odvozená klauzule musí být použita v bezprostředně následujícím rezolučním kroku, pro výrokový počet je korektní, ale není úplná

SLD-rezoluce -- používáme pouze Hornovy klauzule, klauzule jsou uspořádané (místo množiny použijeme seznam), vybereme jedno pravidlo podle kterého rezolvujeme a nadále se ho musíme držet (např. vždy první literály), právě odvozená klauzule musí být použita v bezprostředně následujícím rezolučním kroku, střední klauzule se nemůže později použít jako klauzule boční; pro výrokový počet je korektní, ale není úplná

T-rezoluce -- žádná z rodičovských klauzulí není tautologie

Další logiky

modální logika -- existují různé světy a v nich jsou různá tvrzení, která jsou buď nutná, nebo možná (□ box = nutnost (nebe je modré); ♢ diamond = možnost (člověk má 3 oči))

• kripkeho rámec -- jedná se o graf, kde každý vrchol je jedním ze světů
  • příklad: Pepa je v Praze (w1) a ví, že v Praze platí s (svítí sluníčko). Ví, že existuje Brno, ale neví, jestli pro Brno platí s, nebo nikoliv. Proto pro něj existují 2 světy Brno (w2, w3), kde jeden svět je, že pro Brno platí s a druhý, že nikoliv. Kripkeho rámec by tedy vypadal nějak takto: (w3)<-(w1)->(w2); pro w1 platí s, pro w2 neplatí s, pro w3 platí s.

temporální logika -- výroková temporální logika

• F – bude platit někdy v budoucnosti
• G – bude platit vždy v budoucnosti
• P – platilo někdy v minulosti
• H – platilo vždy v minulosti

minimální temporální logika -- nemá omezení

• T – množina časových bodů
• R – relace následnosti na T

vícehodnotové logiky -- pravda, nepravda, nevím

• mlhavá (fuzzy) logika -- interval <0;1> čím blíže jsme k 1, tím je vyšší jistota platnosti
• intuicionistické logiky -- není pravda jen to, co nelze sestrojit
• 3-hodnotová Lukasziewiczova logika -- pravdivostní funkce pro implikaci val(p => q) je min{1,1-val(p)+val(q)}