Aims

• To introduce the basic concepts and terminology of mechanised deduction
• To present the main approaches to automated, machine-oriented, human-oriented, and interactive mechanised deduction.
• To present the strengths and limitations of the different approaches
• Enable the students to read up-to-date research papers in the field

Objectives

• know the main approaches in mechanised deduction
• be able to understand and to discuss the advantages and limitations of the approaches
• be able to apply the different approaches to unseen examples
• be able to see the relationship of approaches to mechanised deduction and of human theorem proving.
• be able to read, understand, and present a recent research paper of the field.

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

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