Archiv JH: výuka 2022
Section outline
-
-
2022/23 1. cvičení před přednáškou
- Formulí 2. řádu \(\phi(G)\) charakterizovat "graf G je bipartitní".
- Pro daný graf G napsat formuli ve výrokové logice, která vyjadřuje "graf G lze obarvit 3 barvami".
Návod: zavést pro každý vrchol 3 výrokové proměnné a (konjunkcí) formulí F charakterizovat požadové grafy, tj. formule F je splnitelná (tj. má pravdivé ohodnocení v), právě když je G 3-obarvitelný. (I ve skriptech.) Správné obarvení O grafu G určí pravdivé ohodnocení v formule F a zároveň se z ohodnocení v dá vyčíst/zrekonstruovat O. ( O: V(G) -> {0,1,2} )
Pozn.: 3 barvy můžete reprezentovat 2 bity/proměnnými, ale vede to na složitější formule. Obvykle se používá unární reprezentace stavů/čísel a nikoli binární reprezentace (při převodu do SATu).
-
Máme formuli: \( (p \leftrightarrow q) \to (p \wedge \neg r ) \)
a) najděte všechny její modely (nad {p,q,r})
b) převeďte (včetně stručného postupu) do CNF - konjunktivní normální formy
--
CNF lze zjednodušit na \( (p \vee q) \wedge (\neg p \vee \neg q \vee \neg r ) \), protože \( (p \vee q) \to (p \vee q \vee \neg r ) \). (Subsumpce)
Formule se obvykle převádějí do CNF ekvivalentními úpravami (včetně zjednodušování), ne pomocí (ne)modelů z tabulky.
-
Moje př. 2/3.
Ukažte, že \(\{\uparrow\}\) , tj. pouze spojka nand, tvoří univerzální množinu spojek. Víme, že \( p\uparrow q \sim \neg(p \wedge q )\).
-
cvičení 7 Petra Gregora, příklad 4:
Zdůvodněte (sémanticky) následující vztahy. Pro každou strukturu A, formuli φ, sentenci ψ,
(a) A |= (ψ → (∃x)φ) ⇔ A |= (∃x)(ψ → φ)
(b) A |= (ψ → (∀x)φ) ⇔ A |= (∀x)(ψ → φ)
(c) A |= ((∃x)φ → ψ) ⇔ A |= (∀x)(φ → ψ)
(d) A |= ((∀x)φ → ψ) ⇔ A |= (∃x)(φ → ψ) -
Vysledky, konkretne ziskane body za jednotlive podulohy, ve tvaru (pro čtvrtek) "1a 1b 1c ; 2a 2b 2c" a (pro pátek) "1a 1b 1c 1d ; 2a 2b 2c". Celkem max. 12 bodu, požadováno 8 bodů.
Pro připomenutí, čtvrtek:
1a Dokažte tablem (3b), 1b počet neekvivalentních nezávislých výroků (2b), 1c příklad nezávislého výroku (1b)
2a Modely T a axiomatizace v CNF (2b), 2b dokažte rezolucí (3b), 2c vlastnosti rozšíření (1b)
- Pátek
1a Dokažte tablem (2b), 1b počet neekvivalentních nezávislých výroků (2b), 1c příklad nezávislého výroku (1b), 1d vztahy pro množiny modelů (1b)
2a Modely T a axiomatizace v CNF (2b), 2b dokažte rezolucí (3b), 2c vlastnosti rozšíření (1b)
---- časté chyby:
- nemate Moodle :-o
- špatný přepis formule, následně dokazujete něco jiného (u 1/3 odpovědí)
- neúplná odpověď pro otázku s více částmi nebo odpověď ne v požadovaném tvaru
-
Písemka 2 z predikátové logiky bude Čt 22.12. a Pá 6.1.2023
-- Body pro jednotlivé příklady doplněny.
Čt: 1. (3b) Dk. tablem ; 2. (2b) Strukt. pro neplatnost formule ; 3. (3b) Převod: prenexní tvar, Skolemizace, množ. tvar ; 4. (2b) Rezoluce ; 5. (2b) Definovatelnost v grafu
Pá: 1. (3b) Dk. Tablem s teorií ; 2. (1+1b) Definice rovnosti + funkčního symbolu ; 3. (2+3b) Převod + rezoluce ; 4. (2b) Strukt. pro neplatnost formule
---- časté chyby:
Tablo: začít uzávěrem formule (a pracovat s uzavřenými formulemi), tablo pro kvantifikátor odstraní tento kvantifikátor, nelze použít tablo pro spojku pod kvantifikátorem, změna a úprava formule na ekvivalentní, špatné zavádění konstant, špatné pořadí zavádění konstant (nejdřív svědek, pak všichni), substituce za konstantu ...
Pa 2a. Místo rovnosti: f (resp. P) je symetrická, jen speciální případy
Rezoluce: Začít negací uzávěru, ne uzávěrem negace ; špatné unifikace a substituce včetně dosazování za konstanty a termy
-
Opraveno, body zveřejněny, i podrobné body. (Ať víte, co se máte doučit)
Max. bodů 12: 1, 1, 3, 1, 1 / 3, 1, 1
Příklady (pro připomenutí): 1a) Formalizovat 'sněžení', b) příprava rezoluce, na klauzule, c) rezoluce, d) modely, e) počet nezávislých výroků ; 2a) tablo, b) extenze na JKE, c) nekonzervativní extenze
-
Max. bodů 12 : 2, 3, 1 ; 2, 4
Opraveno, body celkové i podrobné
Příklady: 1a) příprava na rezoluci, b) rezoluce, c) Herbrandovo univerzum ; 2a) Formalizace (počítačových) "virusů", b) tablo
----- časté chyby
1a) Dokazovaná formule se upraví na negaci uzávěru. Z původně volných proměnných vzniknou obecné kvantifikované, díky negaci existenčně kvantifikované a následně díky Skolemizaci konstanty.
-
Zápočty jsou zapsané, za 14 bodů v součtu
Pokud jste "těsně" pod limitem, tj. máte aspoň 12 bodů, vypracujte správně všechny náhradní příklady (VL a PL), příklady jsou z posledních písemek.
AD: Odevzdejte u minulých dvou položek ("nahradni písemka") nebo pošlete mailem.
-
-
-