forked from vprover/vprover.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpubs.html
47 lines (46 loc) · 14.4 KB
/
pubs.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
<!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>Publications About Vampire</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"> <h1>Publications About Vampire</h1>
<p>This is a list of publications related to Vampire. <i>(This list is out of date, at the moment please refer to the team's personal or DBLP pages for related papers)</i></p>
<h4>2013</h4> <div class="publist">
<li class="pub"><span><a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle">First-Order Theorem Proving and Vampire</span>. <span class="conf">CAV 2013</span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-38574-2_33">The 481 Ways to Split a Clause and Deal with Propositional Variables</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/cade2013.html">CADE 2013</a></span></li></div> <h4>2012</h4> <div class="publist">
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://doi.acm.org/10.1145/2103656.2103689">Playing in the grey area of proofs</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/popl/popl2012.html">POPL 2012</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://forsyte.at/people/holzer/">Andreas Holzer</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-35182-2_11">Vinter: A Vampire-Based Tool for Interpolation</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/aplas/aplas2012.html">APLAS 2012</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://il.linkedin.com/pub/zurab-khasidashvili/4/a80/a74">Zurab Khasidashvili</a>, <a href="http://www.cs.man.ac.uk/~korovink/">Konstantin Korovin</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462554">Preprocessing techniques for first-order clausification</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/fmcad/fmcad2012.html">FMCAD 2012</a></span></li></div> <h4>2011</h4> <div class="publist">
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-22438-6_23">Sine Qua Non for Large Theory Reasoning</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~%20ley/db/conf/cade/cade2011.html">CADE 2011</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-25324-9_1">Case Studies on Invariant Generation Using a Saturation Theorem Prover</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/micai/micai2011-1.html">MICAI 2011</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-19835-9_7">Invariant Generation in Vampire</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/tacas/tacas2011.html">TACAS 2011</a></span></li></div> <h4>2010</h4> <div class="publist">
<li class="pub"><span><a href="http://pub.ist.ac.at/~tah/">Thomas Henzinger</a>, <a href="http://parlab.eecs.berkeley.edu/node/274">Thibaud Hottelier</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-11319-2_14">Invariant and Type Inference for Matrices</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/vmcai/vmcai2010.html">VMCAI 2010</a></span></li>
<li class="pub"><span><a href="http://cs.ru.nl/~urban/">Josef Urban</a>, <a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.com/content/pdf/10.1007%2F978-3-642-15582-6_30.pdf">Evaluation of Automated Theorem Proving on the Mizar Mathematical Library</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/icms/icms2010.html">ICMS 2010</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-14203-1_16">Interpolation and Symbol Elimination in Vampire</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~%20ley/db/conf/cade/ijcar2010.html">IJCAR 2010</a></span></li></div> <h4>2009</h4> <div class="publist">
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~hoderk/">Krystof Hoder</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-04617-9_55">Comparing Unification Algorithms in First-Order Theorem Proving</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/ki/ki2009.html">KI 2009</a></span></li>
<li class="pub"><span><a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-00593-0_33">Finding Loop Invariants for Programs over Arrays Using a Theorem Prover</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/fase/fase2009.html">FASE 2009</a></span></li>
<li class="pub"><span><a href="http://www.cse.chalmers.se/~laurako/">Laura Kovacs</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/978-3-642-02959-2_17">Interpolation and Symbol Elimination</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/cade2009.html">CADE 2009</a></span></li></div> <h4>2006</h4> <div class="publist">
<li class="pub"><span><a href="http://web.comlab.ox.ac.uk/ian.horrocks/">Ian Horrocks</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/11663881_12">Reasoning Support for Expressive Ontology Languages Using a Theorem Prover</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/foiks/foiks2006.html">FoIKS 2006</a></span></li>
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1016/j.ic.2004.10.012">Efficient Instance Retrieval with Standard and Relational Path Indexing</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/journals/iandc/iandc199.html">Information and Computation, vol. 199</a></span></li></div> <h4>2004</h4> <div class="publist">
<li class="pub"><span><a href="http://www.csc.liv.ac.uk/~ullrich/">Ullrich Hustadt</a>, <a href="http://www.csc.liv.ac.uk/~konev/">Boris Konev</a>, <a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3097&spage=326">TeMP: A Temporal Monodic Prover</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/ijcar2004.html">IJCAR 2004</a></span></li>
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3097&spage=60">Efficient Checking of Term Ordering Constraints</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/ijcar2004.html">IJCAR 2004</a></span></li>
<li class="pub"><span><a href="http://www.cs.manchester.ac.uk/~tsarkov/">Dmitry Tsarkov</a>, <a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.cs.manchester.ac.uk/~seanb/">Sean Bechhofer</a>, <a href="http://web.comlab.ox.ac.uk/ian.horrocks/">Ian Horrocks</a></span>. <span class="ptitle"><a href="http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3298&spage=471">Using Vampire to Reason with OWL</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/semweb/iswc2004.html">ISWC 2004</a></span></li></div> <h4>2003</h4> <div class="publist">
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1016/S0747-7171(03)00040-3">Limited Resource Strategy in Resolution Theorem Proving</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/journals/jsc/jsc36.html">Journal of Symbolic Computation</a></span></li></div> <h4>2002</h4> <div class="publist">
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91">The Design and Implementation of Vampire</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/journals/aicom/aicom15.html">AI Commun. 15</a></span></li></div> <h4>2001</h4> <div class="publist">
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.4605">Splitting without Backtracking</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/ijcai/ijcai2001.html">IJCAI 2001</a></span></li>
<li class="pub"><span><a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.de/link/service/series/0558/bibs/2083/20830013.htm">Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/ijcar2001.html">IJCAR 2001</a></span></li>
<li class="pub"><span><a href="http://www.lsi.upc.edu/~roberto/">Robert Nieuwenhuis</a>, <a href="http://www.mpi-inf.mpg.de/~hillen/">Thomas Hillenbrand</a>, <a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.de/link/service/series/0558/bibs/2083/20830257.htm">On the Evaluation of Indexing Techniques for Theorem Proving</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/ijcar2001.html">IJCAR 2001</a></span></li>
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://dx.doi.org/10.1007/3-540-45575-2_11">Adaptive Saturation-Based Reasoning</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/ershov/ershov2001.html">Ershov Memorial Conference 2001</a></span></li>
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.de/link/service/series/0558/bibs/2083/20830376.htm">Vampire 1.1 (System Description)</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/ijcar2001.html">IJCAR 2001</a></span></li></div> <h4>2000</h4> <div class="publist">
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.de/link/service/series/0558/bibs/1919/19190209.htm">Partially Adaptive Code Trees</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/jelia/jelia2000.html">JELIA 2000</a></span></li></div> <h4>1999</h4> <div class="publist">
<li class="pub"><span><a href="http://www.freewebs.com/riazanov/">Alexandre Riazanov</a>, <a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://link.springer.de/link/service/series/0558/bibs/1632/16320292.htm">Vampire</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/cade99.html">CADE 1999</a></span></li></div> <h4>1995</h4> <div class="publist">
<li class="pub"><span><a href="http://www.voronkov.com/">Andrei Voronkov</a></span>. <span class="ptitle"><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.8772">Implementing Bottom-Up Procedures with Code Trees</a></span>. <span class="conf"><a href="http://www.informatik.uni-trier.de/~ley/db/journals/jar/jar15.html">Journal of Automated Reasoning, vol. 15</a></span></li></div></td></tr></table>
</body>
</html>