Last Change: April 6, 2005
The Postscript version of this document.
The course starts on Wednesday, 3 Nov 15:15 in Seminar Room 5453 (close to my office), see also Section 3.1. For those of you who want to attend the intensive courses in period 2: I will schedule the lectures in such a way that this is possible.
Automated theorem proving (ATP) is a technology that tries to realize an old dream of mankind: to capture the essence of the human reasoning capability and to formalize it to such a degree that intelligent conclusions can be drawn by a machine. As such it is one of the core areas of the field of Artificial Intelligence and it started out already in the 1950s. The first decades of ATP research focused on mechanically proving mathematical theorems. Today the main interest lies in applications within computer science: theorem proving technology is being more and more used in analysis, verification, and synthesis of complex hard- and software.
ATP is a technical subject with a staggering number of theoretical and practical results. In a course like this one, only a small part of these can be traversed. Nevertheless, I believe that it is possible to convey in a quite compact manner the necessary background you need for finding the way on your own. This requires certain restrictions, most importantly, the restriction to classical propositional and first-order logic. In addition, the restriction to techniques that are actually being used in relevant systems. Techniques of mere historical interest are left out.
The timing of the course takes advantage of the recent publication of a state-of-the-art collection of overview articles [4]. Its chapters [1,3] cover the course contents. The Handbook of Automated Reasoning is very expensive and you don't need to buy it. Participants of the course will receive a copy of the relevant chapters.
The course is self-contained. It encompasses hands-on exercises with using and building theorem provers. There will also be a self-study component. If you want to brush up your knowledge on first-order logic before the course starts, then I recommend [2].
I plan to give 9 lectures. These will be accompanied by several practical and theoretical exercises. I cannot grade these, but we can discuss your solution.
As to the examination, I offer you a choice among two possibilities: either you take an oral exam or you prepare a lecture yourself. If you choose the latter, you can pick a chapter in [4] that interests you, and we'll agree on some parts of it for you to present. Some of these lectures will take place after the winter break.
All lectures take place in Seminar Room 5453 (close to my office). The morning lectures start at 10:15.
| Week | Wednesday | Thursday |
| 15:15 | 10:15 | |
| 45 | 3 Nov | 4 Nov |
| 46 | 10 Nov | 11 Nov |
| 49 | -- | 2 Dec in 6103! |
| 50 | 8 Dec | cancelled |
| 51 | 15 Dec | 16 Dec |
| 4 | 28 Jan (OBS: Friday 10:15) | |
The dates for the participants' lectures (45 minutes each) start in week 6, 2005.
First there is a series of 9 lectures done by myself. In the second part, some of you will give lectures (45 minutes each) on more specialized topics.
Propositional and first-order logic; substitution and unification; normal forms; Herbrand's Theorem. Equality.
Lecture on 3 Nov in PDF, ditto, 4 pages on 1
Lecture on 4 Nov in PDF, ditto, 4 pages on 1
Lecture on 10 Nov in PDF, ditto, 4 pages on 1
Solution to Exercise in PDF, ditto, 4 pages on 1
Lecture on 11 Nov in PDF, ditto, 4 pages on 1 (part 1)
Basic completeness proof. Lifting.
Lecture on 11 Nov in PDF, ditto, 4 pages on 1 (part 2)
Lecture on 2 Dec in PDF, ditto, 4 pages on 1 (part 1)
Lecture on 2 Dec in PDF, ditto, 4 pages on 1 (part 2)
Lecture on 8 Dec in PDF, ditto, 4 pages on 1 (part 1)
Lecture on 8 Dec in PDF, ditto, 4 pages on 1 (part 2)
Lecture on 15 Dec in PDF, ditto, 4 pages on 1
Connected tableaux; ordered tableaux; techniques for proving completeness.
Lecture on 8 Dec in PDF, ditto, 4 pages on 1
Factoring. Basic completeness proof. Lifting.
Lecture on 28 Jan in PDF, ditto, 4 pages on 1
Implementation issues. Redundancy criteria. Ordered Resolution with Selection. Set of Support.
The following lectures are given by course participants and guests in lp3/4, 2005:
| Name | Date | Reference | Topic |
| Fredrik Lindblad | 11 Feb | HBAR Ch. 16 | HO Unification |
| David Wahlstedt | 18 Feb | HBAR Ch. 15 | Type Theory |
| Hans Svensson | 25 Feb | HBAR Ch. 7 | Paramodulation |
| Harald Hammarström | 11 Mar | HBAR Ch. 13 | Automating Induction |
| Tobias Gedell | 15 Apr | [Giese PhD] | Constraint Tableaux |
| Ulf Norell | 15 Apr | HBAR Ch. 27 | Sorts |
| Daniel Hedin | 29 Apr | [Implementation] | Resolution Prover |
| Philipp Rümmer | 29 Apr | HBAR Ch. 14 | Inductionless Induction |
The lectures prepared by course participants will be integrated into the Formal Methods Meeting. They usually take place in the sektionsgemänsamma sammanträdesrum. There will be two lectures on each occasion. The dates are 11., 18, and 25. February, 11 March, 15 and 29 April 2005.
jTAP--A Tableau Prover in Java
Otter--A Resolution Theorem Prover. Here is the manual. The version that is installed at CS is outdated. The latest version can be run as ~reiner/bin/otter.
Handbook of Automated Reasoning (HBAR) [4]. Unfortunately, the HBAR is very expensive -- 300 Euro! I have a copy in my room, which you can borrow for a short while. If you need a specific chapter, contact me. Below are some parts you can print out, but please don't distribute the Postscript files to other people.
The Chapter on Resolution
The Chapter on Tableaux