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]