{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:22Z","timestamp":1762458862587,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_20","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"264-278","source":"Crossref","is-referenced-by-count":23,"title":["Partial Inversion of Constructor Term Rewriting Systems"],"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"}]},{"given":"Toshiki","family":"Sakabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/10722010_13","volume-title":"Mathematics of Program Construction","author":"S. Abramov","year":"2000","unstructured":"Abramov, S., Gl\u00fcck, R.: The universal resolving algorithm: Inverse computation in a functional language. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 187\u2013212. Springer, Heidelberg (2000)"},{"key":"20_CR2","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, Cambridge (1998)"},{"key":"20_CR3","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)"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/1014007.1014022","volume-title":"Proceedings of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation","author":"F. Dur\u00e1n","year":"2004","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving termination of membership equational programs. In: Proceedings of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, pp. 147\u2013158. ACM Press, New York (2004)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-40018-9_17","volume-title":"Programming Languages and Systems","author":"R. Gl\u00fcck","year":"2003","unstructured":"Gl\u00fcck, R., Kawabe, M.: A program inverter for a functional language with equality and constructors. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol.\u00a02895, pp. 246\u2013264. Springer, Heidelberg (2003)"},{"key":"20_CR7","first-page":"153","volume-title":"Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation","author":"P.G. Harrison","year":"1988","unstructured":"Harrison, P.G.: Function inversion. In: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, pp. 153\u2013166. North-Holland, Amsterdam (1988)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-44881-0_22","volume-title":"Rewriting Techniques and Applications","author":"N. Hirokawa","year":"2003","unstructured":"Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 311\u2013320. Springer, Heidelberg (2003)"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1145\/1014007.1014025","volume-title":"Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation","author":"Z. Hu","year":"2004","unstructured":"Hu, Z., Mu, S.-C., Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pp. 178\u2013189. ACM Press, New York (2004)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1007\/3-540-51081-8_139","volume-title":"Rewriting Techniques and Applications","author":"H. Khoshnevisan","year":"1989","unstructured":"Khoshnevisan, H., Sephton, K.M.: InvX: An automatic function inverter. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 564\u2013568. Springer, Heidelberg (1989)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming\u00a0(1), 1\u201361 (1998)","DOI":"10.1142\/9789814528849"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-25979-4_14","volume-title":"Rewriting Techniques and Applications","author":"S. Lucas","year":"2004","unstructured":"Lucas, S.: mu-term: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 200\u2013209. Springer, Heidelberg (2004)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-61735-3_7","volume-title":"Algebraic and Logic Programming","author":"M. Marchiori","year":"1996","unstructured":"Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodr\u00edguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol.\u00a01139, pp. 107\u2013121. Springer, Heidelberg (1996)"},{"key":"20_CR15","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Generation of inverse term rewriting systems for pure treeless functions. In: Proceedings of the International Workshop on Rewriting in Proof and Computation, Sendai, Japan, pp. 188\u2013198 (2001)"},{"key":"20_CR16","series-title":"ENTCS","first-page":"18","volume-title":"Functional and Constraint Logic Programming","author":"N. Nishida","year":"2003","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables and its termination proof. In: Functional and Constraint Logic Programming. ENTCS, vol.\u00a086(3), p. 18. Elsevier, Amsterdam (2003)"},{"key":"20_CR17","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: On simulation-completeness of unraveling for conditional term rewriting systems. Technical Report SS 2004-18 of IEICE, 25\u201330 (2004)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Partial inversion of constructor term rewriting systems. Full version of this paper including the proofs of theorems (2005), Available from http:\/\/www.sakabe.i.is.nagoya-u.ac.jp\/~nishida\/papers\/","DOI":"10.1007\/978-3-540-32033-3_20"},{"key":"20_CR19","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, 73\u2013116 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"20_CR20","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":"20_CR21","unstructured":"Okamoto, K., Sakai, M., Sakabe, T.: Completeness of innermost strategy for inside- LR-joinable right-linear terminating TRSs. In: Record of 2003 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers. (2003) 564 (in Japanese). This is an extended result of [23], and the English version of this paper is available from, http:\/\/www.sakabe.i.is.nagoya-u.ac.jp\/~sakai\/papers\/"},{"key":"20_CR22","series-title":"SIGPLAN Notices","first-page":"12","volume-title":"Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation.","author":"A. Romanenko","year":"1991","unstructured":"Romanenko, A.: Inversion and metacomputation. In: Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices, vol.\u00a026, pp. 12\u201322. ACM Press, New York (1991)"},{"key":"20_CR23","unstructured":"Sakai, M., Okamoto, K., Sakabe, T.: Innermost reductions find all normal forms on right-linear terminating overlay TRSs. In: Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain, pp. 79\u201388 (2003)"},{"key":"20_CR24","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1145\/503032.503036","volume-title":"Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation","author":"J.P. Secher","year":"2002","unstructured":"Secher, J.P., S\u00f8rensen, M.H.: From checking to inference via driving and dag grammars. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices, vol.\u00a037, pp. 41\u201351. ACM, New York (2002)"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/3-540-19242-5_17","volume-title":"Conditional Term Rewriting Systems","author":"Y. Toyama","year":"1988","unstructured":"Toyama, Y.: Confluent term rewriting systems with membership conditions. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol.\u00a0308, pp. 228\u2013241. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T03:02:32Z","timestamp":1740538952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}