Spezialvorlesung: Computer-Supported Modeling and Reasoning WS03/04

Organizer:	Dr. Jan-Georg Smaus (lecture + exercises)
Classes:	Wed 9-11 in Gebäude 52, SR 02-017
Exercises:	Fri 9-11 in Gebäude 52, SR 00-005
Credit points:	6
Exam:	Students who actively participate in the course and exercises will get a "benoteten Schein".
Language:	English
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.

This Spezialvorlesung (2+2) aims at teaching new ways of thinking about program development and program analysis, as well as providing practical experience in formal computer-supported verification.

The lecture consists of two parts. In part 1, we shall introduce the foundations of logic reasoning and their implementation in the modern proof system Isabelle. The accompanying practical exercises will be from the fields of logic, (naïve) set theory and discrete mathematics.

In part 2 we shall study the consistent construction of mathematical theories on a large scale, the representation (embedding) of programming languages in logic and verification of programs or program refinements.

The course is now finished (February 2004) and this page will no longer be maintained. A pointer to an up-to-date version of the course material will be given on my homepage.

Comments? Send an email to J.-G. Smaus.