1: \begin{thebibliography}{10}
2:
3: \bibitem{Apt:Handbook}
4: Krzysztof~R. Apt.
5: \newblock Logic programming.
6: \newblock In J.~van Leeuwen, editor, {\em Handbook of {T}heoretical {C}omputer
7: {S}cience}, volume B: Formal Models and Semantics, chapter~15, pages
8: 493--574. MIT Press, 1990.
9:
10: \bibitem{Apt:Book}
11: Krzysztof~R. Apt.
12: \newblock {\em From Logic Programming to Prolog}.
13: \newblock Prentice-Hall International Series in Computer Science. Prentice
14: Hall, 1997.
15:
16: \bibitem{Benoy:King}
17: Florence Benoy and Andy King.
18: \newblock Inferring argument size relationships with {CLP(R)}.
19: \newblock In J.~Gallagher, editor, {\em Logic Program Synthesis and
20: Transformation. Proceedings}, pages 204--223. Springer Verlag, 1996.
21: \newblock Lecture Notes in Computer Science, volume 1207.
22:
23: \bibitem{Bossi:Cocco}
24: Annalisa Bossi and Nicoletta Cocco.
25: \newblock Preserving universal temination through unfold/fold.
26: \newblock In Giorgio Levi and Mario Rodr\'{\i}guez-Artalejo, editors, {\em
27: Algebraic and Logic Programming}, pages 269--286. Springer Verlag, 1994.
28: \newblock Lecture Notes in Computer Science, volume 850.
29:
30: \bibitem{Boye:Maluszynski}
31: Johan Boye and Jan Ma{\l}uszy{\'n}ski.
32: \newblock Directional types and the annotation method.
33: \newblock {\em {J}ournal of {L}ogic {P}rogramming}, 33(3):179--220, 1997.
34:
35: \bibitem{Brodsky:Sagiv:2}
36: Alex Brodsky and Yehoshua Sagiv.
37: \newblock Inference of inequality constraints in logic programs.
38: \newblock In {\em Proceedings of the Tenth ACM SIGACT-SIGART-SIGMOD Symposium
39: on Principles of Database Systems}, pages 227--240, 1991.
40:
41: \bibitem{Maria:Benchmarks}
42: Francisco Bueno, Maria~J. Garc\'{\i}a de~la Banda, and Manuel~V. Hermenegildo.
43: \newblock Effectiveness of global analysis in strict independence-based
44: automatic parallelization.
45: \newblock In Maurice Bruynooghe, editor, {\em Logic Programming, Proceedings of
46: the 1994 International Symposium}, pages 320--336. MIT Press, 1994.
47:
48: \bibitem{Codish:Lagoon}
49: Michael Codish and Vitaly Lagoon.
50: \newblock Type dependencies for logic programs using {ACI}-unification.
51: \newblock In {\em Proceedings of the 1996 Israeli Symposium on Theory of
52: Computing and Systems}, pages 136--145. IEEE Press, June 1996.
53:
54: \bibitem{Codish:Taboch}
55: Michael Codish and Cohavit Taboch.
56: \newblock A semantic basis for termination analysis of logic programs.
57: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 41(1):103--123, 1999.
58:
59: \bibitem{Cousot:Cousot}
60: Patrick Cousot and Radhia Cousot.
61: \newblock Abstract interpretation and application to logic programs.
62: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 13:103--180, 1992.
63:
64: \bibitem{DeSchreye:Decorte:NeverEndingStory}
65: Danny De~Schreye and Stefaan Decorte.
66: \newblock Termination of logic programs: The never-ending story.
67: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 19/20:199--260,
68: May/July 1994.
69:
70: \bibitem{Debray}
71: Saumya~K. Debray.
72: \newblock A simple code improvement scheme for prolog.
73: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 13:103--180, 1992.
74:
75: \bibitem{Decorte:DeSchreye:Fabris}
76: Stefaan Decorte, Danny De~Schreye, and Massimo Fabris.
77: \newblock Automatic inference of norms: a missing link in automatic termination
78: analysis.
79: \newblock In D.~Miller, editor, {\em Proceedings of the 1993 International
80: Logic Programming Symposium}, pages 420--436, 1993.
81:
82: \bibitem{Dershowitz}
83: Nachum Dershowitz.
84: \newblock Orderings for term-rewriting systems.
85: \newblock {\em Theoretical {C}omputer {S}cience}, 17(3):279--301, 1982.
86:
87: \bibitem{Floyd}
88: Robert~W. Floyd.
89: \newblock Assigning meanings to programs.
90: \newblock In J.~Schwartz, editor, {\em Mathematical Aspects of Computer
91: Science}, pages 19--33. American Mathematical Society, 1967.
92: \newblock Proceedings of Symposia in Applied Mathematics; v. 19.
93:
94: \bibitem{Giesl}
95: J{\"u}rgen Giesl.
96: \newblock Termination of nested and mutually recursive algorithms.
97: \newblock {\em {J}ournal of {A}utomated {R}easoning}, 19:1--29, 1997.
98:
99: \bibitem{Graham}
100: Ronald~L. Graham.
101: \newblock {\em Rudiments of {R}amsey theory}.
102: \newblock Number~45 in Regional conference series in mathematics. American
103: {M}athematical {S}ociety, 1980.
104:
105: \bibitem{CLP:Manual}
106: Christian Holzbaur.
107: \newblock O{F}{A}{I} {CLP(Q,R)} {M}anual.
108: \newblock Technical Report TR-95-09, Austrian Research Institute for Artificial
109: Intelligence, Vienna, 1995.
110:
111: \bibitem{Jaffar:Maher}
112: Joxan Jaffar and Michael~J. Maher.
113: \newblock Constraint logic programming: A survey.
114: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 19/20:503--582,
115: May/July 1994.
116:
117: \bibitem{Knuth}
118: Donald~E. Knuth.
119: \newblock Textbook examples of recursion.
120: \newblock In Vladimir Lifschitz, editor, {\em {A}rtificial {I}ntelligence and
121: {M}athematical {T}heory of {C}omputation. {P}apers in {H}onor of {J}ohn
122: {M}c{C}arthy}, pages 207--229. {A}cademic {P}ress, {I}nc., 1991.
123:
124: \bibitem{Lindenstrauss:Sagiv}
125: N. Lindenstrauss and Yehoshua Sagiv.
126: \newblock Automatic termination analysis of logic programs.
127: \newblock In Lee Naish, editor, {\em Proceedings of the Fourteenth
128: International Conference on Logic Programming}, pages 63--77. MIT Press, July
129: 1997.
130:
131: \bibitem{Lindenstrauss:Sagiv:Serebrenik}
132: Naomi Lindenstrauss, Yehoshua Sagiv, and Alexander Serebrenik.
133: \newblock {\em TermiLog\/}: A system for checking termination of queries to
134: logic programs.
135: \newblock In Orna Grumberg, editor, {\em Computer Aided Verification, 9th
136: International Conference}, pages 63--77. Springer Verlag, June 1997.
137: \newblock Lecture Notes in Computer Science, volume 1254.
138:
139: \bibitem{Lindenstrauss:Sagiv:Serebrenik:L}
140: Naomi Lindenstrauss, Yehoshua Sagiv, and Alexander Serebrenik.
141: \newblock Unfolding mystery of the {\em mergesort\/}.
142: \newblock In Norbert Fuchs, editor, {\em Proceedings of the Seventh
143: International Workshop on Logic Program Synthesis and Transformation}.
144: Springer Verlag, 1998.
145: \newblock Lecture Notes in Computer Science, volume 1463.
146:
147: \bibitem{Lloyd:Book}
148: John~W. Lloyd.
149: \newblock {\em Foundations of Logic Programming}.
150: \newblock Symbolic Computation. Springer Verlag, 1984.
151:
152: \bibitem{Manna:McCarthy}
153: Zohar Manna and John McCarthy.
154: \newblock Properties of {P}rograms and partial function logic.
155: \newblock {\em Machine Intelligence}, 5:27--37, 1970.
156:
157: \bibitem{Mesnard:Ganascia}
158: Fred Mesnard and J.~Ganascia.
159: \newblock {CLP(Q)} for proving interargument relations.
160: \newblock In A.~Petrossi, editor, {\em Proceedings {META}'92}, pages 309--320.
161: Springer Verlag, 1992.
162:
163: \bibitem{OKeefe}
164: Richard~A. O'Keefe.
165: \newblock {\em The {C}raft of {P}rolog}.
166: \newblock {MIT} {P}ress, 1990.
167:
168: \bibitem{Plumer:Book}
169: Lutz Pl{\"u}mer.
170: \newblock {\em Termination Proofs for Logic Programs}.
171: \newblock Lecture Notes in Artificial Intelligence, volume 446. Springer
172: Verlag, 1990.
173:
174: \bibitem{Sagiv}
175: Yehoshua Sagiv.
176: \newblock A termination test for logic programs.
177: \newblock In {\em International Logic Programming Symposium}. MIT Press, 1991.
178:
179: \bibitem{XSB:Manual}
180: Konstatinos~F. Sagonas, Terrance Swift, and David~S. Warren.
181: \newblock {\em The XSB Programmer's Manual. Version 1.3 ($\beta$)}.
182: \newblock Department of Computer Science, SUNY @ Stony Brook, U.S.A., September
183: 1993.
184:
185: \bibitem{SICStus:Manual}
186: {SICS}.
187: \newblock {\em User Manual. Version 3.7.1}.
188: \newblock Swedish Institute of Computer Science, 1998.
189:
190: \bibitem{Sterling:Shapiro}
191: Leon Sterling and Ehud Shapiro.
192: \newblock {\em The {A}rt of {P}rolog}.
193: \newblock The {MIT} Press, second edition, 1994.
194:
195: \bibitem{Tamaki:Sato}
196: Hisao Tamaki and Taisuke Sato.
197: \newblock Unfold/{F}old transformation of logic programs.
198: \newblock In Sten-{\AA}ke T{\"a}rnlund, editor, {\em Proceedings of the Second
199: International Logic Programming Conference}, pages 127--138. Uppsala
200: University, 1984.
201:
202: \bibitem{Ullman:van:Gelder}
203: Jeffrey~D. Ullman and Allen van Gelder.
204: \newblock Efficient tests for top-down termination of logical rules.
205: \newblock {\em Journal of the {A}ssociation for {C}omputing {M}achinery},
206: 35(2):345--373, April 1988.
207:
208: \bibitem{van:Gelder}
209: Allen van Gelder.
210: \newblock Deriving constraints among argument sizes in logic programs.
211: \newblock {\em Annals of Mathematics and Artificial Intelligence}, 3:361--392,
212: 1991.
213:
214: \bibitem{Vershaetse:DeSchreye}
215: Kristof Verschaetse and Danny De~Schreye.
216: \newblock Deriving termination proofs for logic programs, using abstract
217: procedures.
218: \newblock In Koichi Furukawa, editor, {\em Logic Programming, Proceedings of
219: the Eigth International Conference}, pages 301--315. MIT Press, 1991.
220:
221: \bibitem{Vershaetse:DeSchreye:Deriving:Linear:Size:Relations}
222: Kristof Verschaetse and Danny De~Schreye.
223: \newblock Deriving of linear size relations by abstract interpretation.
224: \newblock In Maurice Bryunooghe and Martin Wirsing, editors, {\em Programming
225: Language Implementation and Logic Programming, 4th International Symposium},
226: pages 296--310. Springer Verlag, 1992.
227: \newblock Lecture Notes in Computer Science, volume 631.
228:
229: \bibitem{wang}
230: Bal Wang and R.~K. Shyamasundar.
231: \newblock A methodology for proving termination of logic programs.
232: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 21:1--30, 1994.
233:
234: \end{thebibliography}
235: