Uni-Logo

Diese Seite ist nur auf Englisch verfügbar.

Computer-Supported Modeling and Reasoning - Overview

Lecturer and Exercises: Prof. Dr. Jan-Georg Smaus

Time and Location

Lecture: Wednesday 14:15-16:00, room SR 01-016, building 101. Start: October 25th
Exercises: Friday 9:00-10:45, room SR 00-029, building 82

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 system (e.g., program or chip) development and analysis. The system behavior and desired system properties can both be formalised using logic, for the purpose of verifying the properties using computer support.

The lecture is intended for anyone interested in artificial intelligence (KI), logic, hardware and software verification.

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 for Diplom and Bachelor students in their 5th to 8th semester, and Master students in their 1st to 3rd semester.

Some basic knowledge of logic will be of great use for successful participation in this lecture.

Exam and Exercises

The course is worth six credit points. In order to obtain a "benoteten Schein" or credit points (as applicable), participants are required to pass a written or oral exam at the end of the semester, and to participate actively in the course and exercises.