Osnova sekce

  • Important information / důležité informace

    Sbalit vše Rozbalit vše

    EN: Below you will find syllabus and resources for my English lecture (Tuesday 10:40am in S9), English tutorial (Wednesday 3:40pm in S1), and Czech tutorial (Thursday 9:00am in S6). Please use the discussion forum for discussing course material and exercises whenever possible. You need to enroll in the course to see the materials.

    CZ: Níže najdete program a výukové materiály pro mou anglickou přednášku (Út 10:40 v S9), anglické cvičení (St 15:40 v S1) a české cvičení (Čt 9:00 v S6). Používejte, prosím, diskuzní fórum kdykoliv je to možné. Zapište se, prosím, do tohoto kurzu, materiály budou přístupné pouze zapsaným studentům.


    • Discussion Forum / Diskuzní fórum
    • Lecture notes Soubor
    • Slides Soubor
    • Math background Soubor
    • Organization of the exams (will be updated) Soubor

    • Sample exam tests:

       

  • Week 14 (Jan 4-8)

    • English lecture
      • Program: Definable sets and automorphisms. Omega-categoricity. Axiomatizability. Undecidability and Incompleteness.
      English tutorial
      • Program: Resolution in predicate logic.
      České cvičení
      • Program: Rezoluce v predikátové logice.
    • English lecture: Zoom recording Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 13 (Dec 21-22)

    • English lecture
      • Program: Lifting lemma, completeness of resolution, linear resolution, LI-resolution and Prolog. Hilbert proof system in predicate logic. Theory of a structure. Corollaries of the Löwenheim-Skolem Theorem. Elementary equivalence and isomorphism.
      English tutorial
      • Program: Skolemization, conversion to CNF, resolution in predicate logic.
      České cvičení
      • Program: Skolemizace. Herbrandův model. Převod do CNF. Rezoluce v predikátové logice.
    • English lecture: Zoom recording Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor
    • English tutorial: 4th homework assignment Úkol
    • České cvičení: 4. domácí úkol

  • Week 12 (Dec 14-18)

    • English lecture
      • Program: Resolution in predicate logic. Unification algorithm, the general resolution rule, soundness of resolution, lifting lemma.
      English tutorial
      • Program: Compactness theorem. Extension by definitions. Prenex normal form, skolemization. Herbrand universe.
      České cvičení
      • Program: Tablo metoda v predikátové logice. Extenze o definice. Skolemizace.
    • English lecture: Zoom recording Soubor
    • English tutorial: Worksheet 7 Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Příklady 7 Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 11 (Dec 7-11)

    • English lecture
      • Program: Compactness theorem. Extensions of theories, extension by definition. Skolemization, Skolem's theorem. Herbrand model, Herbrand's theorem and its corollaries.
      English tutorial
      • Program: Definable sets. Tableau method in predicate logic. Theorem on constants, deduction theorem.
      České cvičení
      • Program: Definovatelné množiny. Tablo metoda v predikátové logice. 
    • English lecture: Zoom recording Soubor
    • English tutorial: Worksheet 6 Soubor
    • English Tutorial: Zoom recording URL
    • České cvičení: Příklady 6 Soubor
    • České cvičení: Zoom záznam Soubor
    • English tutorial: 3rd homework assignment Úkol
    • České cvičení: 3. domácí úkol

  • Week 10 (Nov 29-Dec 3)

    • English lecture
      • Program: Tableau method in predicate logic, soundness and completeness, canonical model, role of equality.
      English tutorial
      • Program: Semantics of predicate logic. Models and theories, substructures, completeness, extensions. Definable sets.
      České cvičení
      • Program: Sémantika v predikátové logice. Teorie, modely, podstruktury.
    • English lecture: Zoom recording Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 9 (Nov 22-26)

    • English lecture
      • Program: Substructures, definable sets, tableau method in predicate logic.
      English tutorial
      • Program: Semantics of predicate logic.
      České cvičení
      • Program: Syntaxe a sémantika v predikátové logice.
    • English lecture: Zoom recording Soubor
    • English tutorial: Worksheet 5 Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor
    • English tutorial: 2nd homework assignment Úkol
    • České cvičení: 2. domácí úkol

  • Week 8 (Nov 15-19)

    • English lecture
      • Program: Basic syntax and semantics of predicate logic. Structures. Properties of theories.
      English tutorial
      • National holiday - there is no tutorial.
      České cvičení
      • Rezoluční metoda, syntaxe a sémantika predikátové logiky.
    • České cvičení: Příklady 5 Soubor
    • English lecture: Zoom recording Soubor
    • English Tutorial: Zoom recording Soubor

  • Week 7 (Nov 8-12)

    • English lecture
      • Program: Tree of reductions, completeness of resolution. Linear resolution, soundness and completeness. Linear input (LI) resolution and its completeness for Horn formulas. Resolution and Prolog. Intro to predicate logic.
      English tutorial
      • Program: Compactness theorem. Resolution in propositional logic.
      České cvičení
      • Program: Tablo metoda. Věta o kompaktnosti. Rezoluce ve výrokové logice.
    • České cvičení: Příklady 4 Soubor
    • English lecture: Zoom recording - part 1 Soubor
    • English lecture: Zoom recording - part 2 Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 6 (Nov 1-5)

    • English lecture
      • Program: Soundness and Completeness of Tableau method in propositional logic. Compactness theorem. Resolution in propositional logic. Soundness of resolution. Resolution proof, resolution tree, resolution closure.
      English tutorial
      • Program: Properties of theories. Tableau method in propositional logic.
      České cvičení
      • Program: Kódování problémů do SAT. Vlastnosti výrokových teorií, sémantické pojmy, extenze, důsledky. Lindenbaum-Tarski algebra výroků. Tablo metoda ve výrokové logice.
    • English lecture: Zoom recording Soubor
    • English tutorial: Worksheet 4 Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor
    • České cvičení: Příklady 3 Soubor
    • České cvičení: 1. domácí úkol

  • Week 5 (Oct 25-29)

    • English lecture
      • Program: Formal proof systems. Tableau method for propositional logic, tableau proof and refutation, systematic tableaux, finiteness of proofs.
      English tutorial
      • Program: Properties of theories, semantic notions, extensions, consequences. Lindenbaum-Tarski algebra, counting up to equivalence and T-equivalence. Intro to tableaux.
      České cvičení
      • Program: státní svátek
    • English tutorial: 1st homework assignment Úkol
    • Atomic tableaux Soubor
    • English lecture: Zoom recording Soubor
    • English tutorial: Worksheet 3 Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 4 (Oct 18-22)

    • English lecture
      • Program: SAT solvers, Horn-SAT, unit propagation. Theories, semantic notions, consequences. Lindenbaum-Tarski Algebra
      English tutorial
      • Program: Converting formulas to CNF and DNF, 3-SAT, 2-SAT, implication graph. Horn-SAT, unit propagation. Encoding problems in SAT.
      České cvičení
      • Program: Normální formy, CNF a DNF, SAT, 3-SAT, 2-SAT a implikační algoritmus, Horn-SAT a jednotková propagace.
    • English lecture: Zoom recording (Fall 2021) Soubor
    • English lecture: Zoom recording (Fall 2020) Soubor
    • English Tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 3 (Oct 11-15)

    • English lecture
      • Program: Adequacy of logical connectives. Normal forms, CNF and DNF, SAT and SAT solvers. 2-SAT, implication graph algorithm.
      English tutorial
      • Program: Adequacy of logical connectives. Expressing properties in predicate logic. Theories. Normal forms, CNF and DNF. 
      České cvičení
      • Program: Univerzálnost logických spojek. Vyjadřování vlastností v predikátové logice. Teorie. Normální formy, CNF a DNF, SAT, 3-SAT.
    • English lecture: Zoom recording URL
    • English tutorial: Worksheet 2 Soubor
    • English Tutorial: Zoom recording (part 2) Soubor
    • English Tutorial: Zoom recording (part 1) Soubor
    • České cvičení: Příklady 2 Soubor
    • České cvičení: Zoom záznam Soubor

  • Week 2 (Oct 4-8)

    • English lecture
      • Program: Introduction and overview of the course. Basic syntax and semantics of propositional logic. 
      English tutorial
      • Program: Basic syntax and semantics of propositional logic. 
      České cvičení
      • Program: Syntaxe a sémantika výrokové logiky
    • English lecture: Last year's Zoom recording Soubor
    • English tutorial: Worksheet 1 Soubor
    • České cvičení: Příklady 1 Soubor
    • English tutorial: Zoom recording Soubor
    • České cvičení: Zoom záznam (od 08:10) URL

  • Week 1 (Sep 29–Oct 1)

    • English lecture
      • There is no lecture this week (classes only start on Wednesday). However, there is a reading assignment due next Monday.
      English tutorial
      • Program: Intro. Propositional and predicate logic. Formalizing statements.
      České cvičení
      • Program: Úvod. Výroková a predikátová logika. Formalizace vyroků.
    • English tutorial: Worksheet 0 Soubor
    • České cvičení: Příklady 0 Soubor
    • České cvičení: Zoom záznam Soubor