Section outline

  • General

    Collapse all Expand all
    • Výběr skupiny Group self-selection
      Students must
      Mark as done

      Umožní studentům vybrat skupinu. Až potom se zobrazí obsah sekce konkrétního cvičícího.

    • Opravný zápočtový test Choice

      Opravný test z predikátové logiky plánuji pondělí 13.1. v 11:00 v S8.

      Vyhovuje? Raději středa 9:00?

  • Cvičení M. Vomlelové

  • Cvičení Jan Hric CT+PA

    Požadavky na zápočet:
     

    Dosáhnout 140 bodů z celkem 250 b. (Požadavky jsou synchronizované přes cvičení v rámci přednášky.) Budou 2 zápočtové písemky za 100 b, na výrokovou logiku a predikátovou logiku. Dalších 50 bodů bude za Domácí Úkoly. Jeden (hlavní) z nich za 40b. bude použít SAT solver.

    DU: Na cvičení a v Moodlu zadám příklad. Standardní odevzdání do Moodlu do příštího cvičení, do dalšího cvičení pak opravím a ohodnotím a v Moodlu máte zpětnou vazbu. Můžete odevzdávat dokumenty (.pdf), s .txt a .doc jsou trochu problémy, nebo přefocené obrázky (.jpg).

    O úkolech se můžete diskutovat a poradit se se spolužáky, ale odevzdané řešení má být Vaše práce. Můžete se taky "poradit" s ChatGPT (doporučení: nedělejte to), ale za správnost ručíte vy.

    Materiály:

    Příklady na první cca. 2 cvičení + SAT solver:

    https://ktiml.mff.cuni.cz/%7Ehric/vyuka/prikl_vpl.htm

    Přednáška: ZS 2024/25: u Jakuba Bulína, učební text

    https://ktiml.mff.cuni.cz/~bulin ... (nebo jinde podle instrukcí přednášejícího)

    Přednáška: ZS 2021/22:

    Stránka přednášky VPL u Petra Gregora: https://ktiml.mff.cuni.cz/~gregor/logika/index.html

    Stránka cvičení (které budeme používat): https://ktiml.mff.cuni.cz/~gregor/logika2019/cviceni.html

    ZOOM (až pro distanční výuku, bude v případě potřeby)

    https://cuni-cz.zoom.us/...   

  • Archiv JH: výuka 2022

    • Z 1. Cvičení na rozmyšlení Journal
      Students must
      Mark as done

      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).

    • DÚ1 2022 do CNF, zadan 6./7.10.2022 Assignment
      Students must
      Mark as done

      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.

    • DU2 2022 nand Assignment
      Students must
      Mark as done

      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 )\).

    • DU4 Patek: semantika struktury Assignment
      Students must
      Mark as done

      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)(φ → ψ)

    • DU5 Tablo pro PL Assignment
      Students must
      Mark as done
    • Vysledky pisemky1: VL (čtvrtek a pátek) Assignment
      Students must
      Mark as done

      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: predikátová logika (Čt, Pá) Assignment
      Students must
      Mark as done

      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

    • Opravné písemky: VL Assignment
      Students must
      Mark as done

      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

       

    • Opravná písemka: PL Assignment
      Students must
      Mark as done

      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čet Journal
      Students must
      Mark as done

      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.

    • Náhradní, výroková část File PDF
      Students must
      Mark as done
      99.3 KB
    • Náhradní, predikátová část File PDF
      Students must
      Mark as done
      264.0 KB

  • Nahrávky cvičení 2020/21 Jan Hric, Zoom