What we did in class

7th tutorial (Tuesday, November 19)

  • The first written test.

6th tutorial (Tuesday, November 5)

  • Tableau method: Constructing tableaux, systematic tableau, tableau proof/refutation, finding models of a theory. Atomic tableaux, Deduction Theorem.
  • [Worksheet 3], 7–9
  • [Worksheet 4], 1–3
  • Next Tuesday is Dean's day, classes are cancelled.
  • [Homework assignment #3] is due Tuesday, Nov 26 at the beginning of class.
  • The first written test is in two weeks.

5th tutorial (Tuesday, October 29)

  • Properties of theories, models, consequences. Lindenbaum-Tarski algebra of propositions, counting propositions/theories up to equivalence.
  • [Worksheet 3], 5–6
  • The first written test will be on Tuesday, November 19.
  • The 2nd homework assignment is due on Tuesday, November 5.

4th tutorial (Tuesday, October 22)

  • More on CNF and DNF. SAT: reduction to 3-SAT, encoding problems. 2-SAT, implication graph. Horn-SAT, unit propagation. Theories, consequences, properties, semantic notions.
  • [Worksheet 2], 2, 4, 5, 7, 12
  • [Worksheet 3],1–4
  • [Homework assignment #2], due Tuesday, Nov 5 at the beginning of class. If you want more graph colouring instances, look e.g. here.

3rd tutorial (Tuseday, October 15)

  • Programme: Homework solution. More on math. Adequacy of logical connectives. Models. CNF and DNF forms of formulas: using truth tables and syntactic rules.
  • [Worksheet 2], problems 1–4

2nd tutorial (Tuseday, October 8)

  • Programme: More syntax of propositional logic and Boolean operators. Defining properties in predicate logic. Graphs, equivalence relations, partial orders.
  • [Worksheet 1, problems 5–8]
  • [Homework assignment #1], due Monday noon, the SAT solver input is here: input.cnf

1st tutorial (Tuseday, October 1)

  • Programme: Introduction. Propositional and predicate (first-order, higher-order) logic. Syntax of propositional logic (expression/formation tree, prefix/infix/postfix notation). Semantics of propositional logic (Boolean operators, truth table, Venn diagram)
  • [Worksheet 1, problems 1–5]

General information

Credit requirements

There will be two written tests and several homework assignments. In order to obtain credit, you should gain 70% of the points. (Bonus points may be available.) Tentative dates of the tests:

  • November 19
  • January 7


Many in-class problems are taken from previous semesters, e.g. Petr Gregor's English tutorial or Czech tutorial Czech by Jan Hric. If you want extra practice, try exercises from the [book], or contact me.