Požadavky: 2/3 bodů z možných, tj. zadaných příkladů. Příklad za 5 bodů, pokud není řečeno jinak. Standardní doba pro řešení: 1 týden, tj. do dalšího cvičení.
- DU x Dokažte tablem:
- $(p \to(q\to r)) \to((p \to q)\to (p\to r))$
-
- DU x Nechť $\varphi$ je výrok $\neg (p \land q) \to (\neg p \lor \neg q)$.
- (a) Převeďte $\neg \varphi$ do CNF a množinové reprezentace.
- (b) Najděte rezoluční zamítnutí $\neg \varphi$, tj. důkaz $\varphi$.
- DU 4/2019 Nechť $\varphi$ je výrok $\neg (p \lor q) \to (\neg p \land \neg q)$.
- (a) Dokažte $\varphi$ tablem.
- DU 5/2019 (PG2019.5.6) Dokažte rezolucí $T \models s$, kde
- (a) $T = \{ \neg p \to \neg q, \neg q \to \neg r, (r \to p) \to s\}$
-
- DU 6/2019 (PG2018/6.9) Dokažte (sémanticky z definic) nebo vyvraťte nalezením protipříkladu:
pro každou $\varphi$ platí:
- (a) $\varphi \models (\forall x) \varphi$
- (b) $\models \varphi \to (\forall x) \varphi$
- (c) $\varphi \models (\exists x) \varphi$
- (d) $\models \varphi \to (\exists x) \varphi$
- DU x/2018 Dokažte tablem:
- $(\forall x P(x) \to R) \leftrightarrow \exists x(P(x)\to R)$
-
Archiv 2019:
Výsledky: v SISu (v záznamníku učitele) u cvičení si najděte svůj pseudokód, pod tímto pseudokódem budou vaše výsledky z DU na mojí stránce.
Náhradní příklady na konci.
DU1/CV1(3.10.2019): PG2018/1.2a. Pro daný graf G, sestrojte výrokovou formuli,
která je splnitelná, právě když je graf bipartitní.
DU2/CV2(10.10.2019, ): SAT Solvery.2.2 Popište konstrukci formule v CNF.
DU3/CV2(do 6.11.2019 St, 10 bodů): Úloha jako DU2. a/ Nainstalujte si (některý) SAT-solver. b/ Naprogramujte vytváření .cnf souboru v závislosti na $n$, tj. délce řetězce. c/ Najděte největší $n_{max}$, pro které požadovaný řetězec existuje (pomocí části b/ a SAT solveru z a/). d/ Pošlete mi e-mailem v ZIPu nalezené $n_{max}$, počty proměnných a klauzulí ve vygenerovaných .cnf souborech pro $k, 4\le k \le n_{max+1}$ a zdrojáky použité pro generování .cnf souborů. (update:) A vygenerovane .cnf soubory pro $n_{max}$ a $n_{max+1}$.
DU4/CV3 (17.10.) Tablo: PG2018/4.4c
DU5/CV5 (31.10., do 7.11.) Rezoluce: PG2019/5.6 a totéž níže.
A taky DU3 je do 6.11. (středa)
DU6/CV6 (7.11.) PG2018/6.9 Dokažte nebo vyvraťte (sémanticky z definic): ...
- Pokud posíláte fotku nebo sken řešení e-mailem, napište i na papír své jméno.
-
Náhradní příklady, každý za 2 chybějící body (po správném vyřešení).
Některé odkazují na cvičení Petra Gregora 2019/číslo-cvičení/číslo-příkladu.
Vyberte si nejdřív z prvních 3 příkladů (až všechny), pak z dalších.
- Náhradní N1/2019 Teorie těles a skolemizace PG2019/12/1abc
- Náhradní N2/2019 Teorie T a extenze PG2019/9/1abcd
- Náhradní N3/2019 Nesplnitelná konjunkce základních klauzulí PG2019/12/9
- Náhradní N4/2019 Najděte a popište (spočetně) nekonečnou strukturu $\langle X, \le \rangle$,
která je model lineárního uspořádání, má největší a nejmenší prvek a není to ${\it DeLO^{\pm}}$.
Zdůvodněte, že se liší od struktur v PG2019/13/4.
- Náhradní N5/2019 DeLO s konstantou PG2019/13/6
- Náhradní N6/2019 Důkaz v PA PG2019/13/9a
- Náhradní N7/2019 Prenexní tvar a Skolemova varianta PG2019/11/3c+4c