You are here: Home Teaching Winter Term 2013/2014 Computer Supported Modeling and …

Computer Supported Modeling and Reasoning (Lecture)

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 formalized 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.
Course type Lecture
Instructors Jochen Hoenicke
Lecture Tuesday, 10:00–12:00 c.t., in building 51 room 03 026
Exercise Thursday, 10:00–12:00 c.t., in building 82 room 00 029
First session Lecture 22.10.12
Language of instruction English or German
Credits 6
Exams Wednesday, March 12, in building 52 room 00 017
Course Catalog Computer Supported Modeling and Reasoning



  • The slides, lecture notes, screen notes, and the first exercise sheet are online.  The documents will be updated throughout the course.  We will update these documents during this course.
  • For technical reasons the links between the slides, the lecture notes, and the screen notes do not work when viewing online.  Simply download them to the same folder and the links will work.
  • A new version of lambda.thy is available.  Now, CONV includes RED.


Admission criteria

You have achieve at least 50% of the points per exercise sheet.

Exercise Submission Scheme

Every Tuesday before the lecture.  Send Isabelle scripts to


Details of the exams will be published later.

Please register via examination office as usual.


Literature & Web resources

Slides and Additional Material