First-order theorem proving is one of the earliest research areas in artificial intelligence and formal methods. It has applications in program analysis and verification, semantic Web, database systems, and many other areas.
This course has the following objectives:
- to introduce first-order theorem proving using the resolution and superposition calculus;
- to show how this calculus can be efficiently implemented;
- to explain how one can use the first-order theorem prover Vampire for theorem proving and other applications.
We will discuss the resolution and superposition calculus, introduce saturation algorithms, present various algorithms implementing inferences, redundancy elimination, preprocessing and clause form transformation, and explain how these concepts are implemented in Vampire.
The second part of the course will cover more advanced topics and features. Some of these features are implemented only in Vampire. This includes reasoning with theories, such as arithmetic, answering queries to very large knowledge bases, interpolation, and symbol elimination.
All the introduced concepts will be illustrated by running Vampire.
The course is recommended for PhD students in Computer Science. Students are expected to be familiar with first-order logic. The course does not assume a priori knowledge in theorem proving.
At the end of the first week of the course, reading material on first-order theorem proving will be distributed. Students will be asked to choose one topic and present it in detail in the last week of the course.
The course examination will be based on the student presentations, using the pass/failed grading system. Student presentations need to get into the technical detail of the chosen article on theorem proving. The presentations should also relate the chosen topic to the course material, explaining what improvements and/or limitations the chosen topic imposes on theorem proving. Examples should be described and presented using Vampire.
A passing grade will be recommended only for student presentations addressing the above requirements.