Programme of lectures
5th class (Monday, November 11)
Topics: Compactness theorem, applications. Resolution method: resolution proof, resolution refutation, resolution tree, resolution closure, tree of substitutions, soundness and completeness, linear resolution.

Slides by Petr Gregor:
 [slides 4] 18–19
 [slides 5] 4–14

Lecture notes by Martin Pilát:
 [lecnotes] pp. 30–35
4th class (Monday, November 4)
Topics: Formal proof systems, soundness and completeness. Tableau method for propositional logic: tableau from a theory, systematic tableau, soundness theorem, completeness theorem. Syntactic properties of theories.

Slides by Petr Gregor:
 [slides 3] 10–19
 [slides 4] 1–17

Lecture notes by Martin Pilát:
 [lecnotes] pp. 23–30

Textbook "Logic for Applications" by A. Nerode and R. A. Shore
 [book] Chapters I.3 and I.4
3rd class (Monday, October 21)
Topics: Encoding problems in SAT. 2SAT, implication graph. HornSAT, unit propagation algorithm. Theories: semantic notions wrt. a theory, consequences (properties of the consequence operator). Properties of theories: consistency, completeness, extension (simple, conservative), equivalence. Analyzing theories via models, LindenbaumTarski Algebra of propositions.

Slides by Petr Gregor:
 [slides 2] 14–16
 [slides 3] 1–9

Lecture notes by Martin Pilát:
 [lecnotes] pp. 18–21
2nd class (Monday, October 14)
Topics: Syntax conventions. Basic semantics of propositional logic, terminology (truth value, model, satisfiability, ...). Adequacy of logical connectives. Normal forms, CNF and DNF (semantic and syntactic transformation), duality. The Boolean satisfiability problem, 2SAT.

Slides by Petr Gregor:
 [slides 2] 4, 6–14

Lecture notes by Martin Pilát:
 [lecnotes] pp. 14–17, 20

Textbook "Logic for Applications" by A. Nerode and R. A. Shore
 [book] pp. 16–26
1st class (Monday, October 7)
Topics: Introduction, overview of the course, brief history, applications of logic in computer science, basic syntax of propositional logic (language, formula, formation tree).

Slides by Petr Gregor:
 [slides 1] 1–12
 [slides 2] 1–5

Lecture notes by Martin Pilát:
 [lecnotes] pp. 1–14

Textbook "Logic for Applications" by A. Nerode and R. A. Shore
 [book] pp. 1–16