{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:20Z","timestamp":1775873660054,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142024","type":"print"},{"value":"9783642142031","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14203-1_9","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T13:10:58Z","timestamp":1278940258000},"page":"107-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":70,"title":["Sledgehammer: Judgement Day"],"prefix":"10.1007","author":[{"given":"Sascha","family":"B\u00f6hme","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,7,13]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A. Bradley","year":"2008","unstructured":"Bradley, A., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput.\u00a020, 379\u2013405 (2008)","journal-title":"Formal Asp. Comput."},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"738","DOI":"10.1007\/3-540-58156-1_53","volume-title":"Automated Deduction - CADE-12","author":"X. Huang","year":"1994","unstructured":"Huang, X.: Reconstructing proofs at the assertion level. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 738\u2013752. Springer, Heidelberg (1994)"},{"key":"9_CR3","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 NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"9_CR4","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. Automated Reasoning\u00a040, 35\u201360 (2008)","journal-title":"J. Automated Reasoning"},{"key":"9_CR5","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, 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002), \nhttp:\/\/www.in.tum.de\/~nipkow\/LNCS2283\/"},{"key":"9_CR7","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":"9_CR8","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun.\u00a015, 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"2-3","key":"9_CR9","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun.\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","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.: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th IJCAR Automated Theorem Proving System Competition \u2014 CASC-J4. AI Commun.\u00a022, 59\u201372 (2009)","journal-title":"AI Commun."},{"key":"9_CR12","first-page":"201","volume-title":"Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems","author":"G. Sutcliffe","year":"2004","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Sorge, V., Zhang, W. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"issue":"1-2","key":"9_CR13","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. Automated Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Automated Reasoning"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Thery, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Robinson, G., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM\u00a012, 536\u2013541 (1965)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14203-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,20]],"date-time":"2021-08-20T02:05:36Z","timestamp":1629425136000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14203-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142024","9783642142031"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"13 July 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}