1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citename{Abadi \& Cardelli, }1996]{abadi-cardelli-objects}
4: Abadi, Mart\'{\i}n, \& Cardelli, Luca. (1996).
5: \newblock {\em A theory of objects}.
6: \newblock Berlin: Springer.
7:
8: \bibitem[\protect\citename{Andrews, }1991]{andrews-phd-dd}
9: Andrews, James~H. (1991).
10: \newblock {\em Logic programming: Operational semantics and proof theory}.
11: \newblock Distinguished Dissertation Series.
12: \newblock Cambridge University Press.
13:
14: \bibitem[\protect\citename{Andrews, }1995]{andrews-cut-ilps95}
15: Andrews, James~H. (1995).
16: \newblock A paralogical semantics for the {Prolog} cut.
17: \newblock {\em Pages 591--605 of:} {\em Proceedings of the international logic
18: programming symposium}.
19: \newblock Portland: MIT Press.
20:
21: \bibitem[\protect\citename{Andrews, }1997]{andrews-lnaf-tcs}
22: Andrews, James~H. (1997).
23: \newblock A logical semantics for depth-first {Prolog} with ground negation.
24: \newblock {\em Theoretical computer science}, {\bf 184}(1-2), 105--143.
25:
26: \bibitem[\protect\citename{Andrews, }1998]{andrews-spreadsheet-uitp}
27: Andrews, James~H. 1998 (July).
28: \newblock On the spreadsheet presentation of proof obligations.
29: \newblock {\em Pages 34--41 of:} Backhouse, Roland (ed), {\em Proceedings of
30: the 1998 workshop on user interfaces for theorem provers ({UITP})}.
31: \newblock Computing Science Report 98-08, Department of Mathematics and
32: Computing Science, Eindhoven University of Technology.
33:
34: \bibitem[\protect\citename{Andrews, }1999]{andrews-cut-tr}
35: Andrews, James~H. 1999 (July).
36: \newblock {\em The witness properties and the semantics of the {Prolog} cut}.
37: \newblock Tech. rept. 542. Department of Computer Science, University of
38: Western Ontario.
39:
40: \bibitem[\protect\citename{Apt \& Pedreschi, }1993]{apt-strong-info-comp}
41: Apt, Krzysztof, \& Pedreschi, Dino. (1993).
42: \newblock Proving termination of general {P}rolog programs.
43: \newblock {\em Information and computation}, {\bf 106}, 109--157.
44:
45: \bibitem[\protect\citename{Apt \& Marchiori, }1994]{apt-marchiori}
46: Apt, Krzysztof~R., \& Marchiori, Elena. (1994).
47: \newblock Reasoning about {Prolog} programs: From modes through types to
48: assertions.
49: \newblock {\em Formal aspects of computing}, {\bf 6A}, 743--764.
50:
51: \bibitem[\protect\citename{Arbab \& Berry, }1987]{denotationalization}
52: Arbab, Bijan, \& Berry, Daniel~M. (1987).
53: \newblock Operational and denotational semantics of {P}rolog.
54: \newblock {\em Journal of logic programming}, {\bf 4}, 309--329.
55:
56: \bibitem[\protect\citename{Barbuti \& Martelli, }1990]{barbuti-martelli-1990}
57: Barbuti, Roberto, \& Martelli, Maurizio. (1990).
58: \newblock Recognizing non-floundering logic programs and goals.
59: \newblock {\em International journal on the foundations of computer science},
60: {\bf 1}(2), 151--163.
61:
62: \bibitem[\protect\citename{Baudinet, }1992]{baudinet-jlp}
63: Baudinet, Marianne. (1992).
64: \newblock Proving termination properties of {P}rolog programs: A semantic
65: approach.
66: \newblock {\em Journal of logic programming}, {\bf 14}(1), 1--29.
67:
68: \bibitem[\protect\citename{Belnap, }1977]{belnap-four-valued}
69: Belnap, Jr., Nuel~D. (1977).
70: \newblock A useful four-valued logic.
71: \newblock {\em Pages 8--37 of:} Dunn, J.~Michael, \& Epstein, George (eds),
72: {\em Modern uses of multiple-valued logic}.
73: \newblock Dordrecht: Reidel.
74:
75: \bibitem[\protect\citename{Bezem, }1993]{bezem-strong-jlp}
76: Bezem, Marc. (1993).
77: \newblock Strong termination of logic programs.
78: \newblock {\em Journal of logic programming}, {\bf 15}, 79--97.
79:
80: \bibitem[\protect\citename{Billaud, }1990]{billaud-cut-tcs}
81: Billaud, Michel. (1990).
82: \newblock Simple operational and denotational semantics for {P}rolog with cut.
83: \newblock {\em Theoretical computer science}, {\bf 71}, 193--208.
84:
85: \bibitem[\protect\citename{B{\"{o}}rger, }1990]{boerger-opsem}
86: B{\"{o}}rger, Egon. 1990 (March).
87: \newblock {\em A logical operational semantics of full {P}rolog}.
88: \newblock Tech. rept. IWBS Report 111. IBM Wissenschaftliches Zentrum, Institut
89: f{\"{u}}r Wissensbasierte Systeme, Heidelberg, Germany.
90:
91: \bibitem[\protect\citename{Burstall \& Darlington, }1977]{burstall-darlington}
92: Burstall, Rod~M., \& Darlington, John. (1977).
93: \newblock A transformation system for developing recursive programs.
94: \newblock {\em Journal of the {ACM}}, {\bf 24}(1), 44--67.
95:
96: \bibitem[\protect\citename{Clark, }1978]{clark-negfail}
97: Clark, Keith~L. (1978).
98: \newblock Negation as failure.
99: \newblock {\em Pages 293--322 of:} {\em Logic and data bases}.
100: \newblock New York: Plenum Press.
101:
102: \bibitem[\protect\citename{Dahl, }1980]{dahl-negation}
103: Dahl, Ver\'onica. 1980 (July).
104: \newblock Two solutions for the negation problem.
105: \newblock {\em Workshop on logic programming}.
106:
107: \bibitem[\protect\citename{de~Bruin \& de~Vink, }1989]{prolog-continuation}
108: de~Bruin, Arie, \& de~Vink, Erik~P. (1989).
109: \newblock Continuation semantics for {P}rolog with cut.
110: \newblock {\em Pages 178--192 of:} {\em Theory and practice of software
111: engineering}.
112: \newblock Lecture Notes in Computer Science, vol. 351.
113: \newblock Barcelona, Spain: Springer-Verlag.
114:
115: \bibitem[\protect\citename{Debray \& Mishra, }1988]{debray-denotational}
116: Debray, Saumya, \& Mishra, Prateek. (1988).
117: \newblock Denotational and operational semantics of {P}rolog.
118: \newblock {\em Journal of logic programming}, {\bf 5}, 61--91.
119:
120: \bibitem[\protect\citename{Deransart \& Ferrand, }1987]{deransart-std-inria}
121: Deransart, Pierre, \& Ferrand, G\'{e}rard. (1987).
122: \newblock {\em An operational formal definition of {P}rolog}.
123: \newblock Tech. rept. RR763. INRIA.
124:
125: \bibitem[\protect\citename{Elbl, }1999]{elbl-jlp-1999}
126: Elbl, Birgit. (1999).
127: \newblock A declarative semantics for depth-first logic programs.
128: \newblock {\em Journal of logic programming}, {\bf 41}(1), 27--66.
129:
130: \bibitem[\protect\citename{Etalle, }1998]{etalle-modular-general}
131: Etalle, Sandro. (1998).
132: \newblock A semantics for modular general logic programs.
133: \newblock {\em Theoretical computer science}, {\bf 206}(1-2), 51--80.
134:
135: \bibitem[\protect\citename{Fitting, }1985]{fitting-kripke}
136: Fitting, Melvin. (1985).
137: \newblock A {K}ripke-{K}leene semantics for logic programs.
138: \newblock {\em Journal of logic programming}, {\bf 4}, 295--312.
139:
140: \bibitem[\protect\citename{Gabbrieli \& Levi, }1992]{levi-unfold-tcs92}
141: Gabbrieli, Maurizio, \& Levi, Giorgio. (1992).
142: \newblock Unfolding and fixpoint semantics of concurrent constraint logic
143: programs.
144: \newblock {\em Theoretical computer science}, {\bf 105}, 85--128.
145:
146: \bibitem[\protect\citename{Gabbrielli \& Etalle, }1999]{gabbrielli-etalle-1999}
147: Gabbrielli, Maurizio, \& Etalle, Sandro. (1999).
148: \newblock Layered modes.
149: \newblock {\em Journal of logic programming}, {\bf 39}(1-3), 225--244.
150:
151: \bibitem[\protect\citename{Jones \& Mycroft, }1984]{jones-mycroft}
152: Jones, Neil~D., \& Mycroft, Alan. (1984).
153: \newblock Stepwise development of operational and denotational semantics for
154: {P}rolog.
155: \newblock {\em Pages 281--288 of:} {\em Proceedings of the 1984 international
156: symposium on logic programming}.
157: \newblock Atlantic City, New Jersey: IEEE Computer Society.
158:
159: \bibitem[\protect\citename{Kripke, }1975]{kripke}
160: Kripke, Saul. (1975).
161: \newblock Outline of a theory of truth.
162: \newblock {\em Journal of philosophy}, {\bf 72}, 690--716.
163:
164: \bibitem[\protect\citename{Lindenstrauss \& Sagiv,
165: }1997]{lindenstrauss-auto-term-iclp97}
166: Lindenstrauss, Naomi, \& Sagiv, Yehoshua. (1997).
167: \newblock Automatic termination analysis of logic programs.
168: \newblock {\em Pages 63--77 of:} Naish, Lee (ed), {\em Proceedings of the
169: fourteenth international conference on logic programming}.
170: \newblock Leuven, Belgium: MIT Press.
171:
172: \bibitem[\protect\citename{Lindenstrauss {\em et~al.}\relax,
173: }1997]{lindenstrauss-termilog-cav97}
174: Lindenstrauss, Naomi, Sagiv, Yehoshua, \& Serebrenik, Alexander. (1997).
175: \newblock Termilog: A system for checking termination of queries to logic
176: programs.
177: \newblock {\em Pages 444--447 of:} Grumberg, Orna (ed), {\em Computer aided
178: verification, 9th international conference}.
179: \newblock LNCS, no. 1254.
180: \newblock Haifa, Israel: Springer-Verlag.
181:
182: \bibitem[\protect\citename{Loveland \& Reed, }1991]{loveland-near-horn}
183: Loveland, Donald~W., \& Reed, David~W. (1991).
184: \newblock A near-{Horn} {Prolog} for compliation.
185: \newblock {\em Pages 542--564 of:} {\em Computational logic: Essays in honor
186: of {Alan} {Robinson}}.
187: \newblock Cambridge, Mass.: MIT Press.
188:
189: \bibitem[\protect\citename{Naish, }1986]{naish-negation-lncs}
190: Naish, Lee. (1986).
191: \newblock {\em Negation and control in {Prolog}}.
192: \newblock Lecture Notes in Computer Science, no. 238.
193: \newblock Springer.
194:
195: \bibitem[\protect\citename{Nicholson \& Foo, }1989]{nicholson-foo}
196: Nicholson, Tim, \& Foo, Norman. (1989).
197: \newblock A denotational semantics for {P}rolog.
198: \newblock {\em {ACM} transactions on programming languages and systems}, {\bf
199: 11}(October), 650--665.
200:
201: \bibitem[\protect\citename{Pereira {\em et~al.}\relax, }n.d.]{c-prolog}
202: Pereira, Fernando, Warren, David, Bowen, David, Byrd, Lawrence, \& Pereira,
203: Luis.
204: \newblock {\em {C-Prolog} user's manual}.
205: \newblock Tech. rept. EdCAAD, Dept. of Architecture, Univ. of Edinburgh,
206: Edinburgh.
207:
208: \bibitem[\protect\citename{Pierro {\em et~al.}\relax, }1995]{IC::PierroMP1995}
209: Pierro, Alessandra~Di, Martelli, Maurizio, \& Palamidessi, Catuscia. (1995).
210: \newblock Negation as instantiation.
211: \newblock {\em Information and computation}, {\bf 120}(2), 263--278.
212:
213: \bibitem[\protect\citename{Plotkin, }1981]{plotkin-opsem}
214: Plotkin, Gordon. 1981 (September).
215: \newblock {\em A structural approach to operational semantics}.
216: \newblock Tech. rept. DAIMI FN-19. Computer Science Department, Aarhus
217: University, Aarhus.
218:
219: \bibitem[\protect\citename{Pl{\"{u}}mer, }1990]{pluemer-lncs}
220: Pl{\"{u}}mer, Lutz. (1990).
221: \newblock {\em Termination proofs for logic programs}.
222: \newblock Lecture Notes in Artificial Intelligence, vol. 446.
223: \newblock Berlin: Springer-Verlag.
224:
225: \bibitem[\protect\citename{Somogyi {\em et~al.}\relax, }1996]{mercury-jlp}
226: Somogyi, Zoltan, Henderson, Fergus, \& Conway, Thomas. (1996).
227: \newblock The execution algorithm of {Mercury}, an efficient purely declarative
228: logic programming language.
229: \newblock {\em Journal of logic programming}, {\bf 29}(1-3), 17--64.
230:
231: \bibitem[\protect\citename{St{\"a}rk, }1998]{staerk-lptp-jlp}
232: St{\"a}rk, Robert. (1998).
233: \newblock The theoretical foundations of {LPTP} (a logic program theorem
234: prover).
235: \newblock {\em Journal of logic programming}, {\bf 36}(3), 241--269.
236:
237: \bibitem[\protect\citename{Tamaki \& Sato, }1984]{tamaki-sato-unfold}
238: Tamaki, Hisao, \& Sato, Taisuke. (1984).
239: \newblock Unfold/fold transformations of logic programs.
240: \newblock {\em Pages 127--138 of:} {\em Proceedings of the second
241: international logic programming conference}.
242: \newblock Uppsala, Sweden: Uppsala University.
243:
244: \bibitem[\protect\citename{van Emden \& Kowalski, }1976]{vanE-kow}
245: van Emden, Maarten~H., \& Kowalski, Robert~A. (1976).
246: \newblock The semantics of predicate logic as a programming language.
247: \newblock {\em Journal of the association for computing machinery}, {\bf
248: 23}(4), 733--742.
249:
250: \end{thebibliography}
251: