{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T15:05:55Z","timestamp":1725635155167},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221531"},{"type":"electronic","value":"9783540259794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25979-4_19","type":"book-chapter","created":{"date-parts":[[2010,9,10]],"date-time":"2010-09-10T21:32:53Z","timestamp":1284154373000},"page":"269-284","source":"Crossref","is-referenced-by-count":1,"title":["Inductive Theorems for Higher-Order Rewriting"],"prefix":"10.1007","author":[{"given":"Takahito","family":"Aoto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiyuki","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoshihito","family":"Toyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"SIG 4 PRO 17","key":"19_CR1","first-page":"67","volume":"44","author":"T. Aoto","year":"2003","unstructured":"Aoto, T., Yamada, T.: Proving termination of simply typed term rewriting systems automatically. IPSJ Transactions on Programming\u00a044(SIG 4 PRO 17), 67\u201377 (2003) (in Japanese)","journal-title":"IPSJ Transactions on Programming"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-44881-0_27","volume-title":"Rewriting Techniques and Applications","author":"T. Aoto","year":"2003","unstructured":"Aoto, T., Yamada, T.: Termination of simply typed term rewriting systems by translation and labelling. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 380\u2013394. Springer, Heidelberg (2003)"},{"key":"19_CR3","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3923\/itj.2003.21.24","volume":"2","author":"T. Aoto","year":"2003","unstructured":"Aoto, T., Yamada, T., Toyama, Y.: Proving inductive theorems of higher-order functional programs. Information Technology Letters\u00a02, 21\u201322 (2003) (in Japanese)","journal-title":"Information Technology Letters"},{"key":"19_CR4","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)"},{"issue":"2","key":"19_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G., Hullot, J.-M.: Proof by induction in equational theories with constructors. Journal of Computer and System Sciences\u00a025(2), 239\u2013266 (1982)","journal-title":"Journal of Computer and System Sciences"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/LICS.1991.151659","volume-title":"Proceedings of the 6th IEEE Symposium on Logic in Computer Science","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: Executable higher-order algebraic specification languages. In: Proceedings of the 6th IEEE Symposium on Logic in Computer Science, pp. 350\u2013361. IEEE Press, Los Alamitos (1991)"},{"issue":"4","key":"19_CR7","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica\u00a024(4), 395\u2013415 (1987)","journal-title":"Acta Informatica"},{"issue":"1\u20132","key":"19_CR8","first-page":"81","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation\u00a011(1\u20132), 81\u2013111 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR9","unstructured":"Klop, J.W.: Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit, Utrecht (1980)"},{"issue":"6","key":"19_CR10","first-page":"1","volume":"17","author":"H. Koike","year":"2000","unstructured":"Koike, H., Toyama, Y.: Inductionless induction and rewriting induction. Comptuter Software\u00a017(6), 1\u201312 (2000) (in Japanese)","journal-title":"Comptuter Software"},{"issue":"SIG 7 PRO 11","key":"19_CR11","first-page":"35","volume":"42","author":"K. Kusakari","year":"2001","unstructured":"Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. IPSJ Transactions on Programming\u00a042(SIG 7 PRO 11), 35\u201345 (2001)","journal-title":"IPSJ Transactions on Programming"},{"key":"19_CR12","unstructured":"Kusakari, K.: Inductive theorems in SRS (2003) (manuscript) (in Japanese)"},{"key":"19_CR13","unstructured":"Kusakari, K., Sakai, M., Sakabe, T.: Characterizing inductive theorems by extensional initial models in a higher-order equational logic. Distributed at IPSJ seminar PRO\u20132003\u20133 (2003)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-62034-6_56","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"H. Linnestad","year":"1996","unstructured":"Linnestad, H., Prehofer, C., Lysne, O.: Higher-order proof by consistency. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol.\u00a01180, pp. 274\u2013285. Springer, Heidelberg (1996)"},{"issue":"1","key":"19_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science\u00a0192(1), 3\u201329 (1998)","journal-title":"Theoretical Computer Science"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/3-540-61254-8_23","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"K. Meinke","year":"1996","unstructured":"Meinke, K.: Higher-order equational logic for specification, simulation and testing. In: Dowek, G., Heering, J., Meinke, K., M\u00f6ller, B. (eds.) HOA 1995. LNCS, vol.\u00a01074, pp. 124\u2013143. Springer, Heidelberg (1996)"},{"key":"19_CR17","first-page":"154","volume-title":"Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages","author":"D.R. Musser","year":"1980","unstructured":"Musser, D.R.: On proving inductive properties of abstract data types. In: Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pp. 154\u2013162. ACM Press, New York (1980)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0036486","volume-title":"Theoretical Computer Science","author":"T. Nipkow","year":"1983","unstructured":"Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol.\u00a0145, pp. 257\u2013267. Springer, Heidelberg (1983)"},{"key":"19_CR19","unstructured":"Terese.: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"issue":"2","key":"19_CR20","first-page":"369","volume":"90","author":"Y. Toyama","year":"1991","unstructured":"Toyama, Y.: How to prove equivalence of term rewriting systems without induction. Theoretical Computer Science\u00a090(2), 369\u2013390 (1991)","journal-title":"Theoretical Computer Science"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-45127-7_25","volume-title":"Rewriting Techniques and Applications","author":"T. Yamada","year":"2001","unstructured":"Yamada, T.: Confluence and termination of simply typed term rewriting systems. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 338\u2013352. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25979-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T06:15:33Z","timestamp":1553062533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25979-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221531","9783540259794"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25979-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}