{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:01:49Z","timestamp":1760079709122},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_17","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T07:20:19Z","timestamp":1378884019000},"page":"245-260","source":"Crossref","is-referenced-by-count":12,"title":["Mechanizing the Metatheory of Sledgehammer"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reasoning (to appear)"},{"key":"17_CR2","unstructured":"Berghofer, S.: First-order logic according to Fitting. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs (2007), http:\/\/afp.sf.net\/entries\/FOL-Fitting.shtml"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 493\u2013507. Springer, Heidelberg (2013)"},{"key":"17_CR4","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Tech. report associated with TACAS 2013 paper [3] (2013), http:\/\/www21.in.tum.de\/~blanchet\/enc_types_report.pdf"},{"issue":"4","key":"17_CR5","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10817-011-9234-1","volume":"47","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Autom. Reasoning\u00a047(4), 369\u2013398 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"17_CR6","unstructured":"Blanchette, J.C., Popescu, A.: Formal development associated with this paper (2013), http:\/\/www21.in.tum.de\/~popescua\/fol_devel.zip"},{"key":"17_CR7","unstructured":"Blanchette, J.C., Popescu, A.: Sound and complete sort encodings for first-order logic. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs (2013), http:\/\/afp.sourceforge.net\/entries\/Sort_Encodings.shtml"},{"key":"17_CR8","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Coinductive pearl: Modular first-order logic completeness (submitted), http:\/\/www21.in.tum.de\/~blanchet\/compl.pdf"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-69738-1_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C. Bouillaguet","year":"2007","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 74\u201388. Springer, Heidelberg (2007)"},{"key":"17_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-22438-6_17","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity\u2014Translating between many-sorted and unsorted first-order logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 207\u2013221. Springer, Heidelberg (2011)"},{"issue":"1","key":"17_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. J. ACM\u00a039(1), 95\u2013146 (1992)","journal-title":"J. ACM"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0055135","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 153\u2013170. Springer, Heidelberg (1998)"},{"key":"17_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 177\u2013191. Springer, Heidelberg (2006)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-14052-5_5","volume-title":"Interactive Theorem Proving","author":"B. Huffman","year":"2010","unstructured":"Huffman, B., Urban, C.: A new foundation for Nominal Isabelle. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 35\u201350. Springer, Heidelberg (2010)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M.T., Paulson, L.C.: Locales - A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Monk, J.D.: Mathematical Logic. Springer (1976)","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-22863-6_20","volume-title":"Interactive Theorem Proving","author":"M.O. Myreen","year":"2011","unstructured":"Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 265\u2013280. Springer, Heidelberg (2011)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"17_CR19","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) IWIL 2010 (2010)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) PLDI 1988, pp. 199\u2013208. ACM (1988)","DOI":"10.1145\/960116.54010"},{"issue":"2","key":"17_CR21","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput.\u00a0186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"3","key":"17_CR22","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"A.M. Pitts","year":"2006","unstructured":"Pitts, A.M.: Alpha-structural recursion and induction. J. ACM\u00a053(3), 459\u2013506 (2006)","journal-title":"J. ACM"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP 2011, pp. 346\u2013358. ACM (2011)","DOI":"10.1145\/2034574.2034819"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Popescu, A., Gunter, E.L., Osborn, C.J.: Strong normalization of System F by HOAS on top of FOAS. In: LICS 2010, pp. 31\u201340. IEEE (2010)","DOI":"10.1109\/LICS.2010.48"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Metamathematics, Machines, and G\u00f6del\u2019s Proof. Cambridge Tracts in Theoretical Computer Science, vol.\u00a038. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511569883"},{"issue":"2","key":"17_CR27","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/AIC-130550","volume":"26","author":"G. Sutcliffe","year":"2013","unstructured":"Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition\u2014CASC-J6. AI Comm.\u00a026(2), 211\u2013223 (2013)","journal-title":"AI Comm."},{"key":"17_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2004","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 641\u2013653. Springer, Heidelberg (2004)"}],"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-642-40885-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T16:19:08Z","timestamp":1596471548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}