Teaching
These are the lectures that I taught in Wrocław:

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.

ObjectOriented Programming (SS 2011)
ObjectOriented 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 recordbreaking easyness.
ObjectOriented 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 firstorder logic to
clause logic, either as
ps , or
pdf .

Slides on propositional SATsolving, 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 19981999 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 .