Course acronym: FOTP
Course type: Lectures + Practical Discussions
Course credits: 7.5 points
Lecturers: Laura Kovács and Andrei Voronkov Target student audience:PhD students
Language of teaching: English
The course is organised blocked in LP4, in two different weeks between April-May 2016 as follows:
The course uses the Vampire theorem prover for demonstrations.
The Vampire binaries can be downloaded here: Vampire binaries.
|Event||Date and time||Room||Topic||Online material|
|Lecture 1||Tuesday, April 19, 9:00-10:30||EDIT 3364||Introduction
First-Order Logic and TPTP
|Lecture 2||Tuesday, April 19, 11:00-12:30||EDIT 3364||Inference Systems
|Lecture 3||Wednesday, April 20, 9:00-10:30||EDIT 3364||Redundancy Elimination||Slides|
|Lecture 4||Wednesday, April 20, 11:00-12:30||EDIT 3364||Equality|
|Lecture 5||Thursday, April 21, 13:00-14:30||EDIT 8103||Unification and Lifting||Slides|
|Lecture 6||Thursday, April 21, 14:30-16:00||EDIT 8103||From Theory to Practice|
|Lecture 7||Friday, April 22, 9:00-10:30||EDIT 3364||Splitting and AVATAR||Slides|
|Lecture 8||Friday, April 22, 11:00-12:30||EDIT 3364||Sorts
Student presentations will take place on May 2, 2016, in room EDIT 3364,
between 9:30-12:00 and 13:00-15:30.
Except one presentation (see below), each presentation will take 40 minutes, followed by up to 20 minutes questions.
Presentations should be split in two 20 minutes parts, each student presenting exactly one part.
Presentations should be self-contained, motivating and explaining the paper's contributions, with providing details on theoretical and experimental results.
|Paper: "Selecting the Selection"||Jonas Duregard
|Paper: "Playing with AVATAR"||
(20 minutes presentation + 10 minutes questions)
|Paper: "The Vampire and the FOOL"||Jonatan Kilhamn
|Paper: "Extensional Crisis and Proving Identity"||Simon Robillard
There is one exercise sheet containing problems to be solved using Vampire.
Students are asked to formulate these problems in first-order logic and TPTP, and solve them using Vampire.
Solutions should be based on individual work.
Solutions should be send via email to Laura Kovács, by May 3, 2016.
|Exercise||Handed out on||Due on|
|Exercise sheet||April 22||May 3, 6pm|
This course is designed for PhD students, but also open to anyone else interested.
If you are interested in this course, please register
to the course by sending an email to email@example.com.
Please register by March 15, 2016.
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:
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.
The course will cover the following topics (the list of topics may be slightly changed):
Lecture notes, that is slides, will be distributed online.
The lectures will be interleaved with discussions on practical aspects and heuristics for implementing first-order theorem provers.
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:
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.