Computer-Supported Modeling and Reasoning - Overview
Lecturer and Exercises: Prof. Dr. Jan-Georg Smaus
Time and Location
Lecture: Wednesday 9-11, room SR 00-010/14, building 101
Exercises: Friday 9-11, room SR 00-005, building 52
Language
The lecture will be given in English. Questions may be asked/exercises may be done in German.
Contents
This lecture 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 lecture 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 lecture 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 lecture.
Exam and Exercises
Students who actively participate in the course and exercises will get a "benoteten Schein".