Applied Logic

10 credits

Syllabus, Master's level, 1MA058

This course has been discontinued.

A revised version of the syllabus is available.

Code: 1MA058
Education cycle: Second cycle
Main field(s) of study and in-depth level: Computer Science A1N, Mathematics A1N
Grading system: Fail (U), Pass (3), Pass with credit (4), Pass with distinction (5)
Finalised by: The Faculty Board of Science and Technology, 3 November 2008
Responsible department: Department of Mathematics

Entry requirements

120 credit points including Logic and Proof Techniques I, Automata Theory

Learning outcomes

In order to pass the course (grade 3) the student should

be acquainted with the undecidability of predicate logic (Church's theorem);

be acquainted with the completeness theorem of propositional and predicate logic and their use;

be acquainted with and have skills in using methods for efficient representation and solution of problems in propositional logic;

have skills in formalizing problems in modal, propositional and predicate logic;

be acquainted with different interpretations of modal operators and applications to model checking problems;

have skills in model-theoretic reasoning in predicate and modal logic;

be acquainted with calculi and systems for automatic proof search in predicate logic;

be acquainted with decision methods for equational logic;

be able to use a proof support system based on a logical framework;

understand 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 and, possibly, oral examination at the end of the course. Moreover, compulsory assignments may be given during the course.