{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T00:55:36Z","timestamp":1780707336524,"version":"3.54.1"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,5]],"date-time":"2013-03-05T00:00:00Z","timestamp":1362441600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10817-013-9278-5","type":"journal-article","created":{"date-parts":[[2013,3,4]],"date-time":"2013-03-04T15:50:18Z","timestamp":1362412218000},"page":"109-128","source":"Crossref","is-referenced-by-count":82,"title":["Extending Sledgehammer with SMT Solvers"],"prefix":"10.1007","volume":"51","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","published-online":{"date-parts":[[2013,3,5]]},"reference":[{"key":"9278_CR1","doi-asserted-by":"crossref","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.\u00a097\u2013116. Kluwer (1998)","DOI":"10.1007\/978-94-017-0435-9_4"},{"key":"9278_CR2","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Applied Logic, vol.\u00a027. Springer (2002)","DOI":"10.1007\/978-94-015-9934-4"},{"key":"9278_CR3","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011), LNCS, vol.\u00a07086, pp.\u00a0135\u2013150. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"9278_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard\u2014Version 2.0. In: Gupta, A., Kroening, D. (eds.) Satisfiability Modulo Theories (SMT) (2010)"},{"key":"9278_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV 2007), LNCS, vol.\u00a04590, pp.\u00a0298\u2013302. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"issue":"3","key":"9278_CR6","doi-asserted-by":"crossref","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. Form. Asp. Comput. 19(3), 321\u2013341 (2007)","journal-title":"Form. Asp. Comput."},{"issue":"2","key":"9278_CR7","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"9278_CR8","unstructured":"Besson, F., Fontaine, P., Th\u00e9ry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011), pp.\u00a015\u201326 (2011)"},{"issue":"3\u20134","key":"9278_CR9","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de\u00a0Nivelle, H.: Automatic proof construction in type using resolution. J. Autom. Reasoning 29(3\u20134), 253\u2013275 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"9278_CR10","unstructured":"Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. thesis, Dept. of Informatics, T.U. M\u00fcnchen (2012)"},{"key":"9278_CR11","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In:\u00a0Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23), LNAI, vol.\u00a06803, pp.\u00a0207\u2013221. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"9278_CR12","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), LNCS, vol.\u00a07795. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_34"},{"key":"9278_CR13","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle\u2014Superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving (ITP 2012), no. 7406 in LNCS, pp.\u00a0345\u2013360. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_24"},{"key":"9278_CR14","unstructured":"B\u00f6hme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. thesis, Dept. of Informatics, T.U. M\u00fcnchen (2012)"},{"key":"9278_CR15","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011), LNCS, vol.\u00a07086, pp.\u00a0183\u2013198. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_15"},{"issue":"1\u20132","key":"9278_CR16","doi-asserted-by":"crossref","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. Autom. Reasoning 44(1\u20132), 111\u2013144 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"9278_CR17","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2010), LNAI, vol.\u00a06173, pp.\u00a0107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9278_CR18","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) Interactive Theorem Proving (ITP 2010), LNCS, vol.\u00a06172, pp.\u00a0179\u2013194. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"9278_CR19","unstructured":"B\u00f6hme, S., Weber, T.: Designing proof formats: a user\u2019s perspective. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011), pp.\u00a027\u201332 (2011)"},{"key":"9278_CR20","doi-asserted-by":"crossref","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.C.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI 2007), LNCS, vol.\u00a04349, pp.\u00a074\u201388. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_5"},{"key":"9278_CR21","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20, 379\u2013405 (2008)","journal-title":"Form. Asp. Comput."},{"key":"9278_CR22","doi-asserted-by":"crossref","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.) Theorem Proving in Higher Order Logics (TPHOLs 2009), LNCS, vol.\u00a05674, pp.\u00a023\u201342. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"9278_CR23","doi-asserted-by":"crossref","unstructured":"Dahn, B., Gehne, J., Honigmann, T., Wolf, A.: Integration of automated and interactive theorem proving in ILF. In: McCune, W. (ed.) Conference on Automated Deduction (CADE-14), LNCS, vol.\u00a01249, pp.\u00a057\u201360. Springer (1997)","DOI":"10.1007\/3-540-63104-6_7"},{"key":"9278_CR24","unstructured":"Dutertre, B., de\u00a0Moura, L.: The Yices SMT solver. Available http:\/\/yices.csl.sri.com\/tool-paper.pdf (2006). Accessed 21 Feb 2013"},{"key":"9278_CR25","unstructured":"Erk\u00f6k, L., Matthews, J.: Using Yices as an automated solver in Isabelle\/HOL. In: Rushby, J., Shankar, N. (eds.) Automated Formal Methods (AFM08), pp.\u00a03\u201313 (2008)"},{"key":"9278_CR26","doi-asserted-by":"crossref","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. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006), LNCS, vol.\u00a03920, pp.\u00a0167\u2013181. Springer (2006)","DOI":"10.1007\/11691372_11"},{"key":"9278_CR27","doi-asserted-by":"crossref","unstructured":"Foster, S., Struth, G.: Integrating an automated theorem prover into Agda. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods (NFM 2011), LNCS, vol.\u00a06617, pp.\u00a0116\u2013130 (2011)","DOI":"10.1007\/978-3-642-20398-5_10"},{"key":"9278_CR28","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol.\u00a078. Springer (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9278_CR29","doi-asserted-by":"crossref","unstructured":"Guttmann, W., Struth, G., Weber, T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) International Conference on Formal Engineering Methods (ICFEM 2011), LNCS, vol.\u00a06991, pp.\u00a0617\u2013632. Springer (2011)","DOI":"10.1007\/978-3-642-24559-6_41"},{"key":"9278_CR30","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23), LNAI, vol.\u00a06803, pp.\u00a0299\u2013314. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"9278_CR31","doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M.: Super-combinators: A new implementation method for applicative languages. In: LISP and Functional Programming (LFP 1982), pp.\u00a01\u201310. ACM Press (1982)","DOI":"10.1145\/800068.802129"},{"key":"9278_CR32","doi-asserted-by":"crossref","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs \u201999), LNCS, vol.\u00a01690, pp.\u00a0311\u2013321 (1999)","DOI":"10.1007\/3-540-48256-3_21"},{"key":"9278_CR33","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di\u00a0Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, no.\u00a0CP-2003-212448 in NASA Technical Reports, pp.\u00a056\u201368 (2003)"},{"key":"9278_CR34","unstructured":"Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs. http:\/\/afp.sf.net\/ . Accessed 21 Feb 2013"},{"key":"9278_CR35","doi-asserted-by":"crossref","unstructured":"McCune, W., Shumsky, O.: System description: IVY. In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol.\u00a01831, pp.\u00a0401\u2013405. Springer (2000)","DOI":"10.1007\/10721959_30"},{"issue":"2","key":"9278_CR36","doi-asserted-by":"crossref","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. 144(2), 43\u201351 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9278_CR37","doi-asserted-by":"crossref","unstructured":"Meier, A.: Tramp: Transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol.\u00a01831, pp.\u00a0460\u2013464. Springer (2000)","DOI":"10.1007\/10721959_37"},{"issue":"1","key":"9278_CR38","doi-asserted-by":"crossref","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. Autom. Reasoning 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"9278_CR39","doi-asserted-by":"crossref","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. Journal of Applied Logic 7(1), 41\u201357 (2009)","journal-title":"Journal of Applied Logic"},{"key":"9278_CR40","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) Satisfiability Modulo Theories (SMT 2009) (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"9278_CR41","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol.\u00a04963, pp.\u00a0337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9278_CR42","unstructured":"Nipkow, T.: Re: [isabelle] A beginner\u2019s questionu [sic]. Archived https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2010-November\/msg00097.html (2010). Accessed 21 Feb 2013"},{"key":"9278_CR43","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9278_CR44","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp.\u00a0335\u2013367. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"9278_CR45","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 (IWIL-2010) (2010)"},{"key":"9278_CR46","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007), LNCS, vol.\u00a04732, pp.\u00a0232\u2013245 (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9278_CR47","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2. http:\/\/smtlib.cs.uiowa.edu\/papers\/format-v1.2-r06.08.30.pdf (2006). Accessed 21 Feb 2013"},{"key":"9278_CR48","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction\u2014A Basis for Applications, vol.\u00a0III: Applications, pp.\u00a0225\u2013241. Kluwer (1998)","DOI":"10.1007\/978-94-017-0437-3_9"},{"issue":"2\u20133","key":"9278_CR49","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"9278_CR50","doi-asserted-by":"crossref","unstructured":"Rinard, M.C.: Integrated reasoning and proof choice point selection in the Jahob system\u2014mechanisms for program survival. In: Schmidt, R.A. (ed.) Conference on Automated Deduction (CADE-22), LNCS, vol.\u00a05663, pp.\u00a01\u201316. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_1"},{"key":"9278_CR51","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011) (2011)"},{"key":"9278_CR52","doi-asserted-by":"crossref","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 (SEFM 2006), p.\u00a0262. IEEE (2006)","DOI":"10.1109\/SEFM.2006.37"},{"key":"9278_CR53","unstructured":"Schropp, A.: Instantiating Deeply Embedded Many-sorted Theories into HOL Types in Isabelle. M.Sc. thesis, Dept. of Informatics, T.U. M\u00fcnchen (2012)"},{"key":"9278_CR54","unstructured":"Schulz, S.: System description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2004), LNAI, vol.\u00a03097, pp.\u00a0223\u2013228. Springer (2004)"},{"key":"9278_CR55","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with \u03a9 mega: the irrationality of $\\sqrt2$ . In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics, Applied Logic, vol.\u00a028, pp.\u00a0271\u2013314. Springer (2003)","DOI":"10.1007\/978-94-017-0253-9_11"},{"key":"9278_CR56","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol.\u00a01831, pp.\u00a0406\u2013410. Springer (2000)","DOI":"10.1007\/10721959_31"},{"issue":"4","key":"9278_CR57","doi-asserted-by":"crossref","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\u2014the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"9278_CR58","unstructured":"Wampler-Doty, M.: A complete proof of the Robbins conjecture. In: G. Klein, T. Nipkow, L. Paulson (eds.) The Archive of Formal Proofs. Available http:\/\/afp.sf.net\/entries\/Robbins-Conjecture.shtml (2010). Accessed 21 Feb 2013"},{"issue":"5","key":"9278_CR59","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: new oracles for the HOL theorem prover. J. Softw. Tools Technol. Transfer 13(5), 419\u2013429 (2011)","journal-title":"J. Softw. Tools Technol. Transfer"},{"key":"9278_CR60","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp.\u00a01965\u20132013. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"9278_CR61","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) Theorem Proving in Higher Order Logics (TPHOLs \u201997), LNCS, vol.\u00a01275, pp.\u00a0307\u2013322 (1997)","DOI":"10.1007\/BFb0028402"},{"key":"9278_CR62","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Dos\u00a0Reis, G., Th\u00e9ry, L. (eds.) Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library (2009)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9278-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9278-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9278-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T22:54:13Z","timestamp":1745967253000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9278-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,5]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["9278"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9278-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,5]]}}}