Computational Logic: Description of the Courses
This information is preliminary and subject to change.
Advanced Topics in Term Rewriting
Description
After a quick review of the basics of term rewriting, we study a few of the following important topics in more detail:
- completion
- conditional rewriting
- graph rewriting
- termination
- modularity
- tree automata techniques
- unification theory
Computability Theory
Description
This course provides an introduction to recursive function theory and lambda calculus, two important computational models. We show that the two models, although very different, have the same expressive power and we relate them to Turing machines.
Verification using Model Checking
Description
Model checking is a computationally intensive but thorough technique for verification. The aim of this course is to learn how to perform simple model checking tasks. The course will be split into the following three blocks.
- Timed Model Checking: useful for analysing systems in which the exact timing of events is critical to the correctness. As an example of a real time model checker, we intend to use Uppaal.
- Explicit State Model Checking: best when used for verifying asymmetric and/or highly restricted systems such as communication protocols. As an example of an explicit state model checker, we intend to use Spin.
- Symbolic Model Checking: the best way to verify highly symmetric systems with a large degree of freedom such as hardware (microprocessors). As an example of a symbolic model checker, we intend to use NuSMV.
Automated Theorem Proving (in Isabelle/HOL)
Description
The course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade provers, teaches the theoretical backround to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The course is intended to bring master students into contact with current research topics in the field of theorem proving and automated deduction, and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification.
The theorem prover Isabelle/HOL will be used in the course. Topics include higher-order logic, natural deduction, lambda calculus, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs and proofs about programs.
Modal and Temporal Logics
Description
Modal logic is an extension of ordinary, classical logic which allows formalizations of phrases such as "it is possible that" and "it is necessarily true that". Although the beginnings of modal logics lie within philosophy and linguistics, modal logics have now become an exciting way to assess computational processes. In particular temporal logics have received much attention as they allow the modelling of "true in the next step", and "true forever". Thus while and repeat-until loops can be nicely formalized. The course will provide an easy introduction to the basic systems of modal logic and temporal logics, both propositional and predicate, their semantics and their applications.
Requirements
Knowledge of (classical, first-order) logic is assumed.
Process Algebra
Description
Automated and semi-automated manipulation of so-called labelled transitions systems has become an important means in discovering flaws in software and hardware systems. Process algebra has been developed to express such labelled transitions systems algebraically, which enhances the ways of manipulation by means of equational logic and term rewriting.
Programming in OCAML
Description
How to write maintainable and reliable programs? One of the answers is to adopt a functional programming style which emphasizes the use of (recursive) functions. Because side-effects like assignment are banned, code written in a functional programming language is often simple and elegant. The course provides an introduction to Objective CAML (OCAML), a modern functional programming language with object-oriented features. More advanced topics like abstract data types and unit tests that support large scale programming are also discussed.
Computational Logic 1 - 4
The content of these seminars depend on the current research interests of the members of the Computational Logic group. Some of the assigned topics prepare for a master project.