Mechanised Reasoning

Dr Manfred Kerber

Course in the Midlands Graduate School in Theoretical Computer Science, November/December 1999

Aims

Objectives

On completion of this course, the student should:

Prerequisites

Good knowledge of logic

Teaching Methods

The course will be presented in 6 lectures of 90 minutes and complemented by exercises.

Assessment

Students who attended the course can ask for an oral exam.

Recommended Books:

There is a multitude of literature on this topic, some more literature will be mentioned during the course. The literature will mostly consist of parts of different books and research papers, since no book exactly covers the full content of the course.

Title Author(s) Publisher Comments
Principles of Automated Theorem Proving David Duffy John Wiley & Sons 1991 Further Reading
Symbolic Logic and Mechanical Theorem Proving Chin-Liang Chang and Richard Char-Tung Lee Academic Press 1973 Further Reading
First-Order Logic and Automated Theorem Proving Melvin Fitting Springer-Verlag 1990 Further Reading


Detailed Syllabus and Relevant Links

The following courses are currently planned, modifications are possible. Slides and Exercises will be made available after the corresponding lectures as gzipped PostScript and as pdf files.

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 e1.ps.gz; e1.pdf
2 Resolution calculus (unification, clause normal form, skolemisation l2.ps.gz; l2.pdf e2.ps.gz; e2.pdf
3 Extensions to resolution (restriction strategies, selection strategies, sorts) l3.ps.gz; l3.pdf e3.ps.gz; e3.pdf
4 Equality handling (paramodulation, Knuth-Bendix procedure) l4.ps.gz; l4.pdf e4.ps.gz; e4.pdf
5 Higher-order treatment, Inductive theorem proving l5.ps.gz; l5.pdf e5.ps.gz; e5.pdf
6 Interactive theorem proving, Proof planning (natural deduction, tactics, tacticals) l6.ps.gz; l6.pdf e6.ps.gz; e6.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-1a input output
1 Exercise 1-1b input output
1 Exercise 1-2 input no proof found in reasonable time
2 Exercise 2-3a input output
2 Exercise 2-3b input output



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

Last update 8.11.1999