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 AprilMay 2016 as follows:
Binaries:
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:0010:30  EDIT 3364  Introduction FirstOrder Logic and TPTP 
Slides 
Lecture 2  Tuesday, April 19, 11:0012:30  EDIT 3364  Inference Systems Selection Functions Saturation Algorithms 

Lecture 3  Wednesday, April 20, 9:0010:30  EDIT 3364  Redundancy Elimination  Slides 
Lecture 4  Wednesday, April 20, 11:0012:30  EDIT 3364  Equality  
Lecture 5  Thursday, April 21, 13:0014:30  EDIT 8103  Unification and Lifting  Slides 
Lecture 6  Thursday, April 21, 14:3016:00  EDIT 8103  From Theory to Practice  
Lecture 7  Friday, April 22, 9:0010:30  EDIT 3364  Splitting and AVATAR  Slides 
Lecture 8  Friday, April 22, 11:0012:30  EDIT 3364  Sorts Satisfiability Cookies 
Slides 
Student presentations will take place on May 2, 2016, in room EDIT 3364,
between 9:3012:00 and 13:0015: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 selfcontained, motivating and explaining the paper's contributions,
with providing details on theoretical and experimental results.
Paper  Students 
Paper: "Selecting the Selection"  Jonas Duregard Markus Aronsson 
Paper: "Playing with AVATAR" 
Evgenii Kotelnikov (20 minutes presentation + 10 minutes questions) 
Paper: "The Vampire and the FOOL"  Jonatan Kilhamn Fabian Ruch 
Paper: "Extensional Crisis and Proving Identity"  Simon Robillard Nikita Frolov 
There is one exercise sheet containing problems to be solved using Vampire.
Students are asked to formulate these problems in firstorder 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 laura.kovacs@chalmers.se.
Please register by March 15, 2016.
Firstorder 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 firstorder 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 firstorder theorem provers.
At the end of the first week of the course, reading material on firstorder 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.