{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215904},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668565"},{"type":"electronic","value":"9783540466741"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_16","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"177-189","source":"Crossref","is-referenced-by-count":1,"title":["On Automating Inductive and Non-inductive Termination Methods"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Monin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail in Proceeding TAPSOFT\u201997, LNCS, volume 1214, 261\u2013272.","DOI":"10.1007\/BFb0030602"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Proving innermost normalisation automatically in Proceeding RTA\u201997, LNCS, volume 1232, 157\u2013171.","DOI":"10.1007\/3-540-62950-5_68"},{"issue":"2","key":"16_CR3","first-page":"137","volume":"9","author":"A. Cherifa Ben","year":"1987","unstructured":"A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9(2),137\u2013159, 1987.","journal-title":"Termination of rewriting systems by polynomial interpretations and its implementation"},{"key":"16_CR4","unstructured":"C. Cornes et al.. The Coq proof assistant reference manual version 5.10. Technical Report 077, INRIA, 1995."},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Termination of rewriting. Theoretical Computer Science 17, 279\u2013301,1982.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"16_CR6","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"N. Dershowitz and C. Hoot. Natural termination. Theoretical Computer Science142(2), 179\u2013207, 1995.","journal-title":"Theoretical Computer Science"},{"key":"16_CR7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF01237233","volume":"28","author":"J. Dick","year":"1990","unstructured":"J. Dick, J. Kalmus and U. Martin. Automating the Knuth Bendix ordering. Acta Informatica 28, 95\u2013119, 1990.","journal-title":"Acta Informatica"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BFb0030601","volume":"1214","author":"T. Genet","year":"1997","unstructured":"T. Genet and I. Gnaedig. Termination proofs using gpo ordering constraints. TAP-SOFT, LNCS 1214, 249\u2013260, 1997.","journal-title":"TAP-SOFT"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"J. Giesl. Generating polynomial orderings for termination proofs. Proceedings of the 6th International Conference on Rewriting Techniques and Application, Kaiserlautern, LNCS, volume 914, 1995.","DOI":"10.1007\/3-540-59200-8_77"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and F. Monin. On formalised proofs of termination of recursive functions. In Proc. International Conference on Principles and Practice of Declar-ative Programming, Paris, France, 1999.","DOI":"10.1007\/10704567_2"},{"key":"16_CR11","unstructured":"F. Kamareddine and F. Monin. Induction Lemmas for Termination of Recursive Functions in a Typed System Proc. submitted."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational problems in abstract algebra, Pergamon Press, 263\u2013297,1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"16_CR13","unstructured":"T. Kolbe. Challenge problems for automated termination proofs of term rewriting systems. Technical Report IBN96-42, Technische Hochshule Darmstadt, Alexanderstr.10, 64283 Darmstadt, Germany, 1996."},{"issue":"1","key":"16_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00302640","volume":"6","author":"P. Lescanne","year":"1990","unstructured":"P. Lescanne. On the recursive decomposition ordering with lexicographical status and other related orderings. Journal of Automated Reasoning 6(1) 39\u201349, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"P. Manoury. A User\u2019s friendly syntax to define recursive functions as typed lambda-terms. Proceedings of Type for Proofs and Programs TYPES\u201994, LNCS, volume 996,1994.","DOI":"10.1007\/3-540-60579-7_5"},{"key":"16_CR16","unstructured":"P. Manoury and M. Simonot. Des preuves de totalit_e de fonctions comme synth_ese de programmes. PhD thesis, University Paris 7, 1992."},{"issue":"2","key":"16_CR17","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","volume":"135","author":"P. Manoury","year":"1994","unstructured":"P. Manoury and M. Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science 135(2) 319\u2013343, 1994.","journal-title":"Theoretical Computer Science"},{"key":"16_CR18","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0304-3975(96)00172-7","volume":"175","author":"A. Middeldorp","year":"1997","unstructured":"A. Middeldorp and H. Zantema. Simple termination of rewrite systems. Theoretical Computer Science 175, 127\u2013158, 1997.","journal-title":"Theoretical Computer Science"},{"key":"16_CR19","unstructured":"F. Monin and M. Simonot. An ordinal measure based procedure for termination of functions. To appear in Theoretical Computer Science."},{"issue":"2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"M. Parigot. Recursive programming with proofs. Theoretical Computer Science94(2) 335\u2013356, 1992.","journal-title":"Theoretical Computer Science"},{"key":"16_CR21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"J. Steinbach","year":"1994","unstructured":"J. Steinbach. Generating polynomial orderings. Information Processing Letters 49,85\u201393, 1994.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T08:56:35Z","timestamp":1557046595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}