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 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.
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.
Fifth part (temporal logic) Download
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