{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T14:16:46Z","timestamp":1772893006867,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642546235","type":"print"},{"value":"9783642546242","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-642-54624-2_29","type":"book-chapter","created":{"date-parts":[[2014,2,28]],"date-time":"2014-02-28T17:42:59Z","timestamp":1393609379000},"page":"578-602","source":"Crossref","is-referenced-by-count":11,"title":["On Automation of OTS\/CafeOBJ Method"],"prefix":"10.1007","author":[{"given":"Daniel","family":"G\u0103in\u0103","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"29_CR1","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."},{"issue":"298","key":"29_CR2","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00865-4","volume":"3","author":"M. Bidoit","year":"2003","unstructured":"Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theor. Comput. Sci.\u00a03(298), 471\u2013510 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"29_CR3","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0304-3975(01)00317-6","volume":"286","author":"T. Borzyszkowski","year":"2002","unstructured":"Borzyszkowski, T.: Logical systems for structured specifications. Theor. Comput. Sci.\u00a0286(2), 197\u2013245 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR4","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 - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol.\u00a06. World Scientific (1998)","DOI":"10.1142\/3831"},{"issue":"2","key":"29_CR6","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/S0304-3975(01)00361-9","volume":"285","author":"R. Diaconescu","year":"2002","unstructured":"Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theor. Comput. Sci.\u00a0285(2), 289\u2013318 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Futatsugi, K.: Verifying Specifications with Proof Scores in CafeOBJ. In: ASE, pp. 3\u201310. IEEE Computer Society (2006)","DOI":"10.1109\/ASE.2006.73"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-540-69149-5_30","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K. Futatsugi","year":"2008","unstructured":"Futatsugi, K., Goguen, J.A., Ogata, K.: Verifying Design with Proof Scores. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol.\u00a04171, pp. 277\u2013290. Springer, Heidelberg (2008)"},{"key":"29_CR9","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."},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"G\u0103in\u0103, D., Futatsugi, K.: Initial Semnatics in Logics with Constructors. J. Log. Comput (2013), \n                  \n                    http:\/\/dx.doi.org\/10.1093\/logcom\/exs044","DOI":"10.1093\/logcom\/exs044"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-40206-7_26","volume-title":"CALCO 2013","author":"D. G\u0103in\u0103","year":"2013","unstructured":"G\u0103in\u0103, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based Inductive Theorem Prover. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol.\u00a08089, pp. 328\u2013333. Springer, Heidelberg (2013)"},{"key":"29_CR12","unstructured":"Goguen, J.: Theorem Proving and Algebra (1994)"},{"issue":"1","key":"29_CR13","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.: Institutions: Abstract Model Theory for Specification and Programming. Journal of the Association for Computing Machinery\u00a039(1), 95\u2013146 (1992)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Lin, K.: Behavioral Verification of Distributed Concurrent Systems with BOBJ. In: 3rd International Conference on Quality Software (QSIC), p. 216 (2003)","DOI":"10.1109\/QSIC.2003.1319106"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Lin, K., Rosu, G.: Circular Coinductive Rewriting. In: ASE, pp. 123\u2013132 (2000)","DOI":"10.1109\/ASE.2000.873657"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-16901-4_16","volume-title":"Formal Methods and Software Engineering","author":"E.-I. Goriac","year":"2010","unstructured":"Goriac, E.-I., Lucanu, D., Ro\u015fu, G.: Automating Coinduction with Case Analysis. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 220\u2013236. Springer, Heidelberg (2010)"},{"issue":"16","key":"29_CR17","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"},{"key":"29_CR18","unstructured":"Hendrix, J.D.: Decision Procedures for Equationally Based Reasoning. Technical Report, UIUC (2008)"},{"key":"29_CR19","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)"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-04164-8_4","volume-title":"Semantics and Algebraic Specification","author":"J. Meseguer","year":"2009","unstructured":"Meseguer, J.: Order-Sorted Parameterization and Induction. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol.\u00a05700, pp. 43\u201380. Springer, Heidelberg (2009)"},{"issue":"2","key":"29_CR21","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0020-0190(02)00480-5","volume":"86","author":"K. Ogata","year":"2003","unstructured":"Ogata, K., Futatsugi, K.: Flaw and modification of the iKP electronic payment protocols. Inf. Process. Lett.\u00a086(2), 57\u201362 (2003)","journal-title":"Inf. Process. Lett."},{"key":"29_CR22","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.entcs.2008.02.018","volume":"201","author":"K. Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Simulation-based Verification for Invariant Properties in the OTS\/CafeOBJ Method. Electr. Notes Theor. Comput. Sci.\u00a0201, 127\u2013154 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2\/3","key":"29_CR23","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0890-5401(88)90008-9","volume":"76","author":"D. Sannella","year":"1988","unstructured":"Sannella, D., Tarlecki, A.: Specifications in an Arbitrary Institution. Inf. Comput.\u00a076(2\/3), 165\u2013210 (1988)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Specification, Algebra, and Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54624-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T06:15:22Z","timestamp":1558851322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54624-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642546235","9783642546242"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54624-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}