1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citename{Aguzzi \& Modigliani, }1993]{AguMod93}
4: Aguzzi, G., \& Modigliani, U. (1993).
5: \newblock Proving termination of logic program by transforming them into
6: equivalent term rewriting systems.
7: \newblock {\em Pages 114--124 of:} Shyamasundar, R.~K. (ed), {\em Proc. of the
8: 13th {C}onference on {F}oundations of {S}oftware {T}echnology and
9: {T}heoretical {C}omputer {S}cience}.
10: \newblock {LNCS}, vol. 761.
11: \newblock Springer-{V}erlag.
12:
13: \bibitem[\protect\citename{Apt, }1997]{Apt97}
14: Apt, K.~R. (1997).
15: \newblock {\em From logic programming to {P}rolog}.
16: \newblock Prentice Hall.
17:
18: \bibitem[\protect\citename{Apt \& Bezem, }1991]{AB91}
19: Apt, K.~R., \& Bezem, M. (1991).
20: \newblock Acyclic programs.
21: \newblock {\em New {G}eneration {C}omputing}, {\bf 29}(3), 335--363.
22:
23: \bibitem[\protect\citename{Apt \& Etalle, }1993]{AE93}
24: Apt, K.~R., \& Etalle, S. (1993).
25: \newblock On the unification free {P}rolog programs.
26: \newblock {\em Pages 1--19 of:} Borzyszkowski, A., \& Sokolowski, S. (eds),
27: {\em Proc. of the 18th international symposium on {M}athematical
28: {F}oundations of {C}omputer {S}cience}.
29: \newblock {LNCS}, vol. 711.
30: \newblock Springer-{V}erlag.
31:
32: \bibitem[\protect\citename{Apt \& Luitjes, }1995]{AL95}
33: Apt, K.~R., \& Luitjes, I. (1995).
34: \newblock Verification of logic programs with delay declarations.
35: \newblock {\em Pages 66--90 of:} Alagar, V.~S., \& Nivat, M. (eds), {\em Proc.
36: of the 4th international conference on algebraic methodology and software
37: technology}.
38: \newblock {LNCS}, vol. 936.
39: \newblock Springer-{V}erlag.
40:
41: \bibitem[\protect\citename{Apt \& Pedreschi, }1993]{AP93r}
42: Apt, K.~R., \& Pedreschi, D. (1993).
43: \newblock Reasoning about termination of pure {P}rolog programs.
44: \newblock {\em Information and {C}omputation}, {\bf 106}(1), 109--157.
45:
46: \bibitem[\protect\citename{Apt \& Pedreschi, }1994]{AP94m}
47: Apt, K.~R., \& Pedreschi, D. (1994).
48: \newblock Modular termination proofs for logic and pure {P}rolog programs.
49: \newblock {\em Pages 183--229 of:} Levi, G. (ed), {\em Advances in logic
50: programming theory}.
51: \newblock Oxford University Press.
52:
53: \bibitem[\protect\citename{Apt {\em et~al.}\relax, }1994]{AMP94}
54: Apt, K.~R., Marchiori, E., \& Palamidessi, C. (1994).
55: \newblock A declarative approach for first-order built-in's of {P}rolog.
56: \newblock {\em Applicable algebra in engineering, communication and
57: computation}, {\bf 5}(3/4), 159--191.
58:
59: \bibitem[\protect\citename{Arts, }1997]{Art97}
60: Arts, T. (1997).
61: \newblock {\em Automatically proving termination and innermost normalisation of
62: term rewriting systems}.
63: \newblock Ph.D. thesis, Universiteit Utrecht.
64:
65: \bibitem[\protect\citename{Balbiani, }1992]{Bal91}
66: Balbiani, P. (1992).
67: \newblock The finiteness of logic programming derivations.
68: \newblock {\em Pages 403--419 of:} Levi, G. (ed), {\em Proc. of the 3rd
69: {C}onference on {A}lgebraic and {L}ogic {P}rogramming}.
70: \newblock {LNCS}, vol. 632.
71: \newblock Springer-{V}erlag.
72:
73: \bibitem[\protect\citename{Baudinet, }1992]{Bau92}
74: Baudinet, M. (1992).
75: \newblock Proving termination properties of {P}rolog programs: a semantic
76: approach.
77: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 14}, 1--29.
78:
79: \bibitem[\protect\citename{Benoy \& King, }1997]{BK97}
80: Benoy, F., \& King, A. (1997).
81: \newblock Inferring argument size relationships with {CLP(R)}.
82: \newblock {\em Pages 204--223 of:} Gallagher, J.~P. (ed), {\em Proc. of the
83: 6th international workshop on logic programming synthesis and
84: transformation}.
85: \newblock {LNCS}, vol. 1207.
86: \newblock Springer-{V}erlag.
87:
88: \bibitem[\protect\citename{Bezem, }1993]{Bez93}
89: Bezem, M.~A. (1993).
90: \newblock Strong {T}ermination of {L}ogic {P}rograms.
91: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 15}(1 \& 2), 79--98.
92:
93: \bibitem[\protect\citename{Bol {\em et~al.}\relax, }1991]{BAK91}
94: Bol, R.~N., Apt, K.~R., \& Klop, J.~W. (1991).
95: \newblock An analysis of loop checking mechanism for logic programs.
96: \newblock {\em Theoretical {C}omputer {S}cience}, {\bf 86}(1), 35--79.
97:
98: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }1994]{BCF94}
99: Bossi, A., Cocco, N., \& Fabris, M. (1994).
100: \newblock Norms on terms and their use in proving universal termination of a
101: logic program.
102: \newblock {\em Theoretical {C}omputer {S}cience}, {\bf 124}(2), 297--328.
103:
104: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }1999]{BER99}
105: Bossi, A., Etalle, S., \& Rossi, S. (1999).
106: \newblock Properties of input-consuming derivations.
107: \newblock Etalle, S., \& Smaus, J.-G. (eds), {\em Proc. of the {ICLP}
108: {W}orkshop on {V}erification of {L}ogic {P}rograms}.
109: \newblock Electronic {N}otes in {T}heoretical {C}omputer {S}cience, vol. 30(1).
110:
111: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }2000]{BER00}
112: Bossi, A., Etalle, S., \& Rossi, S. (2000).
113: \newblock Semantics of input-consuming logic programs.
114: \newblock {\em Pages 194--208 of:} {Lloyd, J. W. et al.} (ed), {\em Proc. of
115: the 1st {I}nternational {C}onference on {C}omputational {L}ogic}.
116: \newblock {LNCS}, vol. 1861.
117: \newblock Springer-{V}erlag.
118:
119: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }2001]{BERS01}
120: Bossi, A., Etalle, S., Rossi, S., \& Smaus, J.-G. (2001).
121: \newblock On the semantics and termination of logic programs with dynamic
122: scheduling.
123: \newblock Sands, D. (ed), {\em Proc. of the 10th {E}uropean {S}ymposium on
124: {P}rogramming}.
125: \newblock {LNCS}, vol. 2028.
126: \newblock Springer-{V}erlag.
127:
128: \bibitem[\protect\citename{Braem {\em et~al.}\relax, }1994]{BCMV94}
129: Braem, C., Charlier, B.~Le, Modart, S., \& {Van Hentenryck}, P. (1994).
130: \newblock Cardinality analysis of {P}rolog.
131: \newblock {\em Pages 457---471 of:} Bruynooghe, M. (ed), {\em Proc. of the
132: {I}nternational {L}ogic {P}rogramming {S}ymposium}.
133: \newblock MIT Press.
134:
135: \bibitem[\protect\citename{Bronsard {\em et~al.}\relax, }1992]{BLR92}
136: Bronsard, F., Lakshman, T.~K., \& Reddy, U.~S. (1992).
137: \newblock A framework of directionality for proving termination of logic
138: programs.
139: \newblock {\em Pages 321--335 of:} Apt, K.~R. (ed), {\em Proc. of the {J}oint
140: {I}nternational {C}onference and {S}ymposium on {L}ogic {P}rogramming}.
141: \newblock MIT Press.
142:
143: \bibitem[\protect\citename{Bruynooghe {\em et~al.}\relax, }1998]{BVWD98}
144: Bruynooghe, M., Vandecasteele, H., de~Waal, D.~A., \& Denecker, M. (1998).
145: \newblock Detecting unsolvable queries for definite logic programs.
146: \newblock {\em Pages 118--133 of:} {Palamidessi, C. et al.} (ed), {\em Proc.
147: of {PLILP/ALP} '98}.
148: \newblock {LNCS}, vol. 1490.
149: \newblock Springer-{V}erlag.
150:
151: \bibitem[\protect\citename{Cavedon, }1989]{Cav89}
152: Cavedon, L. (1989).
153: \newblock Continuity, consistency, and completeness properties for logic
154: programs.
155: \newblock {\em Pages 571--584 of:} Levi, G., \& Martelli, M. (eds), {\em
156: Proceedings of the {I}nternational {C}onference on {L}ogic {P}rogramming}.
157: \newblock The MIT Press.
158:
159: \bibitem[\protect\citename{Codish \& Taboch, }1999]{CT99}
160: Codish, M., \& Taboch, C. (1999).
161: \newblock {A} semantic basis for the termination analysis of logic programs.
162: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 41}(1), 103--123.
163:
164: \bibitem[\protect\citename{Colussi {\em et~al.}\relax, }1995]{CMM95}
165: Colussi, L., Marchiori, E., \& Marchiori, M. (1995).
166: \newblock On termination of constraint logic programs.
167: \newblock {\em Pages 431--448 of:} Bruynooghe, M., \& Penjam, J. (eds), {\em
168: Proc. of the 1st international conference of {P}rinciples and {P}ractice of
169: {C}onstraint {P}rogramming}.
170: \newblock {LNCS}, vol. 976.
171: \newblock Springer-{V}erlag.
172:
173: \bibitem[\protect\citename{{De Schreye} \& Decorte, }1994]{SD94}
174: {De Schreye}, D., \& Decorte, S. (1994).
175: \newblock Termination of logic programs: the never-ending story.
176: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 19-20}, 199--260.
177:
178: \bibitem[\protect\citename{{De Schreye} {\em et~al.}\relax, }1992]{SVB92}
179: {De Schreye}, D., Verschaetse, K., \& Bruynooghe, M. (1992).
180: \newblock A framework for analyzing the termination of definite logic programs
181: with respect to call patterns.
182: \newblock {\em Pages 481--488 of:} {\em Proc. of the {I}nternational
183: {C}onference on {F}ifth {G}eneration {C}omputer {S}ystems}.
184: \newblock Institute for New Generation Computer Technology.
185:
186: \bibitem[\protect\citename{Debray \& Lin, }1993]{DL93}
187: Debray, S.~K., \& Lin, N.~W. (1993).
188: \newblock Cost analysis of logic programs.
189: \newblock {\em {ACM} {T}rans. on {P}rogramming {L}anguages and {S}ystems}, {\bf
190: 15}(5), 826--875.
191:
192: \bibitem[\protect\citename{Decorte {\em et~al.}\relax, }1993]{DDF93}
193: Decorte, S., {De Schreye}, D., \& Fabris, M. (1993).
194: \newblock Automatic inference of norms: {A} missing link in automatic
195: termination analysis.
196: \newblock {\em Pages 420--436 of:} Miller, D. (ed), {\em Proc. of the
197: {I}nternational {L}ogic {P}rogramming {S}ymposium}.
198: \newblock The {MIT} {P}ress.
199:
200: \bibitem[\protect\citename{Decorte {\em et~al.}\relax, }1998]{DDLMS98}
201: Decorte, S., {De Schreye}, D., Leuschel, M., Martens, B., \& Sagonas, K.
202: (1998).
203: \newblock Termination analysis for tabled logic programming.
204: \newblock {\em Pages 111--127 of:} Fuchs, N.~E. (ed), {\em Proc. of the 7th
205: international workshop on logic programming synthesis and transformation}.
206: \newblock {LNCS}, vol. 1463.
207: \newblock Springer-{V}erlag.
208:
209: \bibitem[\protect\citename{Decorte {\em et~al.}\relax, }1999]{DDV99}
210: Decorte, S., {De Schreye}, D., \& Vandecasteele, H. (1999).
211: \newblock Constraint-based termination analysis of logic programs.
212: \newblock {\em {ACM} {T}rans. on {P}rogramming {L}anguages and {S}ystems}, {\bf
213: 21}(6), 1137--1195.
214:
215: \bibitem[\protect\citename{Deransart \& Ma{\l}uszy{\'n}ski, }1993]{DM93}
216: Deransart, P., \& Ma{\l}uszy{\'n}ski, J. (1993).
217: \newblock {\em A grammatical view of logic programming}.
218: \newblock The MIT Press.
219:
220: \bibitem[\protect\citename{Etalle {\em et~al.}\relax, }1999]{EBC99}
221: Etalle, S., Bossi, A., \& Cocco, N. (1999).
222: \newblock Termination of well-moded programs.
223: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 38}(2), 243--257.
224:
225: \bibitem[\protect\citename{Ganzinger \& Waldmann, }1992]{GW92}
226: Ganzinger, H., \& Waldmann, U. (1992).
227: \newblock Termination {P}roofs of {W}ell-{M}oded {L}ogic {P}rograms via
228: {C}onditional {R}ewrite {S}ystems.
229: \newblock {\em Pages 430--437 of:} Rusinowitch, M., \& R\'emy, J.~L. (eds),
230: {\em Proc. of the 3rd {I}nternational {W}orkshop on {C}onditional {T}erm
231: {R}ewriting {S}ystems}.
232: \newblock {LNCS}, vol. 656.
233: \newblock Springer-{V}erlag.
234:
235: \bibitem[\protect\citename{Gori, }2000]{Gor00}
236: Gori, R. (2000).
237: \newblock An abstract interpretation approach to termination of logic programs.
238: \newblock {\em Pages 362--380 of:} Parigot, M., \& Voronkov, A. (eds), {\em
239: Proc. of the 7th international conference on logic for programming and
240: automated reasoning}.
241: \newblock {LNCS}, vol. 1955.
242: \newblock Springer-{V}erlag.
243:
244: \bibitem[\protect\citename{Hill \& Lloyd, }1994]{HL94}
245: Hill, P.~M., \& Lloyd, J.~W. (1994).
246: \newblock {\em The {G}\"odel programming language}.
247: \newblock The MIT Press.
248:
249: \bibitem[\protect\citename{Hitzler \& Seda, }1999]{HS99}
250: Hitzler, P., \& Seda, A.~K. (1999).
251: \newblock Acceptable programs revisited.
252: \newblock Etalle, S., \& Smaus, J.-G. (eds), {\em Proc. of {ICLP} {W}orkshop
253: on {V}erification of {L}ogic {P}rograms}.
254: \newblock Electronic {N}otes in {T}heoretical {C}omputer {S}cience, vol. 30(1).
255:
256: \bibitem[\protect\citename{Hoarau \& Mesnard, }1998]{HM98}
257: Hoarau, S., \& Mesnard, F. (1998).
258: \newblock Inferring and compiling termination for constraint logic programs.
259: \newblock {\em Pages 240--254 of:} Flener, P. (ed), {\em Proc. of the 8th
260: international workshop on logic programming synthesis and transformation}.
261: \newblock {LNCS}, vol. 1559.
262: \newblock Springer-{V}erlag.
263:
264: \bibitem[\protect\citename{Hoarau \& Mesnard, }2001]{HM01}
265: Hoarau, S., \& Mesnard, F. (2001).
266: \newblock {LOGICAL PEARL} $\sigma$-termination: from a characterisation to an
267: automated sufficient condition.
268: \newblock {\em Theory and practice of logic programming}.
269: \newblock To appear.
270:
271: \bibitem[\protect\citename{Kowalski, }1979]{Kow79}
272: Kowalski, R.~A. (1979).
273: \newblock Algorithm = {L}ogic + {C}ontrol.
274: \newblock {\em Comm. of the {ACM}}, {\bf 22}(7), 424--436.
275:
276: \bibitem[\protect\citename{{Krishna Rao} {\em et~al.}\relax, }1992]{KKS92}
277: {Krishna Rao}, {M~.R.~K.}, Kapur, D., \& Shyamasundar, {R.~K.} (1992).
278: \newblock A transformational methodology for proving termination of logic
279: programs.
280: \newblock {\em Pages 213--226 of:} B{\"o}rger, E., J{\"a}ger, G., {Kleine
281: B{\"u}ning}, H., \& Richter, M.~M. (eds), {\em Proc. of the 5th workshop on
282: {C}omputer {S}cience {L}ogic}.
283: \newblock {LNCS}, vol. 626.
284: \newblock Springer-{V}erlag.
285:
286: \bibitem[\protect\citename{{Krishna Rao} {\em et~al.}\relax, }1997]{KKS97}
287: {Krishna Rao}, {M. R. K.}, Kapur, D., \& Shyamasundar, R.~K. (1997).
288: \newblock Proving termination of {GHC} programs.
289: \newblock {\em New {G}eneration {C}omputing}, {\bf 15}(3), 293--338.
290:
291: \bibitem[\protect\citename{{Krishna Rao} {\em et~al.}\relax, }1998]{KRKS98}
292: {Krishna Rao}, M. R.~K., Kapur, D., \& Shyamasundar, R.~K. (1998).
293: \newblock Transformational methodology for proving termination of logic
294: programs.
295: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 34}(1), 1--41.
296:
297: \bibitem[\protect\citename{Lindenstrauss \& Sagiv, }1997]{LS97}
298: Lindenstrauss, N., \& Sagiv, Y. (1997).
299: \newblock Automatic termination analysis of logic programs.
300: \newblock {\em Pages 63--77 of:} Naish, L. (ed), {\em Proc. of the
301: {I}nternational {C}onference on {L}ogic {P}rogramming}.
302: \newblock The {MIT} {P}ress.
303:
304: \bibitem[\protect\citename{L{\"u}ttringhau{s-K}appel, }1993]{Lut93}
305: L{\"u}ttringhau{s-K}appel, S. (1993).
306: \newblock Control generation for logic programs.
307: \newblock {\em Pages 478--495 of:} Warren, D.~S. (ed), {\em Proceedings of the
308: 10th {I}nternational {C}onference on {L}ogic {P}rogramming}.
309: \newblock MIT Press.
310:
311: \bibitem[\protect\citename{Marchiori, }1996a]{Mar95c}
312: Marchiori, E. (1996a).
313: \newblock On termination of general logic programs w.r.t. constructive
314: negation.
315: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 26}(1), 69--89.
316:
317: \bibitem[\protect\citename{Marchiori \& Teusink, }1999]{MT99}
318: Marchiori, E., \& Teusink, F. (1999).
319: \newblock On termination of logic programs with delay declarations.
320: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 39}(1-3), 95--124.
321:
322: \bibitem[\protect\citename{Marchiori, }1994]{MarM94}
323: Marchiori, M. (1994).
324: \newblock Logic programs as term rewriting systems.
325: \newblock {\em Pages 223--241 of:} Levi, G., \& Rodr{\'\i}guez-Artalejo, M.
326: (eds), {\em Proc. of the 4th international conference on {A}lgebraic and
327: {L}ogic {P}rogramming}.
328: \newblock {LNCS}, vol. 850.
329: \newblock Springer-{V}erlag.
330:
331: \bibitem[\protect\citename{Marchiori, }1996b]{Mar96}
332: Marchiori, M. (1996b).
333: \newblock Proving existential termination of normal logic programs.
334: \newblock {\em Pages 375--390 of:} Wirsing, M., \& Nivat, M. (eds), {\em Proc.
335: of the 5th international conference on algebraic methodology and software
336: technology}.
337: \newblock {LNCS}, vol. 1101.
338: \newblock Springer-{V}erlag.
339:
340: \bibitem[\protect\citename{Martin \& King, }1997]{MK97}
341: Martin, J., \& King, A. (1997).
342: \newblock Generating efficient, terminating logic programs.
343: \newblock {\em Pages 273--284 of:} Bidoit, M., \& Dauchet, M. (eds), {\em
344: Proc. of the 7th international conference on theory and practice of software
345: development}.
346: \newblock {LNCS}, vol. 1214.
347: \newblock Springer-{V}erlag.
348:
349: \bibitem[\protect\citename{McPhee, }2000]{McPhee00}
350: McPhee, R. (2000).
351: \newblock {\em Compositional logic programming}.
352: \newblock Ph.D. thesis, Oxford University Computing Laboratory.
353:
354: \bibitem[\protect\citename{Mesnard, }1996]{Mes96}
355: Mesnard, F. (1996).
356: \newblock Inferring left-terminating classes of queries for constraint logic
357: programs.
358: \newblock {\em Pages 7--21 of:} Maher, M. (ed), {\em Proc. of the {J}oint
359: {I}nternational {C}onference and {S}ymposium on {L}ogic {P}rogramming}.
360: \newblock The {MIT} {P}ress.
361:
362: \bibitem[\protect\citename{Mesnard {\em et~al.}\relax, }2000]{Mesnard00}
363: Mesnard, F., Neumerkel, U., \& Hoarau, S. (2000).
364: \newblock Implementing c{TI} : a {C}onstrained-based {L}eft-termination
365: {I}nference tool for {LP}.
366: \newblock {\em Pages 152--166 of:} de~Castro~Dutra, I. (ed), {\em Proc. of the
367: {CL} workshop on parallelism and {I}mplementation {T}echnology for
368: ({C}onstraint) {L}ogic {P}rogramming {L}anguages}.
369:
370: \bibitem[\protect\citename{Naish, }1992]{Nai92c}
371: Naish, L. (1992).
372: \newblock {\em Coroutining and the construction of terminating logic programs}.
373: \newblock Tech. rept. 92/5. Department of Computer Science, University of
374: Melbourne.
375:
376: \bibitem[\protect\citename{Neumerkel \& Mesnard, }1999]{NM99}
377: Neumerkel, U., \& Mesnard, F. (1999).
378: \newblock Localizing and explaining reasons for nonterminating logic programs
379: with failure slices.
380: \newblock {\em Pages 328--341 of:} Nadathur, G. (ed), {\em Proc. of the
381: international conference on {P}rinciples and {P}ractice of {D}eclarative
382: {P}rogramming}.
383: \newblock {LNCS}, vol. 1702.
384: \newblock Springer-{V}erlag.
385:
386: \bibitem[\protect\citename{Pedreschi \& Ruggieri, }1999a]{PR99}
387: Pedreschi, D., \& Ruggieri, S. (1999a).
388: \newblock Bounded nondeterminism of logic programs.
389: \newblock {\em Pages 350--364 of:} {De~Schreye}, D. (ed), {\em Proc. of the
390: {I}nternational {C}onference on {L}ogic {P}rogramming}.
391: \newblock The {MIT} {P}ress.
392:
393: \bibitem[\protect\citename{Pedreschi \& Ruggieri, }1999b]{PR99fail}
394: Pedreschi, D., \& Ruggieri, S. (1999b).
395: \newblock On logic programs that do not fail.
396: \newblock Etalle, S., \& Smaus, J.-G. (eds), {\em Proc. of {ICLP} {W}orkshop
397: on {V}erification of {L}ogic {P}rograms}.
398: \newblock Electronic {N}otes in {T}heoretical {C}omputer {S}cience, vol. 30(1).
399:
400: \bibitem[\protect\citename{Pedreschi \& Ruggieri, }1999c]{PR95v}
401: Pedreschi, D., \& Ruggieri, S. (1999c).
402: \newblock Verification of {L}ogic {P}rograms.
403: \newblock {\em Journal of logic programming}, {\bf 39}((1-3)), 125--176.
404:
405: \bibitem[\protect\citename{Pl{\"{u}}mer, }1990]{Plu90}
406: Pl{\"{u}}mer, L. (1990).
407: \newblock {\em Termination proofs for logic programs}.
408: \newblock Lecture Notes in Artificial Intelligence, vol. 446.
409: \newblock Springer-{V}erlag.
410:
411: \bibitem[\protect\citename{Ruggieri, }1997]{Rug97t}
412: Ruggieri, S. (1997).
413: \newblock Termination of constraint logic programs.
414: \newblock {\em Pages 838--848 of:} Degano, P., Gorrieri, R., \&
415: Marchetti-Spaccamela, A. (eds), {\em Proc. of the 24th {I}nternational
416: {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP} '97)}.
417: \newblock {LNCS}, vol. 1256.
418: \newblock Springer-{V}erlag.
419:
420: \bibitem[\protect\citename{Ruggieri, }1999]{Rug99}
421: Ruggieri, S. (1999).
422: \newblock {\em Verification and validation of logic programs}.
423: \newblock Ph.D. thesis, Dipartimento di Informatica, Universit{\`a} di Pisa.
424:
425: \bibitem[\protect\citename{Ruggieri, }2001]{RugTCS98}
426: Ruggieri, S. (2001).
427: \newblock {$\exists$}-universal termination of logic programs.
428: \newblock {\em Theoretical {C}omputer {S}cience}, {\bf 254}(1-2), 273--296.
429:
430: \bibitem[\protect\citename{Sagiv, }1991]{Sag91}
431: Sagiv, Y. (1991).
432: \newblock A termination test for logic programs.
433: \newblock {\em Pages 518--532 of:} Saraswat, V.~A., \& Ueda, K. (eds), {\em
434: Proc. of the {I}nternational {L}ogic {P}rogramming {S}ymposium}.
435: \newblock The {MIT} {P}ress.
436:
437: \bibitem[\protect\citename{Serebrenik \& Schreye, }2001]{SS01}
438: Serebrenik, A., \& Schreye, D.~De. (2001).
439: \newblock Non-tranformational termination analysis of logic programs, based on
440: general term-orderings.
441: \newblock {\em Pages 69--85 of:} Lau, K. (ed), {\em Proc. of the 10th
442: international workshop on logic programming synthesis and transformation,
443: selected papers}.
444: \newblock {LNCS}, vol. 2042.
445: \newblock Springer-{V}erlag.
446:
447: \bibitem[\protect\citename{SICStus, }1998]{sicstus}
448: SICStus. (1998).
449: \newblock {\em {SICS}tus {P}rolog {U}ser's manual}.
450: \newblock Intelligent Systems Laboratory, Swedish Institute of Computer
451: Science, PO Box 1263, \mbox{S-164 29} Kista, Sweden.
452: \newblock {\tt http://www.sics.se/sicstus/docs/3.7.1/html/sicstus\_toc.html}.
453:
454: \bibitem[\protect\citename{Smaus, }1999a]{Sma99t}
455: Smaus, J.-G. (1999a).
456: \newblock {\em Modes and types in logic programming}.
457: \newblock Ph.D. thesis, University of Kent at Canterbury.
458:
459: \bibitem[\protect\citename{Smaus, }1999b]{Sma99}
460: Smaus, J.-G. (1999b).
461: \newblock Proving termination of input-consuming logic programs.
462: \newblock {\em Pages 335--349 of:} {De Schreye}, D. (ed), {\em Proc. of the
463: {I}nternational {C}onference on {L}ogic {P}rogramming}.
464: \newblock MIT Press.
465:
466: \bibitem[\protect\citename{Smaus {\em et~al.}\relax, }2001]{SHK01}
467: Smaus, J.-G., Hill, P.~M., \& King, A.~M. (2001).
468: \newblock Verifying termination and error-freedom of logic programs with {\tt
469: block} declarations.
470: \newblock {\em Theory and {P}ractice of {L}ogic {P}rogramming}, {\bf 1}(4),
471: 447--486.
472:
473: \bibitem[\protect\citename{Somogyi {\em et~al.}\relax, }1996]{SHC96}
474: Somogyi, Z., Henderson, F., \& Conway, T. (1996).
475: \newblock The execution algorithm of {Mercury}, an efficient purely declarative
476: logic programming language.
477: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 29}(1--3), 17--64.
478:
479: \bibitem[\protect\citename{Speirs {\em et~al.}\relax, }1997]{SSS97}
480: Speirs, C., Somogyi, Z., \& S{\o}ndergaard, H. (1997).
481: \newblock {T}ermination {A}nalysis for {M}ercury.
482: \newblock {\em Pages 160--171 of:} {Van Hentenryck}, P. (ed), {\em Proc. of
483: the 4th international {S}tatic {A}nalysis {S}ymposium}.
484: \newblock {LNCS}, vol. 1302.
485: \newblock Springer-{V}erlag.
486:
487: \bibitem[\protect\citename{St\"ark, }1998]{Sta98}
488: St\"ark, R.~F. (1998).
489: \newblock The theoretical foundations of {LPTP} ({A} {L}ogic {P}rogram
490: {T}heorem {P}rover).
491: \newblock {\em Journal of {L}ogic {P}rogramming}, {\bf 36}(3), 241--269.
492:
493: \bibitem[\protect\citename{Sterling \& Shapiro, }1986]{SS86}
494: Sterling, L., \& Shapiro, E. (1986).
495: \newblock {\em The art of {P}rolog}.
496: \newblock The {MIT} {P}ress.
497:
498: \bibitem[\protect\citename{Thom \& Zobel, }1988]{nuprolog}
499: Thom, J., \& Zobel, J. (1988).
500: \newblock {\em {NU-{P}rolog} reference manual, version 1.3}.
501: \newblock Tech. rept. Department of Computer Science, University of Melbourne,
502: Australia.
503:
504: \bibitem[\protect\citename{Ueda, }1988]{Ued88}
505: Ueda, K. (1988).
506: \newblock {G}uarded {H}orn {C}lauses, a parallel logic programming language
507: with the concept of a guard.
508: \newblock {\em Pages 441--456 of:} Nivat, M., \& Fuchi, K. (eds), {\em
509: Programming of {F}uture {G}eneration {C}omputers}.
510: \newblock North Holland, Amsterdam.
511:
512: \bibitem[\protect\citename{van Gelder, }1991]{vG91}
513: van Gelder, A. (1991).
514: \newblock Deriving constraints among argument sizes in logic programs.
515: \newblock {\em Annals of {M}athematics and {A}rtificial {I}ntelligence}, {\bf
516: 3}, 361--392.
517:
518: \bibitem[\protect\citename{Verbaeten, }1999]{Ver99}
519: Verbaeten, S. (1999).
520: \newblock Termination analysis for abductive general logic programs.
521: \newblock {\em Pages 365--379 of:} {De~Schreye}, D. (ed), {\em Proc. of the
522: {I}nternational {C}onference on {L}ogic {P}rogramming}.
523: \newblock The {MIT} {P}ress.
524:
525: \bibitem[\protect\citename{Verbaeten \& {De Schreye}, }2001]{VD01}
526: Verbaeten, S., \& {De Schreye}, D. (2001).
527: \newblock Termination of simply-moded well-typed logic programs under a tabled
528: execution mechanism.
529: \newblock {\em Applicable {A}lgebra in {E}ngineering, {C}ommunication and
530: {C}omputing}.
531: \newblock To appear.
532:
533: \bibitem[\protect\citename{Verbaeten {\em et~al.}\relax, }2001]{VSD01}
534: Verbaeten, S., Sagonas, K., \& {De Schreye}, D. (2001).
535: \newblock Termination proofs for logic programs with tabling.
536: \newblock {\em {ACM} {T}rans. on {C}omputational {L}ogic}, {\bf 2}(1), 57--92.
537:
538: \end{thebibliography}
539: