{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:08Z","timestamp":1776333428088,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_1","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T23:13:06Z","timestamp":1373497986000},"page":"1-35","source":"Crossref","is-referenced-by-count":275,"title":["First-Order Theorem Proving and Vampire"],"prefix":"10.1007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol.\u00a0I, pp. 19\u201399. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"1_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), http:\/\/www.SMT-LIB.org"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P. Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing Finite Models by Reduction to Function-Free Clause Logic. J. of Applied Logic\u00a07(1), 58\u201374 (2009)","journal-title":"J. of Applied Logic"},{"issue":"3-4","key":"1_CR4","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B.: An Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal. J. of Symbolic Computation\u00a041(3-4), 475\u2013511 (2006); Phd thesis 1965, University of Innsbruck, Austria","journal-title":"J. of Symbolic Computation"},{"issue":"3","key":"1_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. J. of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"J. of Symbolic Logic"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J. Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT \u2014 A Distributed and Learning Equational Prover. J. of Automated Reasoning\u00a018(2), 189\u2013198 (1997)","journal-title":"J. of Automated Reasoning"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 9, vol.\u00a0I, pp. 535\u2013610. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"1_CR8","unstructured":"Ganzinger, H., Korovin, K.: New Directions in Instantiation-Based Theorem Proving. In: Proc. of LICS, pp. 55\u201364 (2003)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-25324-9_1","volume-title":"Advances in Artificial Intelligence","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Case Studies on Invariant Generation Using a Saturation Theorem Prover. In: Batyrshin, I., Sidorov, G. (eds.) MICAI 2011, Part I. LNCS, vol.\u00a07094, pp. 1\u201315. Springer, Heidelberg (2011)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-19835-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant Generation in Vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 60\u201364. Springer, Heidelberg (2011)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the Grey Area of Proofs. In: Proc. of POPL, pp. 259\u2013272 (2012)","DOI":"10.1145\/2103621.2103689"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K. Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing Unification Algorithms in First-Order Theorem Proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol.\u00a05803, pp. 435\u2013443. Springer, Heidelberg (2009)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: Simple Word Problems in Universal Algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-22438-6_28","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Korovin","year":"2011","unstructured":"Korovin, K., Voronkov, A.: Solving Systems of Linear Inequalities by Bound Propagation. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 369\u2013383. Springer, Heidelberg (2011)"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-22438-6_29","volume-title":"Automated Deduction \u2013 CADE-23","author":"L. Kov\u00e1cs","year":"2011","unstructured":"Kov\u00e1cs, L., Moser, G., Voronkov, A.: On Transfinite Knuth-Bendix Orders. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 384\u2013399. Springer, Heidelberg (2011)"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"key":"1_CR20","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Vampire Web Page (2013), http:\/\/vprover.org"},{"issue":"2-3","key":"1_CR21","first-page":"127","volume":"15","author":"B. L\u00f6chner","year":"2002","unstructured":"L\u00f6chner, B., Hillenbrand, T.: A Phytography of WALDMEISTER. AI Commun.\u00a015(2-3), 127\u2013133 (2002)","journal-title":"AI Commun."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Lusk, E.L.: Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. In: Proc. of LPAR, pp. 96\u2013106 (1992)","DOI":"10.1007\/BFb0013052"},{"issue":"2","key":"1_CR23","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An Efficient Unification Algorithm. TOPLAS\u00a04(2), 258\u2013282 (1982)","journal-title":"TOPLAS"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: OTTER 3.0 Reference Manual and Guide. Technical Report ANL-94\/6, Argonne National Laboratory (January 1994)","DOI":"10.2172\/10129052"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol.\u00a0I, pp. 371\u2013443. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"1-2","key":"1_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Journal of Symbolic Computations\u00a036(1-2), 101\u2013115 (2003)","journal-title":"Journal of Symbolic Computations"},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"2-3","key":"1_CR29","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2014 a Brainiac Theorem Prover. AI Commun.\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 26, vol.\u00a0II, pp. 1853\u20131964. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"issue":"4","key":"1_CR31","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. J. Autom. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"1_CR32","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/AIC-2012-0512","volume":"25","author":"G. Sutcliffe","year":"2012","unstructured":"Sutcliffe, G.: The CADE-23 Automated Theorem Proving System Competition - CASC-23. AI Commun.\u00a025(1), 49\u201363 (2012)","journal-title":"AI Commun."},{"key":"1_CR33","unstructured":"Sutcliffe, G.: The TPTP Problem Library (2013), http:\/\/www.cs.miami.edu\/~tptp\/"},{"key":"1_CR34","unstructured":"Sutcliffe, G.: The CADE ATP System Competition (2013), http:\/\/www.cs.miami.edu\/~tptp\/CASC\/"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Automated Deduction - Cade-13","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER. Version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 141\u2013145. Springer, Heidelberg (1996)"},{"key":"1_CR36","unstructured":"http:\/\/www.complang.tuwien.ac.at\/ioan\/boundPropagation . Vampire with Bound Propagation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T10:54:09Z","timestamp":1596106449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}