In order to pass the course (grade 3) the student should
Propositional logic: combinatorial problems as propositional problems. Methods for efficient solution and representation of propositional problems (DavisPutnam, BDDs).
Modal logic: possible worlds semantics, Kripke models.
Interpretations of modal logic: Temporal logic and epistemic logic. Applications in model checking.
Equational logic: terms, unification, universal algebra, equational reasoning, term rewriting.
Predicate logic and proof search: the completeness theorem, proof search in some calculi (tableaux, resolution).
Solvable and unsolvable problems: complete and decidable theories, quantifier elimination, Gödels incompleteness theorem (without proof).
Constructive logic and type theory: lambda calculus, simple type theory, intuitionistic logic, Martin-Löf type theory, propositions-as-types, program extraction from proofs, logical frameworks, proof support systems (Coq, Hol, Isabelle or Agda).
Lectures and problem solving sessions.
Written and, possibly, oral examination at the end of the course. Moreover, compulsory assignments may be given during the course.
Lägerhyddsvägen 1, Hus 1, 5 och 7 75106 Uppsala
Box 480, 751 06 UPPSALA
Telephone: 018-471 3200
Fax: 018-471 3201