{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:54:41Z","timestamp":1781762081381,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":60,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642243639","type":"print"},{"value":"9783642243646","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-24364-6_2","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T01:22:21Z","timestamp":1317259341000},"page":"12-27","source":"Crossref","is-referenced-by-count":61,"title":["Automatic Proof and Disproof in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lukas","family":"Bulwahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1721654.1721675","volume":"53","author":"S. Antoy","year":"2010","unstructured":"Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM\u00a053, 74\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"2_CR2","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)"},{"key":"2_CR3","first-page":"230","volume-title":"SEFM 2004","author":"S. Berghofer","year":"2004","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) SEFM 2004, pp. 230\u2013239. IEEE C.S., Los Alamitos (2004)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"2_CR5","unstructured":"Blanchette, J.C.: Relational analysis of (co)inductive predicates (co)inductive datatypes, and (co)recursive functions. Softw. Qual. J. (to appear)"},{"key":"2_CR6","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"2_CR7","unstructured":"Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Auto. Reas. (to appear)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"2_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":"2_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":"2_CR11","series-title":"Leibniz International Proceedings in Informatics","first-page":"139","volume-title":"ICLP 2011 (Technical Communications)","author":"L. Bulwahn","year":"2011","unstructured":"Bulwahn, L.: Smart test data generators via logic programming. In: Gallagher, J.P., Gelfond, M. (eds.) ICLP 2011 (Technical Communications). Leibniz International Proceedings in Informatics, vol.\u00a011, pp. 139\u2013150. Schloss Dagstuhl, Leibniz-Zentrum f\u00fcr Informatik (2011)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-540-74591-4_5","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2007","unstructured":"Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in isabelle\/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 38\u201353. Springer, Heidelberg (2007)"},{"key":"2_CR13","unstructured":"Chamarthi, H.R., Dillinger, P., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving (2011), \n                    \n                      http:\/\/arxiv.org\/pdf\/1105.4394"},{"key":"2_CR14","first-page":"268","volume-title":"ICFP 2000","author":"K. Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: A lightweight tool for random testing of Haskell programs. In: ICFP 2000, pp. 268\u2013279. ACM, New York (2000)"},{"key":"2_CR15","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: Translating 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)"},{"key":"2_CR16","unstructured":"Dutertre, B., de\u00a0Moura, L.: The Yices SMT solver (2006), \n                    \n                      http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"2_CR18","first-page":"11","volume-title":"ICFP 2009","author":"S. Fischer","year":"2009","unstructured":"Fischer, S., Kiselyov, O., Shan, C.: Purely functional lazy non-deterministic programming. In: ICFP 2009, pp. 11\u201322. ACM, New York (2009)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-20398-5_10","volume-title":"NASA Formal Methods","author":"S. Foster","year":"2011","unstructured":"Foster, S., Struth, G.: Integrating an automated theorem prover into Agda. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"2_CR20","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A\u00a0Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"2_CR23","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"#cr-split#-2_CR24.1","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, pp. 56\u201368 (2003);"},{"key":"#cr-split#-2_CR24.2","unstructured":"No. CP-2003-212448 in NASA Technical Reports"},{"key":"2_CR25","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"2_CR26","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)"},{"key":"2_CR27","unstructured":"Keller, C.: Cooperation between SAT, SMT provers and Coq"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Jackson, D.: Relational analysis of algebraic datatypes. In: Gall, H.C. (ed.) ESEC\/ FSE 2005. ACM, New York (2005)","DOI":"10.1145\/1081706.1081740"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/j.entcs.2007.09.018","volume":"196","author":"F. Lindblad","year":"2008","unstructured":"Lindblad, F.: Higher-order proof construction based on first-order narrowing. Electr. Notes Theor. Comput. Sci.\u00a0196, 69\u201384 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR30","first-page":"105","volume-title":"TFP 2007","author":"F. Lindblad","year":"2008","unstructured":"Lindblad, F.: Property directed generation of first-order test data. In: Moraz\u00e1n, M. (ed.) TFP 2007, pp. 105\u2013123. Intellect, Bristol (2008)"},{"issue":"1","key":"2_CR31","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":"2_CR32","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":"2_CR33","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":"2_CR34","unstructured":"Nipkow, T.: A tutorial introduction to structured Isar proofs (2011), \n                    \n                      http:\/\/isabelle.in.tum.de\/dist\/Isabelle\/doc\/isar-overview.pdf"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.T.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"2_CR36","unstructured":"Owre, S.: Random testing in PVS. In: AFM 2006 (2006)"},{"issue":"3","key":"2_CR37","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L.C. Paulson","year":"1993","unstructured":"Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Auto. Reas.\u00a011(3), 353\u2013389 (1993)","journal-title":"J. Auto. Reas."},{"issue":"2","key":"2_CR38","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"Paulson, L.C.: Set theory for verification: II. Induction and recursion. J. Auto. Reas.\u00a015(2), 167\u2013215 (1995)","journal-title":"J. Auto. Reas."},{"key":"2_CR39","first-page":"23","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C.: Generic automatic proof tools. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, pp. 23\u201347. MIT Press, Cambridge (1997)"},{"issue":"3","key":"2_CR40","first-page":"73","volume":"5","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. Univ. Comp. Sci.\u00a05(3), 73\u201387 (1999)","journal-title":"J. Univ. Comp. Sci."},{"key":"2_CR41","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.) IWIL 2010 (2010)"},{"key":"2_CR42","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":"2_CR43","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":"2_CR44","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":"2_CR45","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: PxTP 2011 (2011)"},{"key":"2_CR46","first-page":"37","volume-title":"Haskell Symposium 2008","author":"C. Runciman","year":"2008","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values. In: Haskell Symposium 2008, pp. 37\u201348. ACM, New York (2008)"},{"key":"2_CR47","first-page":"262","volume-title":"SEFM 2006","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.) SEFM 2006, p. 262. IEEE, Los Alamitos (2006)"},{"key":"2_CR48","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":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"2_CR50","series-title":"LNCS (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)"},{"issue":"1","key":"2_CR51","first-page":"71","volume":"21","author":"G. Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 automated theorem proving system competition. AI Commun.\u00a021(1), 71\u201382 (2008)","journal-title":"AI Commun."},{"key":"2_CR52","series-title":"Frontiers in Artificial Intelligence and Applications","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: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol.\u00a0112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"key":"2_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"2_CR54","unstructured":"Weber, T.: SAT-Based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Dept. of Informatics, T.U. M\u00fcnchen (2008)"},{"key":"2_CR55","unstructured":"Weber, T.: SMT solvers: New oracles for the HOL theorem prover. In: VSTTE 2009 (2009)"},{"key":"2_CR56","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":"2_CR57","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof\u2014Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23). University of Bia\u0142ystok (2007)"},{"key":"2_CR58","unstructured":"Wenzel, M.: Asynchronous proof processing with Isabelle\/Scala and Isabelle\/jEdit. In: Coen, C.S., Aspinall, D. (eds.) UITP 2010 (2010)"},{"key":"2_CR59","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)"}],"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-24364-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T04:05:42Z","timestamp":1548475542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24364-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243639","9783642243646"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24364-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}