Teaching

• Programming in C++ (SS 2017)

  Programming in C++. You must attend lectures, be willing to use Linux. Solutions must be presented on Lab Computers.

• Introduction to Flightsimulation (WS 2016)

  Flight Simulation.

• Programowanie w C++ (SS 2016)

  Programowanie w C++.

• Theorem Proving (SS 2016)

  Theorem Proving.

• Compiler Construction (WS 2015)

  Compiler Construction.

• Programming in C++ (SS 2015)

  Programming in C++.

• Flight Simulation (WS 2014/2015)

  Flight Simulation.

• Programming in C++ (SS 2014)

  Programowanie w C++.

• Compiler Construction (WS 2013/2014)

  Compiler Construction.

• Theorem Proving (SS 2013)

  Theorem Proving.

• C++ laboratory (SS 2013)

  Laboratory C++.

• Introduction to Flight Simulation (WS 2012/2013)

  Introduction to Flight Simulation.

• C++ Laboratory (SS 2012)

  Laboratory C++ .

• Compiler Construction (WS 2011/2012)

  Compiler Construction.

• Object-Oriented Programming (SS 2011)

  Object-Oriented Programming (Programowanie Obiektowe). Polish students are very much welcome to register for this course, because I want to ensure equal level between courses for Polish and international students.

• Introduction to Flight Simulation (WS 2010/2011)

  Flight Simulation.

• Object Oriented Programming (SS 2010)

  Due to the level of the students, objects were not discussed. Only the absolute basics of programming were covered. Two out of six students were able to pass an exam that was of record-breaking easyness. Object-Oriented Programming .

• Compiler Construction (WS 2009/2010)

  Compiler Construction

• Programowanie Obiektowe (SS 2009)

  Programowanie Obiektowe (angielsku) .

• Logic and Verification (SS 2009)

  Logic and Verification .

• Licencjacki projekt programistycny

  All projects are completed.

• Introduction to Formal Logic, winter semester 2007

  Is here .

• Seminar Interactive Proof Systems, winter semester 2007

  We made ourselves acquainted with HOL light, and verified the unification algorithm. A detailed description is here .

• Some remarks about Python Exercises

  • Give meaningful names to functions and variables. (Not f1, f2, f3, v1, v2, v3)
  • Don't use continue and break. These are just goto's in disguise.
  • Avoid side effects on data structures.

• Introduction to Automated Reasoning, summer semester 2007

  The course has a new homepage .

• Introduction to Automated Reasoning, ESSLLI 2006

  Lectures notes for the ESSLLI course 'introduction to automated reasoning.' The course was held in Malaga from July 31st to August 4th, 2006 in cooperation with Marc Bezem.
  • Reader as ps or pdf .
  • Slides on propositional resolution, either as ps or pdf .
  • Slides on resolution for predicate logic (lifting theorems), either as ps or pdf .
  • Slides on superposition (rules for handling equality), either as ps or pdf .
  • Slides on the transformation from first-order logic to clause logic, either as ps , or pdf .
  • Slides on propositional SAT-solving, either ppt or pdf .
  • Slides on coherent logic (CL), either as ppt or pdf .

• Introduction to Proof Theory, winter semester 2005

  Course was tought together with Ruzica Piskac. She now works at Ecole Polytechnique Federale de Lausanne. This is her present homepage.

• Lecture on Interactive Proof Tools (PVS and COQ) 2003

  Schedule, slides and exercises . Current homepage of Patrick Maier .

• Lecture on Interactive Proof Tools 2001

  Schedule, slides and exercises (somewhat incomplete).

• Introductory Course on Resolution Based Theorem Proving 1998

  The course was given in winter semester 1998-1999 in Amsterdam. The lectore notes below do not introduce resolution itself. (This was done by Kees Doets) The lecture notes refinements of resolution and equality rules, like paramodulation, demodulation, superposition. Here are the notes on refinements as ps or pdf , and here are the notes on equality as either ps or pdf .