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.

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:
  • Lecture notes by Martin Pilát:
  • 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. 2-SAT, implication graph. Horn-SAT, 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, Lindenbaum-Tarski Algebra of propositions.

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, 2-SAT.

  • Slides by Petr Gregor:
  • Lecture notes by Martin Pilát:
  • 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:
  • Lecture notes by Martin Pilát:
  • Textbook "Logic for Applications" by A. Nerode and R. A. Shore
    • [book] pp. 1–16

General information

Tutorial

The lecture is accompanied by a tutorial. Obtaining credit for the tutorial is neccessary for passing the course. See the tutorial website for more information.

Exam requirements

The exam consists of a written test and oral examination. The written part precedes the oral part. If the written part is evaluated as unsatisfactory, the exam ends without taking the oral part. If the oral part is evaluated as unsatisfactory, both written and oral parts have to be repeated on the next exam term. Final grade is based on evaluation of both parts.

Obtaining credit from the seminar is a neccessary requirement for taking the exam. Exam dates will be available in SIS.

Syllabus

  • Propositional logic:
    • elementary syntax and semantics, normal forms of propositional formulas, problem of satisfiability.
    • Tableau method and resolution in propositional logic.
    • Completeness theorem for propositional logic.
  • Predicate (first-order) logic:
    • elementary syntax and semantics, prenex normal form of formulas, properties and models of first-order theories.
    • Tableau method and resolution for predicate logic.
    • Skolem's theorem, Herbrand's theorem.
    • Completeness theorem for predicate logic, compactness.
  • Criteria for completeness, decidability. Limits of formal methods, Goedel's theorems.