On this page you find material for the course Computer-Supported Modeling and Reasoning, which has been presented as a lecture at Albert-Ludwigs-Universität Freiburg in WS01/02, WS02/03, WS03/04, WS04/05, WS05/06, WS06/07, and WS07/08. The material is based on work by Prof. Dr. David Basin, PD Dr. Jan-Georg Smaus, and Dr. Burkhart Wolff. It is currently maintained by PD Dr. Jan-Georg Smaus.
Description
This course is about using logic for program development and program analysis. Programming languages and desired program properties can both be formalised using logic, for the purpose of verifying the properties using computer support.
The course is roughly structured in four parts. In part 1, we shall introduce various logic systems including propositional logic, first-order logic, and (naive) set theory. We shall see how proofs in these systems can be conducted both using paper and pencil and using the interactive theorem prover Isabelle. In part 2, we shall attempt to understand what happens behind the scenes: we shall study meta-logic, which is the general theory allowing us to implement all kinds of logic systems using a single tool. In part 3, we shall see how an important part of mathematics and programming languages can be modeled in this framework, including concepts such as arithmetic, data-types, and recursion. Part 4 will be a case study coming from functional or imperative programming or from the area of specification languages.
Prerequisites
The course is intended both for students of Artificial Intelligence (KI) interested in computer-supported deduction-based problem solving, and students interested in computer based system modeling and program verification.
Some basic knowledge of logic will be of great use for successful participation in this course.
Formats of the Material
Currently, slides are available. These have been enriched with annotations (reachable via hyperlinks) so that they are suitable both as lecture slides for lecturers who want to give a similar course, and as online course for students who want to study on their own. For a lecture, one should count roughly 16 units of 90 minutes of lectures and the same amount of time for exercises.
The slides are not suitable for printout. For printout, lecture notes are available. Here the annotations are rendered as footnotes and using references. We advise to print four pages per sheet.
For studying the material on a computer screen, screen notes are available. Here the annotations are rendered as footnotes and using hyperlinks.
The material is in English.
We refer to the lecture webpages of WS05/06, WS06/07, and WS07/08 for more material.
