1. Outline
2. Target audience
3. Implementation
4. Contents
5. Literature


MAT-60556 in the Course Catalog

MAT-60556 Mathematical Logic

Updated: 2014-08-28

Course outline. Changes possible. Edit 11.9.: Slides 1 and 2 updated slightly. More to follow...

1. Outline

The course is an introductory course on mathematical logic, with a slightly computer science-leaning content. The goal is to provide a basis of formal logics, especially propositional and first-order logics, and some idea of modal logics. The student should gain some understanding formal proof systems and automated reasoning. Relation to computability with applications such as formal verification and model checking are discussed.

2. Target audience

The course is meant for nth year undergraduate and graduate students of XXXX.

Prerequisites only include MAT-02650 (algorithm mathematics) as mandatory. It is recommended that some more mathematical maturity is gained from other mathematics courses. Programming experience is also helpful, though by no means not required.

3. Implementation

Lectures are given on periods 1 and 2, i.e., the fall semester. Weekly schedule includes 4 h of lectures and 2 h exercises.

The course will consist of exercise assignments and exam. Grading is based on the exam.

There will be lecture slides, which will partially be given on this web page. Exercise assignments will also be given here.

Lecture Slides

  1. First part Download PDF
  2. Second part Download
  3. Third part Download PDF
  4. Fourth part Download PDF
  5. NOTE: In 2014 we skip temporal logic. Therefore, the next set of slides relevant for the course is the seventh!

    Fifth part (temporal logic) Download

  6. (sixth part has nothing new)
  7. Seventh part: Boolean Algebras Download
  8. Eight part: Model Theory Download
  9. Ninth part: Recursion theory Download
  10. Tenth part: Limitative results Download

Exercises

  1. Exercise 1, 3.9. Download PDF
  2. Exercise 2, 10.9. Download PDF
  3. Exercise 3, 17.9. Download PDF
  4. Exercise 4, 24.9. Download PDF
  5. Exercise 5, 1.10. Download PDF
  6. Exercise 6, 8.10. Download PDF
  7. Exercise 7, 22.10. Download PDF
  8. Exercise 8, 29.10. Download PDF
  9. Exercise 9, 05.11. Download PDF
  10. Exercise 10, 12.11. Download PDF
  11. Exercise 11, 19.11. Download PDF
  12. Exercise 12, 28.11. Download PDF

The course lectures and exercises will be based on the book: Mathematical Logic for Computer Science, by Mordechai Ben-Ari (3rd edition, Springer 2012). Those wishing to pass the course by self-study, should obtain the book by some means.

Course teacher in charge is Henri Hansen.

4. Contents

Note that the following topics are not listed on a one topic per lecture - basis.

1. Introduction

Origins and history of Logic, Propositional Logic, First order logic, modal and temporal logic, Program Verification

2. Propositional logic 1

Formulas, interpretations, equivalences, operators.

3. Propositional logic 2

Satisfiability, validity, consequence, tableaux, soundness, completeness

4. Propositional logic 3

Deductive systems, resolution, Binary decision diagrams, SAT solvers

5. First order Logic 1

Sets, Relations, predicates, formulas, interpretations

6. First order logic 2

Equivalences, tableaux, soundness, completeness.

7. First order logic 3

Deductive systems, terms and normal forms, resolution, logic programming

8. First order logic and Model Theory

Undecidability, decidable cases, finite and infinite models, complete and incomplete theories

9. Temporal logic (Not in 2014)

LTL (always/eventually), LTL models, validity, satisfiability, model checking

10. Verification (Not in 2014)

Correctness formulas, formal specification, formal semantics, programs as automata, model checking safety and liveness, branching time, symbolic model checking

Auxiliary topics

5. Literature and other material