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:

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



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

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.

Laura Kovács
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2015-02-20 (Webmaster)