{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:18:54Z","timestamp":1725830334959},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_16","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T00:20:53Z","timestamp":1442622053000},"page":"256-271","source":"Crossref","is-referenced-by-count":0,"title":["Proofs and Reconstructions"],"prefix":"10.1007","author":[{"given":"Nik","family":"Sultana","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"16_CR1","unstructured":"Benzm\u00fcller, C.: Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Naturwissenschaftlich-Technische Fakult\u00e4t I, Saarland University (1999)"},{"issue":"1:6","key":"16_CR2","first-page":"1","volume":"5","author":"C. Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C., Brown, C.E., Kohlhase, M.: Cut-Simulation and Impredicativity. Logical Methods in Computer Science\u00a05(1:6), 1\u201321 (2009)","journal-title":"Logical Methods in Computer Science"},{"key":"16_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C.E. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Rabe, F., Sutcliffe, G.: THF0 \u2013 The core TPTP language for classical higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"key":"16_CR4","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., Theiss, F., Paulson, L.C., Fietzke, A.: LEO-II \u2013 A 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)"},{"key":"16_CR5","unstructured":"Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"16_CR6","unstructured":"B\u00f6hme, S., Weber, T.: Designing proof formats: A user\u2019s perspective. In: Fontaine, P., Stump, A. (eds.) International Workshop on Proof Exchange for Theorem Proving, pp. 27\u201332 (2011)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"C.E. Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38574-2_11","volume-title":"Automated Deduction \u2013 CADE-24","author":"Z. Chihani","year":"2013","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 162\u2013177. Springer, Heidelberg (2013)"},{"key":"16_CR9","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. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"de Nivelle, H.: Extraction of proofs from clausal normal form transformation. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol.\u00a02471, pp. 584\u2013598. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45793-3_39"},{"key":"16_CR11","unstructured":"Dowek, G.: Skolemization in simple type theory: the logical and the theoretical points of view. In: Benzm\u00fcller, C., Brown, C.E., Siekmann, J., Statman, R. (eds.) Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Studies in Logic and the Foundations of Mathematics. College Publications (2009)"},{"key":"16_CR12","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, September 2003"},{"key":"16_CR13","unstructured":"Keller, C.: A Matter of Trust: Skeptical Communication Between Coq and External Provers. PhD thesis, \u00c9cole Polytechnique, June 2013"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle \u2013 A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"16_CR16","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: International Workshop on the Implementation of Logics. EasyChair (2010)"},{"issue":"2\/3","key":"16_CR17","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. Journal of Applied Logic (2012)","DOI":"10.1016\/j.jal.2012.12.002"},{"key":"16_CR19","unstructured":"Sultana, N.: Higher-order proof translation. PhD thesis, Computer Laboratory, University of Cambridge, Available as Tech Report UCAM-CL-TR-867 (2015)"},{"issue":"4","key":"16_CR20","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: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 1965\u20132013. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T20:37:43Z","timestamp":1559248663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}