{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:42Z","timestamp":1778914182736,"version":"3.51.4"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2008,4,26]],"date-time":"2008-04-26T00:00:00Z","timestamp":1209168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2008,6]]},"DOI":"10.1007\/s10990-008-9028-2","type":"journal-article","created":{"date-parts":[[2008,4,25]],"date-time":"2008-04-25T13:49:51Z","timestamp":1209131391000},"page":"59-88","source":"Crossref","is-referenced-by-count":44,"title":["Proving operational termination of membership equational programs"],"prefix":"10.1007","volume":"21","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,4,26]]},"reference":[{"key":"9028_CR1","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"285","author":"P. Borovansk\u00fd","year":"2002","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285, 155\u2013185 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9028_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"314","volume-title":"Proc. of 18th International Conference on Automated Deduction","author":"C. Borralleras","year":"2002","unstructured":"Borralleras, C., Lucas, S., Rubio, A.: Recursive path orderings can be context-sensitive. In: Voronkov,\u00a0A. (ed.) Proc. of 18th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol.\u00a02392, pp.\u00a0314\u2013331. Springer, Berlin (2002)"},{"key":"9028_CR3","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236, 35\u2013132 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9028_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-45061-0_22","volume-title":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming","author":"R. Bruni","year":"2003","unstructured":"Bruni, R., Meseguer, J.: Generalized rewrite theories. In: Baeten, J., Lenstra, J., Parrow, J. (eds.) Proceedings of the 30th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol.\u00a02719, pp.\u00a0252\u2013266. Springer, Berlin (2003)"},{"issue":"2","key":"9028_CR5","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9028_CR6","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version\u00a02.2). December 2005, http:\/\/maude.cs.uiuc.edu"},{"key":"9028_CR7","unstructured":"CoFI Task Group on Semantics. CASL\u2014The common algebraic specification language, version\u00a01.0, Semantics. http:\/\/www.brics.dk\/Projects\/CoFI\/Documents\/CASL\/Semantics\/index.html (1999)"},{"key":"9028_CR8","unstructured":"Contejean, E., March\u00e9, C., Monate, B., Urbain, X.: Proving termination of rewriting with CiME. In: Rubio,\u00a0A. (ed.) Proc. WST\u201903 (2003). http:\/\/cime.lri.fr"},{"key":"9028_CR9","first-page":"147","volume-title":"Proc. of ACM SIGPLAN 2004 Symposium PEPM\u201904","author":"F. Dur\u00e1n","year":"2004","unstructured":"Dur\u00e1n, F., Lucas, S., March\u00e9, C., Meseguer, J., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium PEPM\u201904, pp.\u00a0147\u2013158. Assoc. Comput. Mach., New York (2004)"},{"key":"9028_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/3-540-48685-2_24","volume-title":"Proc. RTA\u201999","author":"M.C.F. Ferreira","year":"1999","unstructured":"Ferreira, M.C.F., Ribeiro, A.L.: Context-sensitive AC-rewriting. In: Narendran, P., Rusinowitch, M. (eds.) Proc. RTA\u201999, Trento, Italy. Lecture Notes in Computer Science, vol.\u00a01631, pp.\u00a0286\u2013300. Springer, Berlin (1999)"},{"key":"9028_CR11","volume-title":"Proc. PPDP\u201902","author":"O. Fissore","year":"2002","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Cariboo: An induction based proof tool for termination with strategies. In: Kirchner, C. (ed.) Proc. PPDP\u201902, Pittsburgh, USA. Assoc. Comput. Mach., New York (2002)"},{"key":"9028_CR12","series-title":"AMAST Series","volume-title":"CafeOBJ Report","author":"K. Futatsugi","year":"1998","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series World Scientific, Singapore (1998)"},{"key":"9028_CR13","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39\u201372 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"2","key":"9028_CR14","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. J.\u00a0Symb. Comput. 34(2), 21\u201358 (2002)","journal-title":"J.\u00a0Symb. Comput."},{"key":"9028_CR15","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1017\/S0956796803004945","volume":"14","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Middeldorp, A.: Transformation techniques for context-sensitive rewrite systems. J.\u00a0Funct. Program. 14, 379\u2013427 (2004)","journal-title":"J.\u00a0Funct. Program."},{"key":"9028_CR16","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Proc. of 5th International Workshop on Frontiers of Combining Systems, FroCoS\u201905","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) Proc. of 5th International Workshop on Frontiers of Combining Systems, FroCoS\u201905, Vienna, Austria, vol.\u00a03717, pp.\u00a0216\u2013231. Springer, Berlin (2005)"},{"key":"9028_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: AProVE: A system for proving termination. In: van\u00a0Oostrom, V. (ed.) Rewriting Techniques and Applications. Lecture Notes in Computer Science. Springer, Berlin (2004). http:\/\/www-i2.informatik.rwth-aachen.de\/AProVE"},{"key":"9028_CR18","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J. Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra\u00a0I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"9028_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-6541-0","volume-title":"Software Engineering with OBJ: Algebraic Specification in Action","author":"J. Goguen","year":"2000","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer Academic, Dordrecht (2000)"},{"key":"9028_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-32033-3_14","volume-title":"Proc. RTA\u201905","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) Proc. RTA\u201905, Nara, Japan. Lecture Notes in Computer Science, vol.\u00a03467, pp.\u00a0175\u2013184. Springer, Berlin (2005)"},{"key":"9028_CR21","first-page":"1","volume":"27","author":"P. Hudak","year":"1992","unstructured":"Hudak, P., Peyton-Jones, S., Wadler, P.: Report on the functional programming language Haskell: a\u00a0non-strict, purely functional language. SIGPLAN Not. 27, 1\u2013164 (1992)","journal-title":"SIGPLAN Not."},{"key":"9028_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-61440-0_122","volume-title":"Proc. of ICALP\u201996","author":"S. Lucas","year":"1996","unstructured":"Lucas, S.: Termination of context-sensitive rewriting by rewriting. In: auf der Heide, F.M., Monien, B. (eds.) Proc. of ICALP\u201996. Lecture Notes in Computer Science, vol.\u00a01099, pp.\u00a0122\u2013133. Springer, Berlin (1996)"},{"key":"9028_CR23","unstructured":"Lucas, S.: Context-sensitive computations in functional and functional logic programs. J.\u00a0Funct. Logic Program. 1998(1) (1998)"},{"issue":"1","key":"9028_CR24","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1016\/S0890-5401(02)93176-7","volume":"178","author":"S. Lucas","year":"2002","unstructured":"Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294\u2013343 (2002)","journal-title":"Inf. Comput."},{"key":"9028_CR25","unstructured":"Lucas, S.: Termination of programs with strategy annotations. Technical Report DSIC-II\/20\/03, DSIC, Universidad Polit\u00e9cnica de Valencia (2003)"},{"key":"9028_CR26","series-title":"Lecture Notes in Computer Science","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\u00a0Oostrom,\u00a0V. (ed.) Rewriting Techniques and Applications. Lecture Notes in Computer Science. Springer, Berlin (2004). http:\/\/www.dsic.upv.es\/~slucas\/csr\/termination\/muterm\/"},{"key":"9028_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/978-3-540-24727-2_23","volume-title":"Proc. FOSSACS\u201904","author":"S. Lucas","year":"2004","unstructured":"Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) Proc. FOSSACS\u201904. Lecture Notes in Computer Science, vol.\u00a02987, pp.\u00a0318\u2013332. Springer, Berlin (2004)"},{"issue":"12","key":"9028_CR28","doi-asserted-by":"crossref","first-page":"1782","DOI":"10.1016\/j.ic.2006.07.001","volume":"204","author":"S. Lucas","year":"2006","unstructured":"Lucas, S.: Proving termination of context-sensitive rewriting by transformation. Inf. Comput. 204(12), 1782\u20131846 (2006)","journal-title":"Inf. Comput."},{"key":"9028_CR29","doi-asserted-by":"crossref","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. Inf. Process. Lett. 95, 446\u2013453 (2005)","journal-title":"Inf. Process. Lett."},{"key":"9028_CR30","doi-asserted-by":"crossref","first-page":"873","DOI":"10.1016\/j.jsc.2004.02.003","volume":"38","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Urbain, X.: Modular and incremental proofs of AC-termination. J.\u00a0Symb. Comput. 38, 873\u2013897 (2004)","journal-title":"J.\u00a0Symb. Comput."},{"key":"9028_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-61735-3_7","volume-title":"Proc. of ALP\u201996","author":"M. Marchiori","year":"1996","unstructured":"Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodr\u00edguez-Artalejo, M. (eds.) Proc. of ALP\u201996. Lecture Notes in Computer Science, vol.\u00a01039, pp.\u00a0107\u2013121. Springer, Berlin (1996)"},{"key":"9028_CR32","first-page":"275","volume-title":"Logic Colloquium\u201987","author":"J. Meseguer","year":"1989","unstructured":"Meseguer, J.: General logics. In: Logic Colloquium\u201987, pp.\u00a0275\u2013329. North-Holland, Amsterdam (1989)"},{"key":"9028_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Proceedings WADT\u201997","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) Proceedings WADT\u201997. Lecture Notes in Computer Science, vol.\u00a01376, pp.\u00a018\u201361. Springer, Berlin (1998)"},{"key":"9028_CR34","first-page":"459","volume-title":"Algebraic Methods in Semantics","author":"J. Meseguer","year":"1985","unstructured":"Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, pp.\u00a0459\u2013541. Cambridge University Press, Cambridge (1985)"},{"key":"9028_CR35","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, Berlin (2002)"},{"issue":"4","key":"9028_CR36","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0020-0190(02)00272-7","volume":"84","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Hierarchical termination revisited. Inf. Process. Lett. 84(4), 207\u2013214 (2002)","journal-title":"Inf. Process. Lett."},{"key":"9028_CR37","series-title":"Lecture Notes in Artificial Intelligence","first-page":"485","volume-title":"Proc. IJCAR\u201901","author":"X. Urbain","year":"2001","unstructured":"Urbain, X.: Automated incremental termination proofs for hierarchically defined term rewriting systems. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Proc. IJCAR\u201901, Siena, Italy. Lecture Notes in Artificial Intelligence, vol.\u00a02083, pp.\u00a0485\u2013498. Springer, Berlin (2001)"},{"key":"9028_CR38","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF03177743","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain, X.: Modular and incremental automated termination proofs. J.\u00a0Automat. Reason. 32, 315\u2013355 (2004)","journal-title":"J.\u00a0Automat. Reason."},{"key":"9028_CR39","doi-asserted-by":"crossref","DOI":"10.1142\/3163","volume-title":"Language Prototyping: An\u00a0Algebraic Specification Approach","author":"A. Deursen van","year":"1996","unstructured":"van Deursen, A., Heering, J., Klint, P.: Language Prototyping: An\u00a0Algebraic Specification Approach. World Scientific, Singapore (1996)"},{"key":"9028_CR40","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9028_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-62950-5_69","volume-title":"Proc. RTA\u201997","author":"H. Zantema","year":"1997","unstructured":"Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) Proc. RTA\u201997, Sitges, Spain. Lecture Notes in Computer Science, vol.\u00a01232, pp.\u00a0172\u2013186. Springer, Berlin (1997)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-008-9028-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-008-9028-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-008-9028-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-008-9028-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,4,26]]},"references-count":41,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["9028"],"URL":"https:\/\/doi.org\/10.1007\/s10990-008-9028-2","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,4,26]]}}}