Applied Logic
Syllabus, Master's level, 1MA058
This course has been discontinued.
- 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, 15 March 2007
- Responsible department
- Department of Mathematics
Entry requirements
BSc, Logic and Proof Techniques I, Automata Theory
Learning outcomes
In order to pass the course (grade 3) the student should be able to
Higher grades, 4 or 5, require a higher level of proficiency. The student should be able to solve problems of greater complexity, i.e. problems requiring a combination of ideas and methods for their solution, and be able to give a more detailed account of the proofs of important theorems and by examples and counter-examples be able to motivate the scope of various results. Requirements concerning the student's ability to present mathematical arguments and reasoning are greater.
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.