Syllabus for Applied Logic

Learning outcomes

On completion of the course, the student should be able to:

• give an account of the undecidability of predicate logic (Church's theorem);
• formulate the completeness theorem of propositional and predicate logic and explain its usage;
• use and describe methods for efficient representation and solution of problems in propositional logic;
• formalise problems in modal, propositional and predicate logic;
• explain different interpretations of modal operators and applications to model checking problems;
• reason model-theoretically in predicate and modal logic;
• give an account for some calculus and system for automatic proof search in predicate logic;
• give an account for some decision method for equational logic;
• use a proof support system based on a logical framework;
• explain the algorithmic interpretation of intuitionistic logic and the principles of program extraction from proofs.

Content

Propositional logic: combinatorial problems as propositional problems. Methods for efficient solution and representation of propositional problems (Davis-Putnam, 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ödel's 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).

Instruction

Lectures and problem solving sessions.

Assessment

Written examination at the end of the course combined with assignments given during the course.

If there are special reasons for doing so, an examiner may make an exception from the method of assessment indicated and allow a student to be assessed by another method. An example of special reasons might be a certificate regarding special pedagogical support from the disability coordinator of the university.