Teaching
Current lectures are on
my homepage .
-
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 .