forked from vprover/vprover.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
history.html
64 lines (64 loc) · 4.52 KB
/
history.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
<!DOCTYPE html
PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en-US" xml:lang="en-US">
<head>
<title>History</title>
<link href="vampire.css" rel="StyleSheet" type="text/css" />
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
</head>
<body>
<table style="border-collapse:collapse"><tr>
<script src="scripts/nav.js"></script>
<td class="content"><style>#authors {border-collapse:collapse;
float:right;
empty-cells:show;
margin:0pt;border:0pt;padding:0pt}
#authors td {border:0px;
padding: 0pt;
margin:0px}
#authors img {width:15em}
#geometry {border-collapse:collapse;
empty-cells:show;
margin:0pt 0.7em 0pt 0.7em;
border:0pt;padding:0pt}
#geometry td {margin:0px;
padding: 0pt;
text-align: center;
border:1px solid #555555;
height:9em;
width:7em}</style><table id="authors"><tr><td><img alt="Andrei Voronkov" src="img/voronkov.jpg" style="width:13.04em" /></td> <td><img alt="Alexandre Riazanov" src="img/riazanov.jpg" style="width:13.16em" /></td></tr> <tr><td style="text-align:center"></td> <td><img alt="Krystof Hoder" src="img/hoder.jpg" style="width:13.16em" /></td></tr></table> <h1>History</h1>
<p>Vampire had several predecessors implemented by <a href="http://www.voronkov.com/">Andrei Voronkov</a> 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.</p> <p>There have been three major incarnations of Vampire itself, all
implemented in C++.</p> <ol><li>The first incarnation was born in Uppsala University
in 1994 after <a href="http://www.voronkov.com/">Andrei Voronkov</a>'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.</li> <li>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 <a href="http://www.voronkov.com/">Andrei Voronkov</a>
and <a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a> in 1998.
From 2005 it has been developed and maintained by <a href="http://www.voronkov.com/">Andrei Voronkov</a>.
This incarnation was winning the CASC competitions since
1999.</li> <li>The work on third re-incarnation of Vampire
started in 2008. It has been developed by <a href="http://www.voronkov.com/">Andrei Voronkov</a> and
<a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>. 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 reincarnations
glued by Perl scripts called Dracula and Drakosha.</li> <li>Since <a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a> decided to leave academia and help <a href="https://plus.google.com/+LarryPage/posts">Larry Page</a> and <a href="https://plus.google.com/+SergeyBrin/posts">Sergey Brin</a> to
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 <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, mainly in Vampire's
program analysis, interpolation and symbol elimination
parts. </li></ol>
From 2014, the <a href="team.html">Current Team</a> 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 Krystof Hoder in the third incarnation.
</td></tr></table>
</body>
</html>