{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T10:02:39Z","timestamp":1794391359487,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_11","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"116-130","source":"Crossref","is-referenced-by-count":61,"title":["Extending Sledgehammer with SMT Solvers"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sascha","family":"B\u00f6hme","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Systems and Implementation Techniques","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-94-017-0435-9_4","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Ahrendt","year":"1998","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., Menzel, W., Reif, W., Schellhorn, G., Schmitt, P.H.: Integrating automated and interactive theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction\u2014A Basis for Applications. Systems and Implementation Techniques, vol.\u00a0II, pp. 97\u2013116. Kluwer, Dordrecht (1998)"},{"key":"11_CR2","series-title":"Applied Logic","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Applied Logic, vol.\u00a027. Springer, Heidelberg (2002)","edition":"2"},{"key":"11_CR3","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-14203-1_7","volume-title":"Automated Reasoning","author":"J. Backes","year":"2010","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 76\u201390. Springer, Heidelberg (2010)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s00165-007-0027-6","volume":"19","author":"D. Barsotti","year":"2007","unstructured":"Barsotti, D., Nieto, L.P., Tiu, A.: Verification of clock synchronization algorithms: Experiments on a combination of deductive tools. Formal Asp. Comput.\u00a019(3), 321\u2013341 (2007)","journal-title":"Formal Asp. Comput."},{"key":"11_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"issue":"3-4","key":"11_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automatic proof construction in type theory using resolution. J. Auto. Reas.\u00a029(3-4), 253\u2013275 (2002)","journal-title":"J. Auto. Reas."},{"issue":"1-2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/s10817-009-9142-9","volume":"44","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie\u2014an interactive prover-backend for the Verifying C Compiler. J. Auto. Reas.\u00a044(1-2), 111\u2013144 (2010)","journal-title":"J. Auto. Reas."},{"key":"11_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A.R. Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput.\u00a020, 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"key":"11_CR12","unstructured":"Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality. Presentation at Dagstuhl Seminar on Deduction and Applications (2005)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"11_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73595-3_18","volume-title":"Automated Deduction \u2013 CADE-21","author":"J.-F. Couchot","year":"2007","unstructured":"Couchot, J.-F., Lescuyer, S.: Handling polymorphism in automated deduction. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 263\u2013278. Springer, Heidelberg (2007)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR16","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (2006), \n                  \n                    http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"11_CR17","unstructured":"Erk\u00f6k, L., Matthews, J.: Using Yices as an automated solver in Isabelle\/HOL. In: Rushby, J., Shankar, N. (eds.) Automated Formal Methods, pp. 3\u201313 (2008)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: These proceedings (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"11_CR21","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, number CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"11_CR22","unstructured":"Keller, C.: Cooperation between SAT, SMT provers and Coq. Presentation at the Synthesis. Verification and Analysis of Rich Models workshop (2011)"},{"key":"11_CR23","unstructured":"Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs, \n                  \n                    http:\/\/afp.sf.net\/"},{"key":"11_CR24","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-02959-2_14","volume-title":"Automated Deduction \u2013 CADE-22","author":"K. Korovin","year":"2009","unstructured":"Korovin, K.: Instantiation-based automated reasoning: From theory to practice. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 163\u2013166. Springer, Heidelberg (2009)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","volume":"144","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. Electr. Notes Theor. Comput. Sci.\u00a0144(2), 43\u201351 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"11_CR27","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Auto. Reas.\u00a040(1), 35\u201360 (2008)","journal-title":"J. Auto. Reas."},{"issue":"1","key":"11_CR28","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) Satisfiability Modulo Theories (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"11_CR30","unstructured":"Nipkow, T.: Re: [isabelle] A beginner\u2019s questionu [sic], (November 26, 2010), \n                  \n                    https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2010-November\/msg00097.html"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"11_CR32","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning","author":"A. Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"key":"11_CR33","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) International Workshop on the Implementation of Logics (2010)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"L.C. Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 232\u2013245. Springer, Heidelberg (2007)"},{"key":"11_CR35","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2 (2006), \n                  \n                    http:\/\/goedel.cs.uiowa.edu\/smtlib\/papers\/format-v1.2-r06.08.30.pdf"},{"issue":"2-3","key":"11_CR36","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Comm."},{"key":"11_CR37","first-page":"262","volume-title":"Software Engineering and Formal Methods","author":"J.M. Rushby","year":"2006","unstructured":"Rushby, J.M.: Tutorial: Automated formal methods with PVS, SAL, and Yices. In: Hung, D.V., Pandya, P. (eds.) Software Engineering and Formal Methods, p. 262. IEEE, New York (2006)"},{"key":"11_CR38","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"11_CR39","series-title":"Applied Logic","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-94-017-0253-9_11","volume-title":"Thirty Five Years of Automating Mathematics","author":"J. Siekmann","year":"2003","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with \u03a9mega: The irrationality of \n                  \n                    \n                  \n                  $\\sqrt2$\n                . In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics. Applied Logic, vol.\u00a028, pp. 271\u2013314. Springer, Heidelberg (2003)"},{"key":"11_CR40","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/10721959_31","volume-title":"Automated Deduction - CADE-17","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"key":"11_CR41","unstructured":"Sutcliffe, G., Chang, C., Ding, L., McGuinness, D., da Silva, P.P.: Different proofs are good proofs. In: McGuinness, D., Stump, A., Sutcliffe, G., Tinelli, C. (eds.) Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, pp. 1\u201310 (2010)"},{"issue":"1-2","key":"11_CR42","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Auto. Reas.\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Auto. Reas."},{"key":"11_CR43","unstructured":"Wampler-Doty, M.: A complete proof of the Robbins conjecture. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (2010), \n                  \n                    http:\/\/afp.sf.net\/entries\/Robbins-Conjecture.shtml"},{"key":"11_CR44","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965\u20132013. Elsevier, Amsterdam (2001)"},{"key":"11_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"11_CR46","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Dos Reis, G., Th\u00e9ry, L. (eds.) Programming Languages for Mechanized Mathematics Systems, ACM Digital Library (2009)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T02:44:38Z","timestamp":1553913878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}