1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Arts and Giesl}{Arts and
4: Giesl}{1996}]{Arts-Giesl-inner-tech-96}
5: {\sc Arts, T.} {\sc and} {\sc Giesl, J.} 1996.
6: \newblock Proving innermost normalization automatically.
7: \newblock Tech. Rep. 96/39, Technische Hochschule Darmstadt, Germany.
8:
9: \bibitem[\protect\citeauthoryear{Arts and Giesl}{Arts and
10: Giesl}{2000}]{Arts-Giesl-TCS-2000}
11: {\sc Arts, T.} {\sc and} {\sc Giesl, J.} 2000.
12: \newblock Termination of term rewriting using dependency pairs.
13: \newblock {\em Theoretical Computer Science\/}~{\em 236}, 133--178.
14:
15: \bibitem[\protect\citeauthoryear{Ben~Cherifa and Lescanne}{Ben~Cherifa and
16: Lescanne}{1987}]{Cherifa-Lescanne-SCP87}
17: {\sc Ben~Cherifa, A.} {\sc and} {\sc Lescanne, P.} 1987.
18: \newblock Termination of rewriting systems by polynomial interpretations and
19: its implementation.
20: \newblock {\em Science of Computer Programming\/}~{\em 9,\/}~2 (Oct.),
21: 137--160.
22:
23: \bibitem[\protect\citeauthoryear{Borelleras, Ferreira, and Rubio}{Borelleras
24: et~al\mbox{.}}{2000}]{BorFerRubio-SPO-CADE-2000}
25: {\sc Borelleras, C.}, {\sc Ferreira, M.}, {\sc and} {\sc Rubio, A.} 2000.
26: \newblock Complete monotonic semantic path orderings.
27: \newblock In {\em Proceedings of the 17th International Conference on Automated
28: Deduction}. Lecture Notes in Computer Science, vol. 1831. Springer-Verlag,
29: Pittsburgh, PA, USA, 346--364.
30:
31: \bibitem[\protect\citeauthoryear{Borovansk\'y, Kirchner, Kirchner, Moreau, and
32: Ringeissen}{Borovansk\'y et~al\mbox{.}}{1998}]{BorovanskyKKMR-WRLA98}
33: {\sc Borovansk\'y, P.}, {\sc Kirchner, C.}, {\sc Kirchner, H.}, {\sc Moreau,
34: P.-E.}, {\sc and} {\sc Ringeissen, C.} 1998.
35: \newblock {An Overview of {\sf ELAN}}.
36: \newblock In {\em {P}roceedings of the 2nd {I}nternational {W}orkshop on
37: {R}ewriting {L}ogic and its {A}pplications}, {C.~Kirchner} {and}
38: {H.~Kirchner}, Eds. Electronic Notes in Theoretical Computer Science.
39: Elsevier Science Publishers B. V. (North-Holland), Pont-{\`a}-Mousson
40: (France).
41:
42: \bibitem[\protect\citeauthoryear{Clavel, Eker, Lincoln, and Meseguer}{Clavel
43: et~al\mbox{.}}{1996}]{Maude-RwLg1996}
44: {\sc Clavel, M.}, {\sc Eker, S.}, {\sc Lincoln, P.}, {\sc and} {\sc Meseguer,
45: J.} 1996.
46: \newblock Principles of {Maude}.
47: \newblock In {\em Proceedings of the 1st International Workshop on Rewriting
48: Logic and its Applications}, {J.~Meseguer}, Ed. Electronic Notes in
49: Theoretical Computer Science, vol.~5. North Holland, Asilomar, Pacific Grove,
50: CA, USA.
51:
52: \bibitem[\protect\citeauthoryear{Comon}{Comon}{1991}]{Comon-rob91}
53: {\sc Comon, H.} 1991.
54: \newblock Disunification: a survey.
55: \newblock In {\em Computational {L}ogic. {E}ssays in honor of {A}lan
56: {R}obinson}, {J.-L. Lassez} {and} {G.~Plotkin}, Eds. The MIT press, Cambridge
57: (MA, USA), Chapter~9, 322--359.
58:
59: \bibitem[\protect\citeauthoryear{Dershowitz}{Dershowitz}{1982}]{DershowitzTCS-%
60: 1982}
61: {\sc Dershowitz, N.} 1982.
62: \newblock Orderings for term rewriting systems.
63: \newblock {\em Theoretical Computer Science\/}~{\em 17}, 279--301.
64:
65: \bibitem[\protect\citeauthoryear{Dershowitz and Hoot}{Dershowitz and
66: Hoot}{1995}]{Dershowitz-Hoot-1995}
67: {\sc Dershowitz, N.} {\sc and} {\sc Hoot, C.} 1995.
68: \newblock Natural termination.
69: \newblock {\em Theoretical Computer Science\/}~{\em 142(2)}, 179--207.
70:
71: \bibitem[\protect\citeauthoryear{Dershowitz and Jouannaud}{Dershowitz and
72: Jouannaud}{1990}]{DershowitzJ-1989}
73: {\sc Dershowitz, N.} {\sc and} {\sc Jouannaud, J.-P.} 1990.
74: \newblock {\em Handbook of Theoretical Computer Science}. Vol.~B.
75: \newblock Elsevier Science Publishers B. V. (North-Holland), Chapter 6:
76: {R}ewrite {S}ystems, 244--320.
77: \newblock Also as: Research report 478, LRI.
78:
79: \bibitem[\protect\citeauthoryear{Eker}{Eker}{1998}]{Eker98}
80: {\sc Eker, S.} 1998.
81: \newblock Term rewriting with operator evaluation strategies.
82: \newblock In {\em Proceedings of the 2nd International Workshop on Rewriting
83: Logic and its Applications}, {C.~Kirchner} {and} {H.~Kirchner}, Eds.
84: Pont-\`a-Mousson (France).
85:
86: \bibitem[\protect\citeauthoryear{Fissore}{Fissore}{2003}]{Fissore-These-2003}
87: {\sc Fissore, O.} 2003.
88: \newblock Terminaison de la r\'e\'ecriture sous strat\'egies.
89: \newblock Ph.D. thesis, Universit\'e Henri Poincar\'e-Nancy~I.
90:
91: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
92: et~al\mbox{.}}{2001}]{FGK-local-strat-ENTCS-2001}
93: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2001.
94: \newblock {Termination of rewriting with local strategies}.
95: \newblock In {\em Selected papers of the 4th International Workshop on
96: Strategies in Automated Deduction}, {M.~P. Bonacina} {and} {B.~Gramlich},
97: Eds. Electronic Notes in Theoretical Computer Science, vol.~58. Elsevier
98: Science Publishers B. V. (North-Holland).
99:
100: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
101: et~al\mbox{.}}{2002a}]{FGK-PPDP-2002}
102: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2002a.
103: \newblock {CARIBOO} : An induction based proof tool for termination with
104: strategies.
105: \newblock In {\em Proceedings of the 4th International Conference on Principles
106: and Practice of Declarative Programming}. ACM Press, Pittsburgh (USA),
107: 62--73.
108:
109: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
110: et~al\mbox{.}}{2002b}]{FGK-WRLA-2002}
111: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2002b.
112: \newblock Outermost ground termination.
113: \newblock In {\em Proceedings of the 4th International Workshop on Rewriting
114: Logic and Its Applications}. Electronic Notes in Theoretical Computer
115: Science, vol.~71. Elsevier Science Publishers B. V. (North-Holland), Pisa,
116: Italy.
117:
118: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
119: et~al\mbox{.}}{2002c}]{FGK-out-interne-2002}
120: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2002c.
121: \newblock Outermost ground termination - {E}xtended version.
122: \newblock Tech. Rep. A02-R-493, LORIA, Nancy (France). December.
123:
124: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
125: et~al\mbox{.}}{2004a}]{CARIBOO-APP-2004}
126: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2004a.
127: \newblock Cariboo, a termination proof tool for rewriting-based programming
128: languages with strategies.
129: \newblock Free GPL Licence, APP registration
130: IDDN.FR.001.170013.000.R.P.2005.000.10600.
131: \newblock {\tt Available at http://protheo.loria.fr/softwares/cariboo/}.
132:
133: \bibitem[\protect\citeauthoryear{Fissore, Gnaedig, and Kirchner}{Fissore
134: et~al\mbox{.}}{2004b}]{FGK-ter-faible-ICTAC-2004}
135: {\sc Fissore, O.}, {\sc Gnaedig, I.}, {\sc and} {\sc Kirchner, H.} 2004b.
136: \newblock A proof of weak termination providing the right way to terminate.
137: \newblock In {\em 1st International Colloquium on THEORETICAL ASPECTS OF
138: COMPUTING}. Lecture Notes in Computer Science, vol. 3407. Springer-Verlag,
139: Guiyang, China, 356--371.
140:
141: \bibitem[\protect\citeauthoryear{Futatsugi and Nakagawa}{Futatsugi and
142: Nakagawa}{1997}]{FutatsugiN-IEEE97}
143: {\sc Futatsugi, K.} {\sc and} {\sc Nakagawa, A.} 1997.
144: \newblock An overview of {CAFE} specification environment -- an algebraic
145: approach for creating, verifying, and maintaining formal specifications over
146: networks.
147: \newblock In {\em Proceedings of the 1st {IEEE} Int. Conference on Formal
148: Engineering Methods}.
149:
150: \bibitem[\protect\citeauthoryear{Giesl and Middeldorp}{Giesl and
151: Middeldorp}{2003}]{Giesl-Mid-inn-context-sens-2003}
152: {\sc Giesl, J.} {\sc and} {\sc Middeldorp, A.} 2003.
153: \newblock Innermost termination of context-sensitive rewriting.
154: \newblock In {\em Proceedings of the 6th International Conference on
155: Developments in Language Theory (DLT 2002)}. Lecture Notes in Computer
156: Science, vol. 2450. Springer-Verlag, Kyoto, Japan, 231--244.
157:
158: \bibitem[\protect\citeauthoryear{Giesl, Thiemann, Schneider-Kamp, and
159: Falke}{Giesl et~al\mbox{.}}{2003}]{Giesl-Thi-all-improvingDP-2003}
160: {\sc Giesl, J.}, {\sc Thiemann, R.}, {\sc Schneider-Kamp, P.}, {\sc and} {\sc
161: Falke, S.} 2003.
162: \newblock Improving dependency pairs.
163: \newblock In {\em Proceedings of the 10th International Conference on Logic for
164: Programming, Artificial Intelligence and Reasoning (LPAR '03)}. Lecture Notes
165: in Artificial Intelligence, vol. 2850. Springer-Verlag, Almaty, Kazakhstan,
166: 165--179.
167:
168: \bibitem[\protect\citeauthoryear{Gnaedig, Kirchner, and Fissore}{Gnaedig
169: et~al\mbox{.}}{2001}]{GKF-in-out-2001}
170: {\sc Gnaedig, I.}, {\sc Kirchner, H.}, {\sc and} {\sc Fissore, O.} 2001.
171: \newblock Induction for innermost and outermost ground termination.
172: \newblock Tech. Rep. A01-R-178, LORIA, Nancy (France). September.
173:
174: \bibitem[\protect\citeauthoryear{Goguen, Winkler, Meseguer, Futatsugi, and
175: Jouannaud}{Goguen et~al\mbox{.}}{1992}]{OBJ3}
176: {\sc Goguen, J.}, {\sc Winkler, T.}, {\sc Meseguer, J.}, {\sc Futatsugi, K.},
177: {\sc and} {\sc Jouannaud, J.} 1992.
178: \newblock Introducing {OBJ3}.
179: \newblock Tech. rep., Computer Science Laboratory, SRI International. march.
180:
181: \bibitem[\protect\citeauthoryear{Goubault-Larreck}{Goubault-Larreck}{2001}]{Go%
182: ubault-Larrecq-well-found-2001}
183: {\sc Goubault-Larreck}. 2001.
184: \newblock Well-founded recursive relations.
185: \newblock In {\em Proc. 15th Int. Workshop Computer Science Logic (CSL'2001)}.
186: Lecture Notes in Computer Science, vol. 2142. Springer-Verlag, Paris.
187:
188: \bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1995}]{Gramlich-FI96}
189: {\sc Gramlich, B.} 1995.
190: \newblock Abstract relations between restricted termination and confluence
191: properties of rewrite systems.
192: \newblock {\em Fundamenta Informaticae\/}~{\em 24}, 3--23.
193:
194: \bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1996}]{Gramlich-RTA96}
195: {\sc Gramlich, B.} 1996.
196: \newblock On proving termination by innermost termination.
197: \newblock In {\em Proceedings 7th Conference on Rewriting Techniques and
198: Applications, New Brunswick (New Jersey, USA)}, {H.~Ganzinger}, Ed. Lecture
199: Notes in Computer Science, vol. 1103. Springer-Verlag, 93--107.
200:
201: \bibitem[\protect\citeauthoryear{Kamin and L{\'e}vy}{Kamin and
202: L{\'e}vy}{1980}]{Kamin-Levy}
203: {\sc Kamin, S.} {\sc and} {\sc L{\'e}vy, J.-J.} 1980.
204: \newblock Attempts for generalizing the recursive path ordering.
205: \newblock Unpublished manuscript.
206:
207: \bibitem[\protect\citeauthoryear{Klint}{Klint}{1993}]{Klint-ACM93}
208: {\sc Klint, P.} 1993.
209: \newblock A meta-environment for generating programming environments.
210: \newblock {\em ACM Transactions on Software Engineering and Methodology\/}~{\em
211: 2}, 176--201.
212:
213: \bibitem[\protect\citeauthoryear{Krishna~Rao}{Krishna~Rao}{2000}]{Rao-innermos%
214: t-TCS-2000}
215: {\sc Krishna~Rao, M.} 2000.
216: \newblock Some characteristics of strong normalization.
217: \newblock {\em Theoretical Computer Science\/}~{\em 239}, 141--164.
218:
219: \bibitem[\protect\citeauthoryear{Kruskal}{Kruskal}{1960}]{Kruskal60}
220: {\sc Kruskal, J.~B.} 1960.
221: \newblock Well-quasi ordering, the tree theorem and {V}azsonyi's conjecture.
222: \newblock {\em Trans. Amer. Math. Soc.\/}~{\em 95}, 210--225.
223:
224: \bibitem[\protect\citeauthoryear{Lankford}{Lankford}{1979}]{Lankford-79}
225: {\sc Lankford, D.~S.} 1979.
226: \newblock On proving term rewriting systems are noetherian.
227: \newblock Tech. rep., Louisiana Tech. University, Mathematics Dept., Ruston LA.
228:
229: \bibitem[\protect\citeauthoryear{Lucas}{Lucas}{2001}]{Luc01}
230: {\sc Lucas, S.} 2001.
231: \newblock Termination of rewriting with strategy annotations.
232: \newblock In {\em Proc. of 8th International Conference on Logic for
233: Programming, Artificial Intelligence and Reasoning, LPAR'01}, {A.~Voronkov}
234: {and} {R.~Nieuwenhuis}, Eds. Lecture Notes in Artificial Intelligence, vol.
235: 2250. Springer-Verlag, Berlin, La Habana, Cuba, 669--684.
236:
237: \bibitem[\protect\citeauthoryear{Lucas}{Lucas}{2002}]{LucasIC02}
238: {\sc Lucas, S.} 2002.
239: \newblock Context-sensitive rewriting strategies.
240: \newblock {\em Information and Computation\/}~{\em 178,\/}~1, 294--343.
241:
242: \bibitem[\protect\citeauthoryear{Middeldorp and Hamoen}{Middeldorp and
243: Hamoen}{1994}]{MiddeldorpH-AAECC94}
244: {\sc Middeldorp, A.} {\sc and} {\sc Hamoen, E.} 1994.
245: \newblock Completeness results for basic narrowing.
246: \newblock {\em Applicable Algebra in Engineering, Communication and
247: Computation\/}~{\em 5,\/}~3 \& 4, 213--253.
248:
249: \bibitem[\protect\citeauthoryear{Moreau, Ringeissen, and Vittek}{Moreau
250: et~al\mbox{.}}{2003}]{MoreauRV-2003}
251: {\sc Moreau, P.-E.}, {\sc Ringeissen, C.}, {\sc and} {\sc Vittek, M.} 2003.
252: \newblock {A Pattern Matching Compiler for Multiple Target Languages}.
253: \newblock In {\em 12th Conference on Compiler Construction, Warsaw (Poland)},
254: {G.~Hedin}, Ed. LNCS, vol. 2622. Springer-Verlag, 61--76.
255:
256: \bibitem[\protect\citeauthoryear{Nakamura and Ogata}{Nakamura and
257: Ogata}{2000}]{Nakamura-Ogata-2000}
258: {\sc Nakamura, M.} {\sc and} {\sc Ogata, K.} 2000.
259: \newblock {The evaluation strategy for head normal form with and without
260: on-demand flags}.
261: \newblock In {\em Proceedings of the 3rd International Workshop on Rewriting
262: Logic and its Applications, WRLA'2000}, {K.~Futatsugi}, Ed. Electronic Notes
263: in Theoretical Computer Science, Kanazawa City Cultural Halt, Kanazawa,
264: Japan, 211--227.
265:
266: \bibitem[\protect\citeauthoryear{Nguyen}{Nguyen}{2001}]{NG01a}
267: {\sc Nguyen, Q.-H.} 2001.
268: \newblock Compact normalisation trace via lazy rewriting.
269: \newblock In {\em Proc.\ 1st International Workshop on Reduction Strategies in
270: Rewriting and Programming (WRS 2001)}, {S.~Lucas} {and} {B.~Gramlich}, Eds.
271: Vol.~57. Elsevier Science Publishers B. V. (North-Holland).
272: \newblock Available at {http://www.elsevier.com/locate/entcs/volume57.html}.
273:
274: \bibitem[\protect\citeauthoryear{Panitz and Schmidt-Schauss}{Panitz and
275: Schmidt-Schauss}{1997}]{Panitz-Schmidt-Schauss-1997}
276: {\sc Panitz, S.~E.} {\sc and} {\sc Schmidt-Schauss, M.} 1997.
277: \newblock {TEA}: Automatically proving termination of programs in a non-strict
278: higher-order functional language,.
279: \newblock In {\em Proceedings of Static Analysis Symposium'97}. Lecture Notes
280: in Computer Science, vol. 1302. Springer-Verlag, 345--360.
281:
282: \bibitem[\protect\citeauthoryear{Plaisted}{Plaisted}{1978}]{Plaisted-well-foun%
283: ded-78}
284: {\sc Plaisted, D.} 1978.
285: \newblock Well-founded orderings for proving termination of systems of rewrite
286: rules.
287: \newblock Tech. Rep. R-78-932, Department of Computer Science, Univesity of
288: Illinois at Urbana Champaign. July.
289:
290: \bibitem[\protect\citeauthoryear{Zantema}{Zantema}{1995}]{Zantema-1995}
291: {\sc Zantema, H.} 1995.
292: \newblock Termination of term rewriting by semantic labelling.
293: \newblock {\em Fundamenta Informaticae\/}~{\em 24}, 89--105.
294:
295: \end{thebibliography}
296: