{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:34:09Z","timestamp":1725838449496},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_16","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"219-232","source":"Crossref","is-referenced-by-count":5,"title":["TIP: Tools for Inductive Provers"],"prefix":"10.1007","author":[{"given":"Dan","family":"Ros\u00e9n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicholas","family":"Smallbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/978-3-319-09099-3_2","volume-title":"Tests and Proofs","author":"N Amin","year":"2014","unstructured":"Amin, N., Leino, K.R.M., Rompf, T.: Computing with an SMT solver. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 20\u201335. Springer, Heidelberg (2014)"},{"key":"16_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard - version 2.5. \n                    http:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.5-r2015-06-28.pdf"},{"key":"16_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":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 493\u2013507. Springer, Heidelberg (2013)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Barrett, C., de Moura, L. (eds.) SMT 2008: 6th International Workshop on Satisfiability Modulo. ACM International Conference Proceedings Series, vol. 367, pp. 1\u20135 (2008)","DOI":"10.1145\/1512464.1512466"},{"key":"16_CR5","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: In Workshop on Intermediate Veri cation Languages, Boogie, August 2011"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 87\u2013102. Springer, Heidelberg (2011)"},{"issue":"4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF01806315","volume":"9","author":"WN Chin","year":"1996","unstructured":"Chin, W.N., Darlington, J.: A higher-order removal method. LISP Symbolic Comput. 9(4), 287\u2013322 (1996)","journal-title":"LISP Symbolic Comput."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000 Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 268\u2013279, ACM, New York (2000)","DOI":"10.1145\/357766.351266"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-20615-8_23","volume-title":"Intelligent Computer Mathematics","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 333\u2013337. Springer, Heidelberg (2015)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-13977-2_3","volume-title":"Tests and Proofs","author":"K Claessen","year":"2010","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6\u201321. Springer, Heidelberg (2010)"},{"issue":"3","key":"16_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1134\/S0361768815030056","volume":"41","author":"SA Grechanik","year":"2015","unstructured":"Grechanik, S.A.: Proving properties of functional programs by equality saturation. Program. Comput. Softw. 41(3), 149\u2013161 (2015)","journal-title":"Program. Comput. Softw."},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-319-08434-3_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2014","unstructured":"Johansson, M., Ros\u00e9n, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 108\u2013122. Springer, Heidelberg (2014)"},{"key":"16_CR14","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Panagiotis, M., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-27940-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KRM Leino","year":"2012","unstructured":"Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315\u2013331. Springer, Heidelberg (2012)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: The ACM Annual Conference, vol. 2 (1972)","DOI":"10.1145\/800194.805852"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Sonnex","year":"2012","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407\u2013421. Springer, Heidelberg (2012)"},{"key":"16_CR19","unstructured":"Wand, D., Weidenbach, C.: Automatic induction inside superposition. \n                    https:\/\/people.mpi-inf.mpg.de\/~dwand\/datasup\/draft.pdf"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:44:38Z","timestamp":1559331878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}