# Syllabus for Applied Logic

10.0 credits

## Syllabus

• Course Code: 1MA058
• Education Cycle: Second cycle
• Main Field(s) of Study and In-Depth Level: Computer Science A1N Mathematics A1N
• Grading System: Fail (U), 3, 4, 5.
• Established: 2007-03-15
• Established by: Teknisk-naturvetenskapliga fakultetsnämnden
• Syllabus Applies from: week 44, 2008
• 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).

#### Instructions

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.

• ## Reading List

Applies from: week 36, 2010

• Huth, Michael Ryan, Mark Logic in computer science : modelling and reasoning about systems 2. ed.

Cambridge : Cambridge Univ. Press, 2004 - xiv, 427 s.

ISBN: 0-521-54310-X LIBRIS-ID: 9359296

Library Catalogue

Syllabus Revisions