First-Order Theorem Proving and Vampire (Period 4, 2015/2016)

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


Course Schedule and Organisation

The course is organised blocked in LP4, in two different weeks between April-May 2016 as follows:

Binaries:
The course uses the Vampire theorem prover for demonstrations.
The Vampire binaries can be downloaded here: Vampire binaries.

Course Calendar for Lectures

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
Slides
Lecture 2 Tuesday, April 19, 11:00-12:30 EDIT 3364 Inference Systems
Selection Functions
Saturation Algorithms
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
Satisfiability
Cookies
Slides

Paper Assignment for Student Presentations:

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

Exercise Sheet

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



Course Registration

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.

Course Information

Summary:

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.

Prerequisites:

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.

Course topics (tentative):

The course will cover the following topics (the list of topics may be slightly changed):

Lecture notes:

Lecture notes, that is slides, will be distributed online.

Practical discussions:

The lectures will be interleaved with discussions on practical aspects and heuristics for implementing first-order theorem provers.

Student presentations:

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.

Grading and examination:

The course examination will be based on:

We will use 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.