1: \begin{thebibliography}{10}
2:
3: \bibitem{Andrews:WST99}
4: J.~H. Andrews.
5: \newblock {T}ermination {S}emantics of {L}ogic {P}rograms with {C}ut and
6: {R}elated {F}eatures.
7: \newblock Available at \verb+ http://www.inferenzsysteme.informatik.+\\
8: \verb+tu-darmstadt.de/~giesl/WST99/submissions/andrews.ps+, May 1999.
9:
10: \bibitem{Apt:Handbook}
11: K.~R. Apt.
12: \newblock Logic programming.
13: \newblock In J.~van Leeuwen, editor, {\em Handbook of {T}heoretical {C}omputer
14: {S}cience}, volume B: Formal Models and Semantics, chapter~15, pages
15: 493--574. MIT Press, 1990.
16:
17: \bibitem{Apt:Book}
18: K.~R. Apt.
19: \newblock {\em From Logic Programming to Prolog}.
20: \newblock Prentice-Hall International Series in Computer Science. Prentice
21: Hall, 1997.
22:
23: \bibitem{Benoy:King}
24: F.~Benoy and A.~King.
25: \newblock Inferring argument size relationships with {CLP(R)}.
26: \newblock In J.~Gallagher, editor, {\em Logic Program Synthesis and
27: Transformation. Proceedings}, pages 204--223. Springer Verlag, 1996.
28: \newblock Lecture Notes in Computer Science, volume 1207.
29:
30: \bibitem{Bossi:Cocco}
31: A.~Bossi and N.~Cocco.
32: \newblock Preserving universal temination through unfold/fold.
33: \newblock In G.~Levi and M.~Rodr\'{\i}guez-Artalejo, editors, {\em Algebraic
34: and Logic Programming}, pages 269--286. Springer Verlag, 1994.
35: \newblock Lecture Notes in Computer Science, volume 850.
36:
37: \bibitem{Bossi:Cocco:Fabris}
38: A.~Bossi, N.~Cocco, and M.~Fabris.
39: \newblock Norms on terms and their use in proving universal termination of a
40: logic program.
41: \newblock {\em Theoretical Computer Science}, 124(2):297--328, February 1994.
42:
43: \bibitem{Boye:Maluszynski}
44: J.~Boye and J.~Ma{\l}uszy{\'n}ski.
45: \newblock Directional types and the annotation method.
46: \newblock {\em {J}ournal of {L}ogic {P}rogramming}, 33(3):179--220, 1997.
47:
48: \bibitem{Brodsky:Sagiv}
49: A.~Brodsky and Y.~Sagiv.
50: \newblock Inference of monotonicity constraints in datalog programs.
51: \newblock In {\em Proceedings of the Eighth ACM SIGACT-SIGART-SIGMOD Symposium
52: on Principles of Database Systems}, pages 190--199, 1989.
53:
54: \bibitem{Brodsky:Sagiv:2}
55: A.~Brodsky and Y.~Sagiv.
56: \newblock Inference of inequality constraints in logic programs.
57: \newblock In {\em Proceedings of the Tenth ACM SIGACT-SIGART-SIGMOD Symposium
58: on Principles of Database Systems}, pages 227--240, 1991.
59:
60: \bibitem{Maria:Benchmarks}
61: F.~Bueno, M.~J. Garc\'{\i}a de~la Banda, and M.~V. Hermenegildo.
62: \newblock Effectiveness of global analysis in strict independence-based
63: automatic parallelization.
64: \newblock In M.~Bruynooghe, editor, {\em Logic Programming, Proceedings of the
65: 1994 International Symposium}, pages 320--336. MIT Press, 1994.
66:
67: \bibitem{Codish:Lagoon}
68: M.~Codish and V.~Lagoon.
69: \newblock Type dependencies for logic programs using {ACI}-unification.
70: \newblock In {\em Proceedings of the 1996 Israeli Symposium on Theory of
71: Computing and Systems}, pages 136--145. IEEE Press, June 1996.
72:
73: \bibitem{Codish:Taboch}
74: M.~Codish and C.~Taboch.
75: \newblock A semantic basis for termination analysis of logic programs.
76: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 41(1):103--123, 1999.
77:
78: \bibitem{Cousot:Cousot}
79: P.~Cousot and R.~Cousot.
80: \newblock Abstract interpretation and application to logic programs.
81: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 13:103--180, 1992.
82:
83: \bibitem{DeSchreye:Decorte:NeverEndingStory}
84: D.~De~Schreye and S.~Decorte.
85: \newblock Termination of logic programs: The never-ending story.
86: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 19/20:199--260,
87: May/July 1994.
88:
89: \bibitem{Decorte:DeSchreye}
90: S.~Decorte and D.~De~Schreye.
91: \newblock Demand-driven and constraint-based automatic left termination
92: analysis for logic programs.
93: \newblock In L.~Naish, editor, {\em Proceedings of the Fourteenth International
94: Conference on Logic Programming}, pages 78--92. MIT Press, July 1997.
95:
96: \bibitem{Dershowitz}
97: N.~Dershowitz.
98: \newblock Orderings for term-rewriting systems.
99: \newblock {\em Theoretical {C}omputer {S}cience}, 17(3):279--301, 1982.
100:
101: \bibitem{Giesl}
102: J.~Giesl.
103: \newblock Termination of nested and mutually recursive algorithms.
104: \newblock {\em {J}ournal of {A}utomated {R}easoning}, 19:1--29, 1997.
105:
106: \bibitem{CLP:Manual}
107: C.~Holzbaur.
108: \newblock O{F}{A}{I} {CLP(Q,R)} {M}anual.
109: \newblock Technical Report TR-95-09, Austrian Research Institute for Artificial
110: Intelligence, Vienna, 1995.
111:
112: \bibitem{Jaffar:Maher}
113: J.~Jaffar and M.~J. Maher.
114: \newblock Constraint logic programming: A survey.
115: \newblock {\em The {J}ournal of {L}ogic {P}rogramming}, 19/20:503--582,
116: May/July 1994.
117:
118: \bibitem{Knuth}
119: D.~E. Knuth.
120: \newblock Textbook examples of recursion.
121: \newblock In V.~Lifschitz, editor, {\em {A}rtificial {I}ntelligence and
122: {M}athematical {T}heory of {C}omputation. {P}apers in {H}onor of {J}ohn
123: {M}c{C}arthy}, pages 207--229. {A}cademic {P}ress, {I}nc., 1991.
124:
125: \bibitem{Lindenstrauss:Sagiv}
126: N.~Lindenstrauss and Y.~Sagiv.
127: \newblock Automatic termination analysis of logic programs.
128: \newblock In L.~Naish, editor, {\em Proceedings of the Fourteenth International
129: Conference on Logic Programming}, pages 63--77. MIT Press, July 1997.
130:
131: \bibitem{Lindenstrauss:Sagiv:Serebrenik}
132: N.~Lindenstrauss, Y.~Sagiv, and A.~Serebrenik.
133: \newblock {\em TermiLog\/}: A system for checking termination of queries to
134: logic programs.
135: \newblock In O.~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: N.~Lindenstrauss, Y.~Sagiv, and A.~Serebrenik.
141: \newblock Unfolding mystery of the {\em mergesort\/}.
142: \newblock In N.~Fuchs, editor, {\em Proceedings of the Seventh International
143: Workshop on Logic Program Synthesis and Transformation}. Springer Verlag,
144: 1998.
145: \newblock Lecture Notes in Computer Science, volume 1463.
146:
147: \bibitem{Manna:McCarthy}
148: Z.~Manna and J.~McCarthy.
149: \newblock Properties of {P}rograms and partial function logic.
150: \newblock {\em Machine Intelligence}, 5:27--37, 1970.
151:
152: \bibitem{Mesnard:Ganascia}
153: F.~Mesnard and J.~Ganascia.
154: \newblock {CLP(Q)} for proving interargument relations.
155: \newblock In A.~Petrossi, editor, {\em Proceedings {META}'92}, pages 309--320.
156: Springer Verlag, 1992.
157:
158: \bibitem{Plumer:Book}
159: L.~Pl{\"u}mer.
160: \newblock {\em Termination Proofs for Logic Programs}.
161: \newblock Lecture Notes in Artificial Intelligence, volume 446. Springer
162: Verlag, 1990.
163:
164: \bibitem{Plumer:ICLP}
165: L.~Pl{\"u}mer.
166: \newblock Termination proofs for logic programs based on predicate
167: inequalities.
168: \newblock In {\em Proceedings of ICLP'90}, pages 634--648. MIT Press, 1990.
169:
170: \bibitem{Plumer}
171: L.~Pl{\"u}mer.
172: \newblock Automatic termination proofs for prolog programs operating on
173: nonground terms.
174: \newblock In {\em International Logic Programming Symposium}. MIT Press, 1991.
175:
176: \bibitem{XSB:Manual}
177: K.~F. Sagonas, T.~Swift, and D.~S. Warren.
178: \newblock {\em The XSB Programmer's Manual. Version 1.3 ($\beta$)}.
179: \newblock Department of Computer Science, SUNY @ Stony Brook, U.S.A., September
180: 1993.
181:
182: \bibitem{SICStus:Manual}
183: {SICS}.
184: \newblock {\em User Manual. Version 3.7.1}.
185: \newblock Swedish Institute of Computer Science, 1998.
186:
187: \bibitem{Tamaki:Sato}
188: H.~Tamaki and T.~Sato.
189: \newblock Unfold/{F}old transformation of logic programs.
190: \newblock In S.-{\AA}. T{\"a}rnlund, editor, {\em Proceedings of the Second
191: International Logic Programming Conference}, pages 127--138. Uppsala
192: University, 1984.
193:
194: \bibitem{Ullman:van:Gelder}
195: J.~D. Ullman and A.~van Gelder.
196: \newblock Efficient tests for top-down termination of logical rules.
197: \newblock {\em Journal of the {A}ssociation for {C}omputing {M}achinery},
198: 35(2):345--373, April 1988.
199:
200: \bibitem{Vershaetse:DeSchreye}
201: K.~Verschaetse and D.~De~Schreye.
202: \newblock Deriving termination proofs for logic programs, using abstract
203: procedures.
204: \newblock In K.~Furukawa, editor, {\em Logic Programming, Proceedings of the
205: Eigth International Conference}, pages 301--315. MIT Press, 1991.
206:
207: \bibitem{Vershaetse:DeSchreye:Deriving:Linear:Size:Relations}
208: K.~Verschaetse and D.~De~Schreye.
209: \newblock Deriving of linear size relations by abstract interpretation.
210: \newblock In M.~Bryunooghe and M.~Wirsing, editors, {\em Programming Language
211: Implementation and Logic Programming, 4th International Symposium}, pages
212: 296--310. Springer Verlag, 1992.
213: \newblock Lecture Notes in Computer Science, volume 631.
214:
215: \end{thebibliography}
216: