Institute for Computer Languages
Compilers and Languages Group

First-order theorem proving and Vampire

August 1, 2011, Wroclaw, Poland
CADE 2011 Tutorial

---

The tutorial serves the following purposes:

• to give an overview of first-order theorem proving using the resolution and superposition calculus;
• to show how this calculus and its modifications are implemented in Vampire;
• to explain the new features of Vampire.

This tutorial will be co-located with CADE 2011, Wroclaw, Poland.

Organisers

• Kryštof Hoder (The University of Manchester)
• Laura Kovács (Vienna University of Technology)
• Andrei Voronkov (The University of Manchester)

Schedule

The tutorial be of 1/2 day and will take place on August 1, 2011. It will comprise of three sessions, as follows:

• Session 1, 9:00-11:00 (A. Voronkov): First-order theorem proving and Vampire.
  Slides and examples
  
• Session 2, 11:00-11:45 (K. Hoder): Vampire usage and demo.
  Slides and examples
  
• Session 3, 11:45-12:30 (L. Kovács): New features and applications of Vampire.
  Slides and examples
  

Tutorial Topics

The tutorial will be structured on the following topics:

1. First-order theorem proving:
   • The resolution and superposition calculus;
   • Saturation algorithms;
   • Redundancy elimination;
   • Preprocessing and clause form transformation;
   • Additional rules (splitting, definition introduction);
2. Vampire:
   • Basic principles of use;
   • Implementation of the resolution and superposition calculus;
   • Implementation of saturation;
   • Options controlling proof search;
   • Input and output syntax;
3. Advanced modes and features of Vampire:
   • Working with very large knowledge bases;
   • Interpreted values and theories;
   • Consequence removal;
   • Colored proofs;
   • Interpolation;
   • Symbol Elimination;
   • Invariant generation and program analysis;
   • Multiple strategies and use of multi-core architectures.