Propositional and Predicate Logic

Weekly outline

• Select week Important information / důležité informace

  Important information / důležité informace

  Collapse all Expand all

  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.

  
  

  • Select activity Discussion Forum / Diskuzní fórum

    

    Discussion Forum / Diskuzní fórum

    Not available unless: You belong to any group
  • Select activity Lecture notes

    

    Lecture notes File

    Not available unless: You belong to English lecture
  • Select activity Slides

    

    Slides File

    Not available unless: You belong to English lecture
  • Select activity Math background

    

    Math background File

    Not available unless: You belong to English lecture
  • Select activity Organization of the exams (will be updated)

    

    Organization of the exams (will be updated) File

    Not available unless: You belong to English lecture
  • Select activity Sample exam tests:   Sample exam 1 with soluti...

    Sample exam tests:

     

    • Sample exam 1 with solutions
    • Sample exam 2 with solutions
    • Sample exam 3
    • Sample exam 4
    • Sample exam 5
    • Sample exam 6
    • Sample exam 7
    • Sample exam 8
    • More exams from previous years

    Not available unless: You belong to English lecture
• Select week Week 14 (Jan 4-8)

  Week 14 (Jan 4-8)
  • Select activity English lecture Program: Definable sets and aut...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 13 (Dec 21-22)

  Week 13 (Dec 21-22)
  • Select activity English lecture Program: Lifting lemma, complet...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
  • Select activity English tutorial: 4th homework assignment

    

    English tutorial: 4th homework assignment

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: 4. domácí úkol

    

    České cvičení: 4. domácí úkol Assignment

    Not available unless: You belong to české cvičení
• Select week Week 12 (Dec 14-18)

  Week 12 (Dec 14-18)
  • Select activity English lecture Program: Resolution in predicat...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 7

    

    English tutorial: Worksheet 7 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Příklady 7

    

    České cvičení: Příklady 7 File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 11 (Dec 7-11)

  Week 11 (Dec 7-11)
  • Select activity English lecture Program: Compactness theorem. E...

    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. 

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 6

    

    English tutorial: Worksheet 6 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording URL

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Příklady 6

    

    České cvičení: Příklady 6 File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
  • Select activity English tutorial: 3rd homework assignment

    

    English tutorial: 3rd homework assignment

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: 3. domácí úkol

    

    České cvičení: 3. domácí úkol Assignment

    Not available unless: You belong to české cvičení
• Select week Week 10 (Nov 29-Dec 3)

  Week 10 (Nov 29-Dec 3)
  • Select activity English lecture Program: Tableau method in pred...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 9 (Nov 22-26)

  Week 9 (Nov 22-26)
  • Select activity English lecture Program: Substructures, definab...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 5

    

    English tutorial: Worksheet 5 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
  • Select activity English tutorial: 2nd homework assignment

    

    English tutorial: 2nd homework assignment

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: 2. domácí úkol

    

    České cvičení: 2. domácí úkol Assignment

    Not available unless: You belong to české cvičení
• Select week Week 8 (Nov 15-19)

  Week 8 (Nov 15-19)
  • Select activity English lecture Program: Basic syntax and seman...

    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.

    Not available unless: You belong to any group
  • Select activity České cvičení: Příklady 5

    

    České cvičení: Příklady 5 File

    Not available unless: You belong to české cvičení
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
• Select week Week 7 (Nov 8-12)

  Week 7 (Nov 8-12)
  • Select activity English lecture Program: Tree of reductions, co...

    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.

    Not available unless: You belong to any group
  • Select activity České cvičení: Příklady 4

    

    České cvičení: Příklady 4 File

    Not available unless: You belong to české cvičení
  • Select activity English lecture: Zoom recording - part 1

    

    English lecture: Zoom recording - part 1 File

    Not available unless: You belong to English lecture
  • Select activity English lecture: Zoom recording - part 2

    

    English lecture: Zoom recording - part 2 File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 6 (Nov 1-5)

  Week 6 (Nov 1-5)
  • Select activity English lecture Program: Soundness and Complete...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 4

    

    English tutorial: Worksheet 4 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: Příklady 3

    

    České cvičení: Příklady 3 File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: 1. domácí úkol

    

    České cvičení: 1. domácí úkol Assignment

    Not available unless: You belong to české cvičení
• Select week Week 5 (Oct 25-29)

  Week 5 (Oct 25-29)
  • Select activity English lecture Program: Formal proof systems. ...

    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

    Not available unless: You belong to any group
  • Select activity English tutorial: 1st homework assignment

    

    English tutorial: 1st homework assignment

    Not available unless: You belong to English tutorial
  • Select activity Atomic tableaux

    

    Atomic tableaux File

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 3

    

    English tutorial: Worksheet 3 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 4 (Oct 18-22)

  Week 4 (Oct 18-22)
  • Select activity English lecture Program: SAT solvers, Horn-SAT,...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording (Fall 2021)

    

    English lecture: Zoom recording (Fall 2021) File

    Not available unless: You belong to English lecture
  • Select activity English lecture: Zoom recording (Fall 2020)

    

    English lecture: Zoom recording (Fall 2020) File

    Not available unless: You belong to English lecture
  • Select activity English Tutorial: Zoom recording

    

    English Tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 3 (Oct 11-15)

  Week 3 (Oct 11-15)
  • Select activity English lecture Program: Adequacy of logical co...

    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.

    Not available unless: You belong to any group
  • Select activity English lecture: Zoom recording

    

    English lecture: Zoom recording URL

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 2

    

    English tutorial: Worksheet 2 File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording (part 2)

    

    English Tutorial: Zoom recording (part 2) File

    Not available unless: You belong to English tutorial
  • Select activity English Tutorial: Zoom recording (part 1)

    

    English Tutorial: Zoom recording (part 1) File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Příklady 2

    

    České cvičení: Příklady 2 File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení
• Select week Week 2 (Oct 4-8)

  Week 2 (Oct 4-8)
  • Select activity English lecture Program: Introduction and overv...

    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

    Not available unless: You belong to any group
  • Select activity English lecture: Last year's Zoom recording

    

    English lecture: Last year's Zoom recording File

    Not available unless: You belong to English lecture
  • Select activity English tutorial: Worksheet 1

    

    English tutorial: Worksheet 1 File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Příklady 1

    

    České cvičení: Příklady 1 File

    Not available unless: You belong to české cvičení
  • Select activity English tutorial: Zoom recording

    

    English tutorial: Zoom recording File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Zoom záznam (od 08:10)

    

    České cvičení: Zoom záznam (od 08:10) URL

    Not available unless: You belong to české cvičení
• Select week Week 1 (Sep 29–Oct 1)

  Week 1 (Sep 29–Oct 1)
  • Select activity English lecture There is no lecture this week (...

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

    Not available unless: You belong to any group
  • Select activity English tutorial: Worksheet 0

    

    English tutorial: Worksheet 0 File

    Not available unless: You belong to English tutorial
  • Select activity České cvičení: Příklady 0

    

    České cvičení: Příklady 0 File

    Not available unless: You belong to české cvičení
  • Select activity České cvičení: Zoom záznam

    

    České cvičení: Zoom záznam File

    Not available unless: You belong to české cvičení