-
Notifications
You must be signed in to change notification settings - Fork 4
/
trophies.html
86 lines (81 loc) · 4.2 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
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
---
title: Our Trophies
layout: default
---
<h2>CASC</h2>
<table>
<tr>
<td colspan="3"><img src="img/trophies.JPG" alt="vampire trophies" width="660" height="380"></td>
</tr>
<tr>
<td><img src="img/trophy2.jpg" alt="more trophies" width="200" height="135"></td>
<td><img src="img/trophy1.jpg" alt="more trophies" width="200" height="135"></td>
<td><img src="img/trophy3.jpg" alt="more trophies" width="200" height="135"></td>
</tr>
</table>
<p>
Vampire has won at least one division of the world cup in theorem proving CASC since 1999.
All together Vampire won 45 titles: more than any other prover.
We take part in the following divisions of the competition:
</p>
<ol>
<li>
The FOF division: first-order theorems.
This division was ranked second in importance after the MIX division before 2007 and is now recognised as the main competition division.
<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>
The LTB division: problems with very large axiomatisations (some of them contain about 3.5 million axioms).
<li>
The EPR division: problems that fall within the Effectively Propositional fragment. We entered this track for the first time in 2015. The track is traditionally won by <a href="http://www.cs.man.ac.uk/~korovink/iprover/">iProver</a>
<li>
The FNT division: first-order non-theorems. We entered this track for the first time in 2015. Our success is supported heavily by our implementation of finite model building.
<li>
The TFA division: typed first-order theorems with arithmetic. We entered this track for the first time in 2015. Such problems are typically the domain of SMT solvers.
<li>
The SLH division: typed first-order theorems without arithmetic generated by Sledgehammer. This division has a much shorter time limit and is designed to reflect the Sledgehammer use case.
</ol>
<p>
Here is the list of our achievements:
</p>
<table>
<thead>
<tr><th>Year<th>FOF<th>CNF/MIX<th>LTB<th>EPR<th>FNT<th>TFA<th>SLH
<tbody>
<tr><td>1999<td><td>winner<td>-<td><td><td><td>
<tr><td>2000<td>winner<td><td>-<td><td><td><td>
<tr><td>2001<td><td>winner<td>-<td><td><td><td>
<tr><td>2002<td>winner<td>winner<td>-<td><td><td><td>
<tr><td>2003<td>winner<td>winner<td>-<td><td><td><td>
<tr><td>2004<td>winner*<td>winner<td>-<td><td><td><td>
<tr><td>2005<td>winner<td>winner*<td>-<td><td><td><td>
<tr><td>2006<td>winner<td>winner*<td>-<td><td><td><td>
<tr><td>2007<td>winner<td>winner*<td>-<td><td><td><td>
<tr><td>2008<td>winner<td>winner*<td>-<td><td><td><td>
<tr><td>2009<td>winner<td>winner*<td>winner<td><td><td><td>
<tr><td>2010<td>winner<td>winner*<td>winner<td><td><td><td>
<tr><td>2011<td>winner*<td>-<td>winner*<td><td><td><td>
<tr><td>2012 (IJCAR)<td>winner*<td>-<td>winner<td><td><td><td>
<tr><td>2012 (Turing)<td>winner*<td>-<td>winner<td><td><td><td>
<tr><td>2013<td>winner*<td>-<td><td><td><td><td>
<tr><td>2014<td>winner<td>-<td>-<td><td><td><td>
<tr><td>2015<td>winner<td>-<td>winner<td>winner<td>winner<td>winner<td>
<tr><td>2016<td>winner<td>-<td>winner<td><td>winner<td>winner<td>
<tr><td>2017<td>winner<td>-<td>winner<td><td>winner<td>winner<td>winner
<tr><td>2018<td>winner<td>-<td><td><td>winner<td>winner<td>-<td>
<tr><td>2019<td>winner<td>-<td><td>winner<td>winner<td>winner
<tr><td>2020<td>winner<td>-<td><td>-<td>winner<td>winner<td>-
<tr><td>2021<td>winner<td>-<td>winner<td>-<td>winner<td>-<td>-
<tr><td>2022<td>winner<td>-<td>winner<td>-<td>winner<td>-<td>-
</table>
<p>
Note: winner* means that Vampire solved more problems that all other provers in this division (this has not been computed post 2013) and '-' means that the division did not exist that year. Tracks EPR, FNT, and TFA were entered for the first time in 2015. Track SLH only ran in 2017.
</p>
<h2>SMTCOMP</h2>
<p>
Since 2016 we have also entered SMTCOMP.
We performed well both years (full details will be added here soon).
You can view the results for <a href="http://smtcomp.sourceforge.net/2016/results-summary.shtml?v=1467876482">2016</a> and <a href="http://smtcomp.sourceforge.net/2017/results-summary.shtml?v=1500632282">2017</a> directly.
Vampire competed in all tracks with quantifiers and without bitvectors or floating point.
</p>