{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:41:34Z","timestamp":1725910894450},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319677286"},{"type":"electronic","value":"9783319677293"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67729-3_1","type":"book-chapter","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:04:04Z","timestamp":1505523844000},"page":"3-12","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Proof Generator from Semi-formal Proof Documents"],"prefix":"10.1007","author":[{"given":"Adri\u00e1n","family":"Riesco","sequence":"first","affiliation":[]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,17]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","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. 4350. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-71999-1"},{"issue":"11","key":"1_CR2","first-page":"1618","volume":"12","author":"M Clavel","year":"2006","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univ. Comput. Sci. 12(11), 1618\u20131650 (2006). Programming and Languages. Special Issue with Extended Versions of Selected Papers from PROLE 2005: The 5th Spanish Conference on Programming and Languages","journal-title":"J. Univ. Comput. Sci."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-33826-7_16"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-15545-6_13","volume-title":"Software, Services, and Systems","author":"K Futatsugi","year":"2015","unstructured":"Futatsugi, K.: Generate & check method for verifying transition systems in CafeOBJ. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 171\u2013192. Springer, Cham (2015). doi:\n10.1007\/978-3-319-15545-6_13"},{"key":"1_CR5","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.tcs.2012.07.041","volume":"464","author":"K Futatsugi","year":"2012","unstructured":"Futatsugi, K., G\u00e2in\u00e2, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoret. Comput. Sci. 464, 90\u2013112 (2012)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-40206-7_26","volume-title":"Algebra and Coalgebra in Computer Science","author":"D G\u00e2in\u00e2","year":"2013","unstructured":"G\u00e2in\u00e2, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 328\u2013333. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-40206-7_26"},{"key":"1_CR7","unstructured":"Garland, S.J., Guttag, J.V.: LP, the Larch Prover (Version 3.1). MIT Laboratory for Computer Science (1991)"},{"key":"1_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-6541-0","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"J Goguen","year":"2000","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-17511-4_20"},{"key":"1_CR10","unstructured":"Mossakowski, T., Maeder, C., Codescu, M., L\u00fccke, D.: Hets user guide -version 0.97-. Technical report, DFKI GmbH, Formal Methods for Software Development, February 2011"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"issue":"6","key":"1_CR12","first-page":"771","volume":"19","author":"K Ogata","year":"2013","unstructured":"Ogata, K., Futatsugi, K.: Compositionally writing proof scores of invariants in the OTS\/CafeOBJ method. J. UCS 19(6), 771\u2013804 (2013)","journal-title":"J. UCS"},{"issue":"5","key":"1_CR13","doi-asserted-by":"crossref","first-page":"1160","DOI":"10.1587\/transinf.E97.D.1160","volume":"97\u2013D","author":"I Ouranos","year":"2014","unstructured":"Ouranos, I., Ogata, K., Stefaneas, P.S.: TESLA source authentication protocol verification experiment in the timed OTS\/CafeOBJ method: experiences and lessons learned. IEICE Trans. 97\u2013D(5), 1160\u20131170 (2014)","journal-title":"IEICE Trans."},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi:\n10.1007\/3-540-55602-8_217"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle: A Generic Theorem Prover","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)"},{"key":"1_CR16","first-page":"1","volume":"29","author":"A Riesco","year":"2016","unstructured":"Riesco, A., Ogata, K., Futatsugi, K.: A Maude environment for CafeOBJ. Formal Aspects Comput. 29, 1\u201326 (2016)","journal-title":"Formal Aspects Comput."},{"key":"1_CR17","unstructured":"Sawada, T., Futatsugi, K., Preining, N.: CafeOBJ Reference Manual (version 1.5.3), February 2015"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67729-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:04:19Z","timestamp":1505523859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67729-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319677286","9783319677293"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67729-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}