Mechanised Reasoning

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

- 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

- 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.

Good knowledge of logic

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

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

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