Mechanised Deduction
Dr Manfred Kerber  10 credit module Semester 2 
In the academic year 2001/02 the module takes place in G33, Aston Webb, Mondays 11:0012:00 and 17:0018: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, KnuthBendix procedure)  l4.ps.gz, l4.pdf 
ex4.ps.gz
ex4.pdf

5  
6  Higherorder treatment (higherorder resolution, higherorder 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
 
11  Student presentations 
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 11  input 
output 
1  Exercise 12  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.
Maintained by M.Kerber@cs.bham.ac.uk
School of Computer Science
The University of Birmingham
Last update 14 May 1999