{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:58Z","timestamp":1725551938141},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_21","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"288-303","source":"Crossref","is-referenced-by-count":0,"title":["Proving Injectivity of Functions via Program Inversion in Term Rewriting"],"prefix":"10.1007","author":[{"given":"Naoki","family":"Nishida","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahiko","family":"Sakai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2-3","key":"21_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/S0167-6423(02)00023-0","volume":"43","author":"S. Abramov","year":"2002","unstructured":"Abramov, S., Gl\u00fcck, R.: The universal resolving algorithm and its correctness: Inverse computation in a functional language. Science of Computer Programming\u00a043(2-3), 193\u2013229 (2002)","journal-title":"Science of Computer Programming"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-74130-5_15","volume-title":"Implementation and Application of Functional Languages","author":"J.M. Almendros-Jim\u00e9nez","year":"2007","unstructured":"Almendros-Jim\u00e9nez, J.M., Vidal, G.: Automatic partial inversion of inductively sequential functions. In: Horv\u00e1th, Z., Zs\u00f3k, V., Butterfield, A. (eds.) IFL 2006. LNCS, vol.\u00a04449, pp. 253\u2013270. Springer, Heidelberg (2007)"},{"key":"21_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-48685-2_2","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1999","unstructured":"Dershowitz, N., Mitra, S.: Jeopardy. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 16\u201329. Springer, Heidelberg (1999)"},{"issue":"2","key":"21_CR5","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(94)90241-0","volume":"134","author":"Z. F\u00fcl\u00f6p","year":"1994","unstructured":"F\u00fcl\u00f6p, Z.: Undecidable properties of deterministic top-down tree transducers. Theoretical Computer Science\u00a0134(2), 311\u2013328 (1994)","journal-title":"Theoretical Computer Science"},{"key":"21_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"unstructured":"Gramlich, B.: On the (non-)existence of least fixed points in conditional equational logic and conditional rewriting. In: Proc. 2nd Int. Workshop on Fixed Points in Computer Science (FICS 2000) \u2013 Extended Abstracts, pp. 38\u201340 (2000)","key":"21_CR7"},{"issue":"4","key":"21_CR8","first-page":"367","volume":"66","author":"R. Gl\u00fcck","year":"2005","unstructured":"Gl\u00fcck, R., Kawabe, M.: A method for automatic program inversion based on LR(0) parsing. Fundam. Inform.\u00a066(4), 367\u2013395 (2005)","journal-title":"Fundam. Inform."},{"issue":"5","key":"21_CR9","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1071221.1071222","volume":"40","author":"R. Gl\u00fcck","year":"2005","unstructured":"Gl\u00fcck, R., Kawabe, M.: Revisiting an automatic program inverter for Lisp. SIGPLAN Notices\u00a040(5), 8\u201317 (2005)","journal-title":"SIGPLAN Notices"},{"unstructured":"Kawabe, M., Futamura, Y.: Case studies with an automatic program inversion system. In: Proc. of the 21st Conference of Japan Society for Software Science and Technology, No. 6C-3, 5 pages (2004)","key":"21_CR10"},{"issue":"4","key":"21_CR11","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S. Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Information Processing Letters\u00a095(4), 446\u2013453 (2005)","journal-title":"Information Processing Letters"},{"doi-asserted-by":"crossref","unstructured":"Matsuda, K., Hu, Z., Nakano, K., Hamana, M., Takeichi, M.: Bidirectionalization transformation based on automatic derivation of view complement functions. In: Proc. of the 12th ACM SIGPLAN International Conference on Functional Programming, pp. 47\u201358 (2007)","key":"21_CR12","DOI":"10.1145\/1291151.1291162"},{"doi-asserted-by":"crossref","unstructured":"Matsuda, K., Mu, S.C., Hu, Z., Takeichi, M.: A grammar-based approach to invertible programs. In: Proc. of the 19th European Symposium on Programming (2010) (to appear)","key":"21_CR13","DOI":"10.1007\/978-3-642-11957-6_24"},{"key":"21_CR14","first-page":"177","volume-title":"Automata Studies","author":"J. McCarthy","year":"1956","unstructured":"McCarthy, J.: The inversion of functions defined by Turing machines. In: Automata Studies, pp. 177\u2013181. Princeton University Press, Princeton (1956)"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/11561347_14","volume-title":"Generative Programming and Component Engineering","author":"T.\u00c6. Mogensen","year":"2005","unstructured":"Mogensen, T.\u00c6.: Semi-inversion of guarded equations. In: Gl\u00fcck, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol.\u00a03676, pp. 189\u2013204. Springer, Heidelberg (2005)"},{"key":"21_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/1328408.1328413","volume-title":"Proc. of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation","author":"T.\u00c6. Mogensen","year":"2008","unstructured":"Mogensen, T.\u00c6.: Semi-inversion of functional parameters. In: Proc. of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 21\u201329. ACM Press, New York (2008)"},{"unstructured":"Nishida, N.: Transformational Approach to Inverse Computation in Term Rewriting. Doctor thesis, Nagoya University, Nagoya, Japan (2004), \n                      \n                        http:\/\/www.trs.cm.is.nagoya-u.ac.jp\/~nishida\/papers\/","key":"21_CR17"},{"doi-asserted-by":"crossref","unstructured":"Nishida, N., Sakai, M.: Completion after program inversion of injective functions. Postproceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming. ENTCS, vol. 237, pp. 39\u201356 (2009)","key":"21_CR18","DOI":"10.1016\/j.entcs.2009.03.034"},{"unstructured":"Nishida, N., Sakai, M., Kato, T.: Convergent term rewriting systems for inverse computation of injective functions. In: Proc. of the 9th International Workshop on Termination (WST 2007), pp. 77\u201381 (2007), \n                      \n                        http:\/\/www.trs.cm.is.nagoya-u.ac.jp\/~nishida\/papers\/","key":"21_CR19"},{"issue":"243","key":"21_CR20","first-page":"25","volume":"104","author":"N. Nishida","year":"2004","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: On simulation-completeness of unraveling for conditional term rewriting systems. IEICE Technical Report SS2004-18, the Institute of Electronics, Information and Communication Engineers (IEICE)\u00a0104(243), 25\u201330 (2004)","journal-title":"IEICE Technical Report SS2004-18, the Institute of Electronics, Information and Communication Engineers (IEICE)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/978-3-540-32033-3_20","volume-title":"Term Rewriting and Applications","author":"N. Nishida","year":"2005","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Partial inversion of constructor term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 264\u2013278. Springer, Heidelberg (2005)"},{"unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Generation of inverse computation programs of constructor term rewriting systems. The IEICE Transactions on Information and Systems\u00a0J88-D-I(8), 1171\u20131183 (2005); in Japanese, see [17]","key":"21_CR22"},{"issue":"1-2","key":"21_CR23","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s002000100064","volume":"12","author":"E. Ohlebusch","year":"2001","unstructured":"Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing\u00a012(1-2), 73\u2013116 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"21_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)"},{"key":"21_CR25","first-page":"273","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"D.A. Plaisted","year":"1993","unstructured":"Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a01, pp. 273\u2013364. Oxford University Press, Oxford (1993)"},{"key":"21_CR26","series-title":"SIGPLAN Notices","first-page":"12","volume-title":"Proc. of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation","author":"A. Romanenko","year":"1991","unstructured":"Romanenko, A.: Inversion and metacomputation. In: Proc. of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices, vol.\u00a026, pp. 12\u201322. ACM Press, New York (1991)"},{"unstructured":"Schernhammer, F., Gramlich, B.: On proving and characterizing operational termination of deterministic conditional rewrite systems. In: Proc. of the 9th International Workshop on Termination (WST 2007), pp. 82\u201385 (2007)","key":"21_CR27"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/11805618_3","volume-title":"Term Rewriting and Applications","author":"T.F. \u015eerb\u0103nu\u0163\u0103","year":"2006","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: Computationally equivalent elimination of conditions. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 19\u201334. Springer, Heidelberg (2006)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11805618_22","volume-title":"Term Rewriting and Applications","author":"I. Wehrman","year":"2006","unstructured":"Wehrman, I., Stump, A., Westbrook, E.M.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 287\u2013296. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:06:43Z","timestamp":1619784403000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}