Instructors |
Luís Cruz-Filipe
< lcf [at] imada.sdu.dk > Marco Peressotti < peressotti [at] imada.sdu.dk > |
---|---|

Period | Spring 2020 |

Code | DM846 (10ECTS, Master level, https://odin.sdu.dk/sitecore/index.php?a=searchfagbesk&internkode=dm846&lang=en) |

Office hours | Open door (or by Appointment). |

Prerequisites | The student is expected to have basic understanding of mathematical proofs and to be familiar with the basics of propositional logic and predicate calculus, obtainable e.g. by having followed DM535 (Discrete Methods for Computer Science) or MM537 (Introduction to Mathematical Methods). |

The aim of this course is to provide students with a background on logic focusing on aspects most relevant to computer science.

At the end of this course, the student is expected to have the following competences:

- understand the theoretical concepts of soundness, completeness, and decidability;
- prove soundness of particular logics;
- choose the logic framework most suited for particular computer science applications;
- be able to use existing tools for reasoning within particular logics.

- Deductive systems for propositional logic.
- First order logic and subsets thereof, combinatorial logic and type theory.
- Curry-Howard isomorphism.
- Modal and temporal logic.
- Formal specification and validation.
- Pi-calculus, tools for logic reasoning