Skip to content

History

Jump to bottom
Michael Rawson edited this page Mar 14, 2024 · 6 revisions

Editor's note: the following copy was originally written by Andrei (?) and survived a few copyings around. I've lightly edited it to bring it up to date, leaving the spirit of the original intact as far as possible!

-- Michael

Vampire had several predecessors implemented by Andrei Voronkov in the International Laboratory of Intelligent Systems in Novosibirsk from 1990. The first predecessor that was actually able to prove something appeared in 1989 and called Drakosha. It has been implemented in LISP.

Andrei Voronkov

Voronkov, just a few years ago

There have been four major incarnations of Vampire itself, all implemented in C++.

  1. The first incarnation was born in Uppsala University in 1994 after Voronkov's visit to the Bull Research Lab. This implementation was used for the first experiments with code trees and a pre-CASC competition with the SETHEO theorem prover in Munich.
  2. The second re-incarnation appeared in Uppsala University and then wandered to the University of Manchester. It has been developed from the first incarnation (that was eventually completely rewritten) by Voronkov and Alexandre Riazanov in 1998. From 2005 it has been developed and maintained by Voronkov. This incarnation has been winning the CASC competitions since 1999.
  3. The work on the third re-incarnation of Vampire started in 2008. It has been developed by Voronkov and Kryštof Hoder. This version used some code and algorithms for preprocessing from the second re-incarnation but re-implemented the resolution and superposition engine from scratch. The version used in CASC 2009 was actually a combination of the second and the third reincarnation glued by Perl scripts called Dracula and Drakosha.
  4. Since Hoder decided to leave academia and help Larry Page and Sergey Brin make more money, Vampire is waking up for its fourth reincarnation. Several people are working on it. A considerable amount of code was contributed by Laura Kovács, mainly in Vampire's program analysis, interpolation and symbol elimination parts. From 2014, the current team took over the active development of Vampire. Whilst the current version is labelled as the fourth reincarnation, much of the core still consists of code written by Hoder in the third incarnation.

Alexandre Riazanov Kryštof Hoder

Riazanov, Hoder

Since then, it has been a tale of two cities, Manchester and Vienna, but perhaps also the best and worst of times for Vampire. New heights of reasoning performance, capabilities and applications have been reached, including

  • improvements to the core superposition calculus
  • a finite model builder
  • higher-order reasoning
  • inductive reasoning
  • reasoning with theories
  • question answering
  • program synthesis
  • many applications of SAT and SMT solving
  • a slow ingress of machine learning
  • ever more aggressive use of portfolio modes

all while maintaining Vampire's dominance in CASC.

However, a significant amount of technical debt built up, which hampered Vampire's progress. Happily, modernisation efforts are paying off and this Vampire is accelerating into the future...

Clone this wiki locally