{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:03Z","timestamp":1762458543467},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_8","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:28:09Z","timestamp":1184603289000},"page":"111-130","source":"Crossref","is-referenced-by-count":5,"title":["Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems"],"prefix":"10.1007","author":[{"given":"Enno","family":"Ohlebusch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BFb0030602","volume-title":"Proceedings of the 22nd International Colloquium on Trees in Algebra and Programming","author":"T. Arts","year":"1997","unstructured":"T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In Proceedings of the 22nd International Colloquium on Trees in Algebra and Programming, volume 1214 of Lecture Notes in Computer Science, pages 261\u2013272, Berlin, 1997. Springer-Verlag."},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-62950-5_68","volume-title":"Proceedings of the 8th International Conference on Rewriting Techniques and Applications","author":"T. Arts","year":"1997","unstructured":"T. Arts and J. Giesl. Proving innermost normalisation automatically. In Proceedings of the 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 157\u2013172, Berlin, 1997. Springer-Verlag."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"J. Avenhaus and C. Lor\u00eda-S\u00e1enz. On conditional rewrite systems with extra variables and deterministic logic programs. In Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, volume 822 of Lecture Notes in Artificial Intelligence, pages 215\u2013229, Berlin, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58216-9_40"},{"key":"8_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-57529-4_47","volume-title":"Proceedings of the 13th Conference on the Foundations of Software Technology and Theoretical Computer Science","author":"G. Aguzzi","year":"1993","unstructured":"G. Aguzzi and U. Modigliani. Proving termination of logic programs by transforming them into equivalent term rewriting systems. In Proceedings of the 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 761 of Lecture Notes in Computer Science, pages 114\u2013124, Berlin, 1993. Springer-Verlag."},{"key":"8_CR5","unstructured":"T. Arts. Automatically Proving Termination and Innermost Normalisation of Term Rewriting Systems. PhD thesis, Utrecht University, 1997."},{"key":"8_CR6","unstructured":"T. Arts and H. Zantema. Termination of logic programs via labelled term rewrite systems. In Proceedings of Computing Science in the Netherlands, pages 22\u201334, 1995."},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-60939-3_17","volume-title":"Proceedings of the 5th International Workshop on Logic Program Synthesis and Transformation","author":"T. Arts","year":"1996","unstructured":"T. Arts and H. Zantema. Termination of logic programs using semantic unification. In Proceedings of the 5th International Workshop on Logic Program Synthesis and Transformation, volume 1048 of Lecture Notes in Computer Science, pages 219\u2013233, Berlin, 1996. Springer-Verlag."},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/3-540-51081-8_99","volume-title":"Proceedings of the 3rd International Conference on Rewriting Techniques and Applications","author":"H. Bertling","year":"1989","unstructured":"H. Bertling and H. Ganzinger. Completion-time optimization of rewrite-time goal solving. In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 45\u201358, Berlin, 1989. Springer-Verlag."},{"issue":"3","key":"8_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J.A. Bergstra","year":"1986","unstructured":"J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323\u2013362, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"8_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012855","volume-title":"Proceedings of the 9th Conference on Automated Deduction","author":"N. Dershowitz","year":"1988","unstructured":"N. Dershowitz, M. Okada, and G. Sivakumar. Canonical conditional rewrite systems. In Proceedings of the 9th Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 538-549, Berlin, 1988. Springer-Verlag."},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(90)90105-Q","volume":"89","author":"H. Ganzinger","year":"1991","unstructured":"H. Ganzinger. Order-sorted completion: The many-sorted way. Theoretical Computer Science, 89:3\u201332, 1991.","journal-title":"Theoretical Computer Science"},{"key":"8_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/3-540-19242-5_8","volume-title":"Proceedings of the 1st International Workshop on Conditional and Typed Rewriting Systems","author":"E. Giovannetti","year":"1988","unstructured":"E. Giovannetti and C. Moiso. Notes on the elimination of conditions. In Proceedings of the 1st International Workshop on Conditional and Typed Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 91\u201397, Berlin, 1988. Springer-Verlag."},{"key":"8_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","volume":"24","author":"B. Gramlich","year":"1995","unstructured":"B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24:3\u201323, 1995.","journal-title":"Fundamenta Informaticae"},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","first-page":"113","volume-title":"Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"H. Ganzinger and U. Waldmann. Termination proofs of well-moded logic programs via conditional rewrite systems. In Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, volume 656 of Lecture Notes in Computer Science, pages 113\u2013127, Berlin, 1993. Springer-Verlag."},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19&20","author":"M. Hanus","year":"1994","unstructured":"M. Hanus. The integration of functions into logic programming: Prom theory to practice. The Journal of Logic Programming, 19&20:583\u2013628, 1994.","journal-title":"The Journal of Logic Programming"},{"key":"8_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/3-540-60381-6_11","volume-title":"Proceedings of the 4rd International Workshop on Conditional and Typed Rewriting Systems","author":"C. Hintermeier","year":"1995","unstructured":"C. Hintermeier. How to transform canonical decreasing CTRSs into equivalent canonical TRSs. In Proceedings of the 4rd International Workshop on Conditional and Typed Rewriting Systems, volume 968 of Lecture Notes in Computer Science, pages 186\u2013205, Berlin, 1995. Springer-Verlag."},{"key":"8_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/3-540-15975-4_37","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Johnsson","year":"1985","unstructured":"T. Johnsson. Lambda lifting: Transforming programs to recursive functions. In Functional Programming Languages and Computer Architecture, volume 201 of Lecture Notes in Computer Science, pages 190\u2013203, Berlin, 1985. Springer-Verlag."},{"key":"8_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BFb0023769","volume-title":"Proceedings of the 5th Workshop on Computer Science Logic","author":"M.R.K. Krishna Rao","year":"1992","unstructured":"M.R.K. Krishna Rao, D. Kapur, and R.K. Shyamasundar. A transformational methodology for proving termination of logic programs. In Proceedings of the 5th Workshop on Computer Science Logic, volume 626 of Lecture Notes in Computer Science, pages 213\u2013226, Berlin, 1992. Springer-Verlag."},{"issue":"1","key":"8_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(97)00028-9","volume":"34","author":"M.R.K. Krishna Rao","year":"1998","unstructured":"M.R.K. Krishna Rao, D. Kapur, and R.K. Shyamasundar. Transformational methodology for proving termination of logic programs. The Journal of Logic Programming, 34(1):1\u201342, 1998.","journal-title":"The Journal of Logic Programming"},{"key":"8_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-58431-5_16","volume-title":"Proceedings of the 4th International Conference on Algebraic and Logic Programming","author":"M. Marchiori","year":"1994","unstructured":"M. Marchiori. Logic programs as term rewriting systems. In Proceedings of the 4th International Conference on Algebraic and Logic Programming, volume 850 of Lecture Notes in Computer Science, pages 223\u2013241, Berlin, 1994. Springer-Verlag."},{"key":"8_CR22","series-title":"Technical Report","volume-title":"Unravelings and ultra-properties","author":"M. Marchiori","year":"1995","unstructured":"M. Marchiori. Unravelings and ultra-properties. Technical Report 8, Dept. of Pure and Applied Mathematics, University of Padova, Italy, 1995."},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-61735-3_7","volume-title":"Proceedings of the 5th International Conference on Algebraic and Logic Programming","author":"M. Marchiori","year":"1996","unstructured":"M. Marchiori. Unravelings and ultra-properties. In Proceedings of the 5th International Conference on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, pages 107\u2013121, Berlin, 1996. Springer-Verlag."},{"key":"8_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0058025","volume-title":"Proceedings of the 17th International Conference on the Foundations of Software Technology and Theoretical Computer Science","author":"M. Marchiori","year":"1997","unstructured":"M. Marchiori. On the expressive power of rewriting. In Proceedings of the 17th International Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1346 of Lecture Notes in Computer Science, pages 88\u2013102, Berlin, 1997. Springer-Verlag."},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jsco.1995.1036","volume":"20","author":"E. Ohlebusch","year":"1995","unstructured":"E. Ohlebusch. Modular properties of composable term rewriting systems. Journal of Symbolic Computation, 20:1\u201341, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"F. van Raamsdonk. Translating logic programs into conditional rewriting systems. In Proceedings of the 14th International Conference on Logic Programming, pages 168\u2013182. MIT Press, 1997.","DOI":"10.7551\/mitpress\/4299.003.0018"},{"key":"8_CR27","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0743-1066(94)90027-2","volume":"19&20","author":"D. Schreye de","year":"1994","unstructured":"D. de Schreye and S. Decorte. Termination of logic programs: The never-ending story. The Journal of Logic Programming, 19&20:199\u2013260, 1994.","journal-title":"The Journal of Logic Programming"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,16]],"date-time":"2024-02-16T18:48:00Z","timestamp":1708109280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}