Mechanised Deduction

Dr Manfred Kerber

10 credit module Semester 2


Detailed Syllabus and Relevant Links

In the academic year 2001/02 the module takes place in G33, Aston Webb, Mondays 11:00-12:00 and 17:00-18:00.

The following lectures are currently planned, modifications are possible. Slides and Exercises are available in gzipped PostScript files, during the module, spare copies can be found in the School's library, these should be taken first in order not to waste printer resources. The files will be made readable after the corresponding lectures. You can directly preview and print the files (locally) by something like:
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Deduction/ex2.ps.gz | ghostview -
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Deduction/ex2.ps.gz | lpr -
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Deduction/l2.ps.gz | ghostview -seascape -
zcat /bham/ftp/pub/authors/M.Kerber/Teaching/Deduction/l2.ps.gz | psnup -r -4 | lpr -

Week Content Slides Exercises
1 Introduction to mechanised deduction, different goals and approaches, examples program verification (Hoare calculus) and planning (situation calculus) l1.ps.gz, l1.pdf ex1.ps.gz ex1.pdf
2 Resolution calculus (unification, clause normal form, skolemisation l2.ps.gz, l2.pdf ex2.ps.gz ex2.pdf
3 Extensions to resolution (restriction strategies, selection strategies, sorts) l3.ps.gz, l3.pdf ex3.ps.gz ex3.pdf
4 Equality handling (paramodulation, Knuth-Bendix procedure) l4.ps.gz, l4.pdf ex4.ps.gz ex4.pdf
5
6 Higher-order treatment (higher-order resolution, higher-order unification) l5.ps.gz, l5.pdf ex5.ps.gz ex5.pdf
7 Interactive theorem proving (natural deduction, tactics, tacticals) l6.ps.gz, l6.pdf ex6.ps.gz ex6.pdf
8 Inductive theorem proving (classical approaches, rippling) l7.ps.gz, l7.pdf ex7.ps.gz ex7.pdf
9 Proof planning l8.ps.gz, l8.pdf ex8.ps.gz ex8.pdf
10 Application, Revision  ex9.ps.gz ex9.pdf
11Student presentations 


A pointer to the 1999 exam can be found here as ps.gz pdf.

Here are some links to input and output files of proofs generated with the Otter resolution theorem prover:

Worksheet Exercise input file output file
1 Exercise 1-1 input output
1 Exercise 1-2 input output
1 Exercise 2 input no proof found in reasonable time
2 Exercise 3 a input output
2 Exercise 3 b input output


In the second part of the module participants of the course will give presentations of research papers from the following list in topics.ps.gz, topics.pdf.
A schedule for the student talks will be made available here.
The criteria for assessing the presentations can be found here.


button bar


Maintained by M.Kerber@cs.bham.ac.uk
School of Computer Science
The University of Birmingham

Last update 14 May 1999