{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:12Z","timestamp":1762458552237},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540734475"},{"type":"electronic","value":"9783540734499"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73449-9_18","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T16:49:53Z","timestamp":1187023793000},"page":"229-245","source":"Crossref","is-referenced-by-count":8,"title":["On the Completeness of Context-Sensitive Order-Sorted Specifications"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hendrix","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Boudol, G.: Computational semantics of term rewriting systems. Algebraic methods in semantics, 169\u2013236 (1986)"},{"key":"18_CR2","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude. LNCS. vol. 4350, Springer, Heidelberg (to appear, 2007)"},{"issue":"1","key":"18_CR3","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(91)90040-9","volume":"83","author":"N. Dershowitz","year":"1991","unstructured":"Dershowitz, N., Kaplan, S., Plaisted, D.A.: Rewrite, rewrite, rewrite, rewrite, rewrite, .... Theor. Comput. Sci.\u00a083(1), 71\u201396 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/1014007.1014022","volume-title":"Proc.\u00a0of PEPM","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: Proc.\u00a0of PEPM, pp. 147\u2013158. ACM, New York (2004)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series (1998)","DOI":"10.1142\/3831"},{"key":"18_CR6","first-page":"52","volume-title":"Proc. of POPL 1985","author":"K. Futatsugi","year":"1985","unstructured":"Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proc. of POPL 1985, pp. 52\u201366. ACM, New York (1985)"},{"issue":"4","key":"18_CR7","doi-asserted-by":"publisher","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.\u00a0Program\u00a014(4), 379\u2013427 (2004)","journal-title":"J.\u00a0Funct.\u00a0Program"},{"key":"18_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"18_CR9","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1017\/S0960129500000517","volume":"4","author":"J. Goguen","year":"1994","unstructured":"Goguen, J., Diaconescu, R.: An oxford survey of order sorted algebra. Mathematical Structures in Computer Science\u00a04(3), 363\u2013392 (1994)","journal-title":"Mathematical Structures in Computer Science"},{"key":"18_CR10","unstructured":"Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. Technical Report UIUCDCS-R-2007-2812, University of Illinois (2007), Available at http:\/\/maude.cs.uiuc.edu\/tools\/scc\/"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Proc.\u00a0of IJCAR","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: IJCAR 2006. LNCS, vol.\u00a04130, pp. 151\u2013155. Springer, Heidelberg (2006)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","first-page":"165","volume-title":"Proc. of RTA 2006","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: RTA 2006. LNCS, vol.\u00a04098, pp. 165\u2013174. Springer, Heidelberg (2006)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1007\/11814771_45","volume-title":"Proc.\u00a0of IJCAR","author":"F. Jacquemard","year":"2006","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. In: IJCAR 2006. LNCS, vol.\u00a04130, pp. 557\u2013571. Springer, Heidelberg (2006)"},{"key":"18_CR14","unstructured":"Lucas, S.: Context-sensitive computations in functionnal and functional logic programs. Journal of Functional and Logic Programming, 1998(1) (1998)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-45127-7_17","volume-title":"Rewriting Techniques and Applications","author":"S. Lucas","year":"2001","unstructured":"Lucas, S.: Transfinite rewriting semantics for term rewriting systems. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 216\u2013230. Springer, Heidelberg (2001)"},{"issue":"1","key":"18_CR16","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. Information and Computation\u00a0178(1), 294\u2013343 (2002)","journal-title":"Information and Computation"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"12","key":"18_CR18","doi-asserted-by":"publisher","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. Information and Computation\u00a0204(12), 1782\u20131846 (2006)","journal-title":"Information and Computation"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/3-540-44802-0_38","volume-title":"Computer Science Logic","author":"H. Ohsaki","year":"2001","unstructured":"Ohsaki, H.: Beyond regularity: Equational tree automata for associative and commutative theories. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 539\u2013553. Springer, Heidelberg (2001)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-44881-0_14","volume-title":"Rewriting Techniques and Applications","author":"K.N. Verma","year":"2003","unstructured":"Verma, K.N.: Two-way equational tree automata for AC-like theories: Decidability and closure properties. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 180\u2013196. Springer, Heidelberg (2003)"},{"key":"18_CR22","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. of RTA 1997","author":"H. Zantema","year":"1997","unstructured":"Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) Proc. of RTA 1997. LNCS, vol.\u00a01232, pp. 172\u2013186. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73449-9_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T19:36:54Z","timestamp":1684006614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73449-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540734475","9783540734499"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73449-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}