Shrnutí na Formální a predikátová logika

## Úvod Formální logika je sada metod a zápisů pro přesné vyjadřování tvrzení o objektech, vztazích a důkazech. Cílem tohoto materiálu je poskytnout srozumitelný přehled základních témat, postupů a užitečných triků, které se objevují v úlohách z formální logiky (např. formulace jazyka, skolemizace, PNF, rezoluce, modus ponens, modely teorií). Materiál je koncipován pro samostudium a má usnadnit orientaci a přípravu na cvičení nebo zkoušku. ## Základní části a postupy Níže rozložíme často se opakující úlohy na menší kroky, doplníme definice, příklady a praktické tipy. ### 1) Formulace jazyka (výrok: jak přepsat zadání do FOL) - Cílem: vytvořit formuli v predikátové logice 1. řádu, která přesně popisuje text zadání. - Postup: 1. Identifikujte kvantifikátory: text typu „každé“, „všechna“ → $orall$, text typu „existuje“ → $\\exists$. 2. Určete predikáty/funkční symboly: např. $even(x)$, $odd(x)$, $dir(x)$. 3. Přidejte podmínky (složené pomocí $\\land$, $\\lor$, $\\to$, negace $\\neg$) přesně tak, jak uvádí zadání. 4. Kontrola: čtení formule nahlas často odhalí chyby. > Definice: Formulace jazyka je formule predikátové logiky, která pomocí kvantifikátorů a predikátů přesně zachycuje tvrzení v přirozeném jazyce. Praktický příklad: „Mezi každými dvěma různými sudými čísly existuje liché číslo.“ - Krok 1: dvě proměnné → $orall x\\forall y$. - Krok 2: obě sudá: $even(x)\\land even(y)$. - Krok 3: různá a uspořádání: $x<y$ (nebo $x\neq y$ dle zadání). - Krok 4: existence lichého mezi nimi: $\\exists z\,(odd(z)\\land x<z\\land z<y)$. - Výsledná formule: $$\\forall x\\forall y\,\bigl((even(x)\\land even(y)\\land x<y)\\to \\exists z\,(odd(z)\\land x<z\\land z<y)\bigr)$$ Tip: Ve většině vět platí, že $\\forall$ části uvádějí předpoklady a tvar implikace $(P\\to Q)$, kde $P$ jsou podmínky o proměnných a $Q$ je existence nebo jiná závěrečná podmínka. Zajímavost: V praxi se někdy nelze do signatury automaticky doplnit nové predikáty; pokud v zadání máte jen $dir(x)$ (adresář), ale potřebujete "soubor", lze ho modelovat jako $\\neg dir(x)$, pokud to je v kontextu rozumné. ### 2) Prenexní normální forma (PNF) a Skolemizace - Cíl PNF: přesunout všechny kvantifikátory před samotnou formuli, aniž by se změnil význam (kromě volných proměnných). - Skolemizace: odstranění existenčních kvantifikátorů zavedením Skolemových funkcí, aby vznikla ekvivalentní formule vhodná pro rezoluci. Základní postup PNF: 1. Eliminuje se logické ekvivalence a implikace. 2. Přesouvají se negace dovnitř pomocí De Morganových zákonů a pravidla dvojnásobné negace. 3. Zajištění, že kvantifikátory se netýkají vzájemně konfliktujících proměnných (přejmenování proměnných). 4. Kvantifikátory se vytahují před formuli. Skolemizace (jednoduchý postup): 1. Mějme formuli v PNF: $\\forall x\\exists y\,P(x,y)$. Pro odstranění $\\exists y$ zavedeme Skolemovu funkci $f(x)$ a nahradíme $y$ výrazem $f(x)$. 2. Po Skolemizaci dostaneme: $\\forall x\,P(x,f(x))$ a eliminujeme $\\exists$ (funkce je pevná, tedy neexistuje již kvantifikátor pro $y$). Příklad (krátce): $$\\forall x\\exists y\,R(x,y)$$ Skolemizace → $$\\forall x\,R(x,f(x))$$ ### 3) CNF a DNF (převod mezi nimi) - DNF (disjunktivní normální forma): disjunkce konjunkcí literálů; vhodná, když chceme přímo číst pravdivé řádky tabulky pravdivosti. - CNF (konjunktivní normální forma): konjunkce disjunkcí literálů; vhodná pro rezoluční důkazy. Převod z pravdivostní tabulky: - DNF: vezměte řádky, kde je výsledek 1; pro každý takový řádek vytvořte konjunkci literálů (proměnná je negovaná, pokud v řádku má 0). Nakonec spojte tyto konjunkce disjunkcí. - CNF: vezměte řádky, kde je výsledek 0; pro každý takový řádek vytvořte disjunkci literálů (proměnná je nenegovaná, pokud v řádku má 0). Nakonec spojte tyto disjunkce konjunkcemi. Příklad DNF (čtyři řádky s hodnotou 1): $$(\\neg x\\land\\neg y\\land z)\\lor(\\neg x\\land y\\land\\neg z)\\lor(x\\land\\neg y\\land\\neg z)\\lor(x\\land\\neg y\\land z)$$ Příklad CNF (čtyři řádky