forked from vprover/vprover.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
trophies.html
30 lines (30 loc) · 3.25 KB
/
trophies.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
<!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>Our Trophies</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>#ttable {border-collapse:collapse;
empty-cells:show;
margin: 10pt 0pt 10pt 120pt;}
#ttable td {border:solid #c4d8ff 2px;
padding: 0px 5px 0px 5px;
text-align: center}</style><div style="float:right;padding:0pt 0pt 5pt 0pt"><img src="trophies.jpg" /></div> <h1>Our Trophies</h1> <p>Vampire is winning at least one division of the world cup in theorem
proving <a href="http://www.cs.miami.edu/~tptp/CASC/">CASC</a> since 1999. All together Vampire won 30 titles: more than any other
prover.</p> <p>We traditionally take part in the following two divisions
of the competition:</p> <ol><li>The FOF division: unrestricted first-order problems. This
division was ranked second in importance after the MIX
division before 2007 and is now recognised as the main
competition division.</li> <li>The CNF division: first-order problems in conjunctive normal
form. This division was called MIX and recognised
as the main competition division before 2007.</li> <li>The LTB division: problems with very large axiomatisations
(some of them contain about 3.5 million axioms).</li></ol> <p>Here is the list of our achievements:</p> <table id="ttable"><tr><td></td> <td>FOF</td> <td>CNF/MIX</td> <td>LTB</td></tr> <tr><td>1999</td> <td></td> <td>winner</td> <td>-</td></tr> <tr><td>2000</td> <td>winner</td> <td></td> <td>-</td></tr> <tr><td>2001</td> <td></td> <td>winner</td> <td>-</td></tr> <tr><td>2002</td> <td>winner</td> <td>winner</td> <td>-</td></tr> <tr><td>2003</td> <td>winner</td> <td>winner</td> <td>-</td></tr> <tr><td>2004</td> <td>winner*</td> <td>winner</td> <td>-</td></tr> <tr><td>2005</td> <td>winner</td> <td>winner*</td> <td>-</td></tr> <tr><td>2006</td> <td>winner</td> <td>winner*</td> <td>-</td></tr> <tr><td>2007</td> <td>winner</td> <td>winner*</td> <td>-</td></tr> <tr><td>2008</td> <td>winner</td> <td>winner*</td> <td></td></tr> <tr><td>2009</td> <td>winner</td> <td>winner*</td> <td>winner</td></tr> <tr><td>2010</td> <td>winner</td> <td>winner</td> <td>winner*</td></tr> <tr><td>2011</td> <td>winner*</td> <td></td> <td>winner*</td></tr> <tr><td>2012 (IJCAR)</td> <td>winner*</td> <td></td> <td>winner</td></tr> <tr><td>2012 (Turing)</td> <td>winner*</td> <td></td> <td>winner</td></tr> <tr><td>2013</td> <td>winner</td> <td></td> <td></td></tr></table> <p>Note: winner* means that Vampire solved more problems that all other provers
in this division and '-' means that the division did not exist that year.</p> <h2>V for Victory for V for Vampire?</h2> <img src="vv.jpg" /></td></tr></table><div style="clear:left"> </div>
</body>
</html>