Teaching

• Logic and Verification, SS 2008

  Logic and Verification .

• Programowanie Obiektowe (angielsku)

  Programowanie Obiektowe (angielsku) .

• 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 .