{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:00:14Z","timestamp":1759147214197,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402050"},{"type":"electronic","value":"9783642402067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40206-7_26","type":"book-chapter","created":{"date-parts":[[2013,8,26]],"date-time":"2013-08-26T23:29:41Z","timestamp":1377559781000},"page":"328-333","source":"Crossref","is-referenced-by-count":10,"title":["Constructor-Based Inductive Theorem Prover"],"prefix":"10.1007","author":[{"given":"Daniel","family":"G\u0103in\u0103","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"Chiba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasuhito","family":"Arimoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","key":"26_CR1","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"1-2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2005.09.002","volume":"67","author":"M. Bidoit","year":"2006","unstructured":"Bidoit, M., Hennicker, R.: Constructor-based observational logic. J. Log. Algebr. Program.\u00a067(1-2), 3\u201351 (2006)","journal-title":"J. Log. Algebr. Program."},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.tcs.2012.07.041","volume":"464","author":"K. Futatsugi","year":"2012","unstructured":"Futatsugi, K., G\u0103in\u0103, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theor. Comput. Sci.\u00a0464, 90\u2013112 (2012)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"G\u0103in\u0103, D., Futatsugi, K.: Initial Semantics in Logics with Constructors. J. Log. Comput. (2013), \n                    \n                      http:\/\/dx.doi.org\/10.1093\/logcom\/exs044","key":"26_CR5","DOI":"10.1093\/logcom\/exs044"},{"doi-asserted-by":"crossref","unstructured":"G\u0103in\u0103, D., Lucanu, D., Ogata, K., Futatsugi, K.: On Automation of OTS\/CafeOBJ method (submitted, 2013)","key":"26_CR6","DOI":"10.1007\/978-3-642-54624-2_29"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.tcs.2012.12.002","volume":"474","author":"D. G\u0103in\u0103","year":"2013","unstructured":"G\u0103in\u0103, D.: Interpolation in logics with constructors. Theor. Comput. Sci.\u00a0474, 46\u201359 (2013)","journal-title":"Theor. Comput. Sci."},{"issue":"16","key":"26_CR8","first-page":"2204","volume":"18","author":"D. G\u0103in\u0103","year":"2012","unstructured":"G\u0103in\u0103, D., Futatsugi, K., Ogata, K.: Constructor-based logics. J. UCS\u00a018(16), 2204\u20132233 (2012)","journal-title":"J. UCS"},{"unstructured":"Hendrix, J.D.: Decision Procedures for Equationally Based Reasoning. Technical Report, UIUC (2008)","key":"26_CR9"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-642-03741-2_30","volume-title":"Algebra and Coalgebra in Computer Science","author":"D. Lucanu","year":"2009","unstructured":"Lucanu, D., Goriac, E.-I., Caltais, G., Ro\u015fu, G.: CIRC: A Behavioral Verification Tool Based on Circular Coinduction. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 433\u2013442. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Algebra and Coalgebra in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40206-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T19:58:17Z","timestamp":1558036697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40206-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402050","9783642402067"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40206-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}