Updated: 2014-08-28

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

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.

The course is meant for *n*^{th} 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.

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 **

- First part Download PDF
- Second part Download
- Third part Download PDF
- Fourth part Download PDF
- 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

- (sixth part has nothing new)
- Seventh part: Boolean Algebras Download
- Eight part: Model Theory Download
- Ninth part: Recursion theory Download
- Tenth part: Limitative results Download

** Exercises **

- Exercise 1, 3.9. Download PDF
- Exercise 2, 10.9. Download PDF
- Exercise 3, 17.9. Download PDF
- Exercise 4, 24.9. Download PDF
- Exercise 5, 1.10. Download PDF
- Exercise 6, 8.10. Download PDF
- Exercise 7, 22.10. Download PDF
- Exercise 8, 29.10. Download PDF
- Exercise 9, 05.11. Download PDF
- Exercise 10, 12.11. Download PDF
- Exercise 11, 19.11. Download PDF
- 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.

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

Formulas, interpretations, equivalences, operators.

Satisfiability, validity, consequence, tableaux, soundness, completeness

Deductive systems, resolution, Binary decision diagrams, SAT solvers

Sets, Relations, predicates, formulas, interpretations

Equivalences, tableaux, soundness, completeness.

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

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

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

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

- Set theory: Finite and infinite sets, operators, relations, functions, cardinality, axiom of choice, continuum hypothesis
- Satisfiability Modulo Theories (SMT): Tools, applications to model checking
- Higher order logics: Fixed points in logic, second order logics

- M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed),
Springer.
**course textbook**, chapters 1-12. - J. Bell and M. Machover: A Course in Mathematical Logic,
Elsevier.
**course textbook**Chapters 4-7. (Chapters 1--3 also valid, though they cover the same issues as the first book) - I. Bratko: Prolog Programming for Artificial Intelligence (4th ed), Addison Wesley. Recommended for those who wish to learn logic programming for games etc.
- a proof of the church theorem
- a proof of the compactness theorem
- a proof scetch Tarski theorem
- a proof of the (simplified downward) Löwenheim-Skolem theorem
- Last year's exam 1, with some answers
- Last year's exam 2 with some answers
- Last year's exam 3