Institute for Computer Languages

Compilers and Languages Group

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.

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

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

The tutorial will be structured on the following topics:

**First-order theorem proving:**- The resolution and superposition calculus;
- Saturation algorithms;
- Redundancy elimination;
- Preprocessing and clause form transformation;
- Additional rules (splitting, definition introduction);

**Vampire:**- Basic principles of use;
- Implementation of the resolution and superposition calculus;
- Implementation of saturation;
- Options controlling proof search;
- Input and output syntax;

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