\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{MPRT90b}

\bibitem[AAB92]{Anderson92}
J.~M.~Dunn A.~Anderson and N.D. Belnap.
\newblock {\em Entailment. The Logic of Relevance and Necessity}, volume~2.
\newblock Princeton University Press, 1992.

\bibitem[AAB{\etalchar{+}}95]{sics}
Johan Andersson, Stefan Andersson, Kent Boortz, Mats Carlsson, Hans Nilsson,
  Thomas Sj{\"o}land, and Johan Widen.
\newblock {SICS}tus prolog user's manual.
\newblock Technical Report T93-01, Swedish Institute of Computer Science, 1995.

\bibitem[AB75]{Anderson75}
A.~Anderson and N.D. Belnap.
\newblock {\em Entailment. The Logic of Relevance and Necessity}, volume~1.
\newblock Princeton University Press, 1975.

\bibitem[AB90]{Apt90iclp}
Krzysztof~R. Apt and Marc Bezem.
\newblock Acyclic programs.
\newblock In Peter {Warren, David H.D.; Szerdei}, editor, {\em Proceedings of
  the 7th International Conference on Logic Programming ({ICLP} '90)}, pages
  617--633, Jerusalem, June 1990. MIT Press.

\bibitem[AB94]{Apt94}
K.~Apt and R.~Bol.
\newblock Logic programming and negation.
\newblock {\em Journal of Logic Programming}, 19/20:9--72, May/July 1994.

\bibitem[ABT90]{Brogi90}
D.~Pedreschi A.~Brogi, P.~Mancarella and F.~Turini.
\newblock Universal quantification by case analysis.
\newblock In {\em Proc. ECAI-90}, pages 111--116, 1990.

\bibitem[ABW88]{Apt88}
K.~{A}pt, {H}. {B}lair, and {A}. {W}alker.
\newblock {T}owards a theory of declarative knowledge.
\newblock In Jack {M}inker, editor, {\em Foundations of {D}eductive
  {D}atabases}, chapter~2, pages 89--148. Morgan {K}aufmann, 1988.

\bibitem[ACCL91]{Abadi91}
M.~Abadi, L.~Cardelli, P.-L. Curien, and J.-J. L{\'e}vy.
\newblock Explicit substitutions.
\newblock {\em Journal of Functional Programming}, 1(4):375--416, 1991.

\bibitem[Acz77]{Acz77}
Peter Aczel.
\newblock An introduction to inductive definitions.
\newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic},
  volume~90 of {\em Studies in Logic and the Foundations of Mathematics},
  chapter C.7, pages 739--782. North-Holland, Amsterdam, 1977.

\bibitem[AF99]{Appel99iclp}
Andrew~W. Appel and Amy~P. Felty.
\newblock Lightweight lemmas in lambda prolog.
\newblock In Danny~De Schreye, editor, {\em Proceedings of the International
  Conference on Logic Programming (ICLP'99)}, pages 411--425, Las Cruces, New
  Mexico, December 1999. MIT Press.

\bibitem[Apt90]{Apt90}
Krzysztof~R. Apt.
\newblock Logic programming.
\newblock In J.~van Leewen, editor, {\em Handbook of Theoretical Computer
  Science}, volume B: Formal Models and Semantics, chapter~10, pages 493--574.
  The MIT Press, New York, N.Y., 1990.

\bibitem[Bar80]{Barendregt80}
H.~P. Barendregt.
\newblock {\em The Lambda-Calculus: Its Syntax and Semantics}.
\newblock North-Holland, 1980.

\bibitem[BDLM00]{Bugliesi00}
Bugliesi, Delzanno, Liquori, and Martelli.
\newblock Object calculi in linear logic.
\newblock {\em JLC: Journal of Logic and Computation}, 10, 2000.

\bibitem[Bel74]{Belnap74}
N.D. Belnap.
\newblock Functions which really depend on their argument.
\newblock Manuscript, 1974.

\bibitem[Bel93]{Belnap93}
N.~D. Belnap.
\newblock Life in the undistributed middle.
\newblock In K.~Dosen and P.~Schroeder-Heister, editors, {\em Substructural
  Logics}, pages 31--42. Oxford University Press, 1993.

\bibitem[BF93]{Baker94}
Clement~A. Baker-Finch.
\newblock Relevance and contraction: A logical basis for strictness and sharing
  analysis.
\newblock Technical Report ISE RR 34/94, University of Canberra, 1993.

\bibitem[BLLM94]{Bruscoli94}
P.~Bruscoli, F.~Levi, G.~Levi, and M.~C. Meo.
\newblock Compilative constructive negation in constraint logic programs.
\newblock In Sophie Tiso, editor, {\em Proc. Trees in Algebra and Programming -
  CAAP'94, 19th International Colloquium}, volume 787, pages 52--76. Springer,
  1994.

\bibitem[BM90]{Bonner90}
Anthony~J. Bonner and L.~Thorne McCarty.
\newblock Adding negation-as-failure to intuitionistic logic programming.
\newblock In Saumya~Hermenegildo Manuel~Debray, editor, {\em Proceedings of the
  1990 North American Conference on Logic Programming}, pages 671--693, Austin,
  TX, October 1990. MIT Press.

\bibitem[BMPT87]{Barbuti87}
R.~Barbuti, Paolo Mancarella, Dino Pedreschi, and Franco Turini.
\newblock Intensional negation of logic programs.
\newblock In {\em Proceedings ofTapsoft87}, volume 259 of {\em LNCS}, pages
  96--110, Austin, TX, October 1987. Springer Verlag Press.

\bibitem[BMPT90]{Bar90}
Roberto Barbuti, Paolo Mancarella, Dino Pedreschi, and Franco Turini.
\newblock {A} transformational approach to negation in logic programming.
\newblock {\em Journal of Logic Programming}, 8:201--228, 1990.

\bibitem[BMV89]{Bonner89}
A.~J. Bonner, L.~T. McCarty, and K.~Vadaparty.
\newblock Expressing {D}atabase {Q}ueries with {I}ntuitionistic {L}ogic.
\newblock In Ewing~L. Lusk and Ross~A. Overbeek, editors, {\em Proceedings of
  the North American Conference on Logic Programming}, pages 831--850,
  Cleveland, Ohio, USA, 1989.

\bibitem[Bol88]{Bollen87}
A.~W. Bollen.
\newblock {\em Conditional Logic Programming}.
\newblock PhD thesis, Australian National University, 1988.

\bibitem[Bol90]{Bollen91}
A.~W. Bollen.
\newblock Relevant logic programming.
\newblock {\em Journal of Automated Reasoning}, 7(4):563--586, December 1990.

\bibitem[Bon91]{Bonner91phd}
A.J. Bonner.
\newblock {\em Hypothetical Reasoning in Deductive Databases}.
\newblock PhD thesis, Rutgers University, October 1991.

\bibitem[Bon94]{Bonner94}
A.J. Bonner.
\newblock Hypothetical reasoning with intuitionistic logic.
\newblock In R.~Demolombe and T.~Imielinski, editors, {\em Non-Standard Queries
  and Answers}, volume 306 of {\em Studies in Logic and Computation}, pages
  187--219. Oxford University Press, 1994.

\bibitem[BR57]{Rasiowa57}
A.~{Bia{l}ynicki-Birula} and H.~Rasiowa.
\newblock On the representation of quasi-boolean algebras.
\newblock {\em Bulletin de L'acad{\'{e}}mie Polonaise des Sciences},
  5:259--261, 1957.

\bibitem[CdPR99]{Cervesato99lfm}
Iliano Cervesato, Valeria de~Paiva, and Eike Ritter.
\newblock Explicit substitutions for linear logical frameworks: Preliminary
  results.
\newblock In A.~Felty, editor, {\em Proceedings of the Worskshop on Logical
  Frameworks and Meta-Languages --- LFM'99}, Paris, France, 28 September 1999.

\bibitem[Cer96]{Cervesato96phd}
Iliano Cervesato.
\newblock {\em A Linear Logical Framework}.
\newblock PhD thesis, Dipartimento di Informatica, Universit{\`a} di Torino,
  February 1996.

\bibitem[CF58]{Curry58}
H.~B. Curry and R.~Feys.
\newblock {\em Combinatory Logic}.
\newblock North-Holland, Amsterdam, 1958.

\bibitem[Cha88]{Chan88}
D.~Chan.
\newblock Constructive negation based on the completed databases.
\newblock In R.~A. Kowalski and K.~A. Bowen, editors, {\em Proc. Fifth
  International Conference and Symposium on Logic Programming}, pages 111--125,
  Seattle, Washington, August 15-19 1988.

\bibitem[Cha89]{Chan89}
D.~Chan.
\newblock An {E}xtension of {C}onstructive {N}egation and its {A}pplication in
  {C}oroutining.
\newblock In Ewing~L. Lusk and Ross~A. Overbeek, editors, {\em Proceedings of
  the North American Conference on Logic Programming}, pages 477--496,
  Cleveland, Ohio, USA, 1989.

\bibitem[CHP97]{Cervesato97tcs}
Iliano Cervesato, Joshua~S. Hodas, and Frank Pfenning.
\newblock Efficient resource management for linear logic proof search.
\newblock {\em Theoretical Computer Science}, 1997.
\newblock To appear in a special issue on Proof Search in Type-Theoretic
  Languages, D. Galmiche, editor.

\bibitem[Chu41]{Church41}
A.~Church.
\newblock {\em The Calculi of Lambda Conversion}.
\newblock Princeton University Press, 1941.

\bibitem[Chu51]{Church51}
A.~Church.
\newblock The weak theory of implication.
\newblock In {\em Kontrolliertes}. Karl Albert, 1951.

\bibitem[CKW93]{Chen93}
Weidong Chen, Michael Kifer, and David~S. Warren.
\newblock Hilog: {A} foundation for higher-order logic programming.
\newblock {\em Journal of Logic Programming}, 15(3):187--230, February 1993.

\bibitem[CL89]{CL89}
Hubert Comon and Pierre Lescanne.
\newblock Equational problems and disunification.
\newblock {\em Journal of Symbolic Computation}, 7(3--4):371--425 (or
  371--426??), March--April 1989.

\bibitem[Cla78]{Cla78}
K.~L. Clark.
\newblock Negation as failure.
\newblock In H.~Gallaire and J.~Minker, editors, {\em Logic and Databases},
  pages 293--322. Plenum Press, New York, 1978.

\bibitem[Col84]{Col84}
A.~Colmerauer.
\newblock {Equations and Inequations on Finite and Infinite Trees}.
\newblock In {\em {Proceedings of the International Conference on Fifth
  Generation Computer Systems (FGCS-84)}}, pages 85--99, Tokyo, Japan, November
  1984. ICOT.

\bibitem[Com88]{Comon88}
H.~Comon.
\newblock {\em Unification et disunification. {T}h\'eories et applications}.
\newblock {T}h\`ese de {D}octorat d'{U}niversit\'e, Institut Polytechnique de
  Grenoble (France), 1988.

\bibitem[Com91]{Comon91}
H.~Comon.
\newblock Disunification: a survey.
\newblock In J-L. Lassez and G.Plotkin, editors, {\em Computational Logic}. MIT
  Press, Cambridge,MA, 1991.

\bibitem[Com98]{Comon98}
H.~Comon.
\newblock About proofs by consistency.
\newblock {\em Lecture Notes in Computer Science}, 1379:136--??, 1998.

\bibitem[CP96]{Cervesato96lics}
Iliano Cervesato and Frank Pfenning.
\newblock A linear logical framework.
\newblock In E.~Clarke, editor, {\em Proceedings of the Eleventh Annual
  Symposium on Logic in Computer Science}, pages 264--275, New Brunswick, New
  Jersey, July 1996. IEEE Computer Society Press.

\bibitem[dB80]{DeBruijn80}
N.G. de~Bruijn.
\newblock A survey of the project {AUTOMATH}.
\newblock In J.P. Seldin and J.R. Hindley, editors, {\em To H.B. Curry: Essays
  in Combinatory Logic, Lambda Calculus and Formalism}, pages 579--606.
  Academic Press, 1980.

\bibitem[dB91]{DeBruijn91lf}
N.G. de~Bruijn.
\newblock A plea for weaker frameworks.
\newblock In G.~Huet and G.~Plotkin, editors, {\em Logical Frameworks}, pages
  40--67. Cambridge University Press, 1991.

\bibitem[DM97]{MacDowell97lics}
Raymond Dowell and Dale Miller.
\newblock A logic for reasoning with higher-order abstract syntax: An extended
  abstract.
\newblock In Glynn Winskel, editor, {\em Proceedings of the Twelfth Annual
  Symposium on Logic in Computer Science}, pages 434--445, Warsaw, Poland, June
  1997.

\bibitem[DPS97]{Despeyroux97}
Jo{\"e}lle Despeyroux, Frank Pfenning, and Carsten Sch{\"u}rmann.
\newblock Primitive recursion for higher-order abstract syntax.
\newblock In R.~Hindley, editor, {\em Proceedings of the Third International
  Conference on Typed Lambda Calculus and Applications (TLCA'97)}, pages
  147--163, Nancy, France, April 1997. Springer-Verlag LNCS.
\newblock An extended version is available as Technical Report CMU-CS-96-172,
  Carnegie Mellon University.

\bibitem[Dun92]{Dung92}
P.~M. Dung.
\newblock Declarative semantics of hypothetical logic programming with negation
  as failure.
\newblock In E.~Lamma and P.~Mello, editors, {\em Proceedings of the Third
  International Workshop on Extensions of Logic Programming ({ELP} '92)},
  volume 660 of {\em LNAI}, pages 45--58, Bologna, Italy, February 1992.
  Springer Verlag.

\bibitem[Eri93]{Eriksson93phd}
Lars-Henrik Eriksson.
\newblock {\em Finitary Partial Inductive Definitions and General Logic}.
\newblock PhD thesis, Department of Computer and System Sciences, Royal
  Institute of Technology, Stockholm, 1993.

\bibitem[Fag97]{Fages97}
Fran{\c{c}}ois Fages.
\newblock Constructive negation by pruning.
\newblock {\em Journal of Logic Programming}, 32(2):85--118, August 1997.

\bibitem[FBM93]{Bruscoli93}
G.~Levi F.~Bruscoli, F.~Levi and M.C. Meo.
\newblock Intensional negation in constraint logic programming.
\newblock In D.~Sacca, editor, {\em Proc. GULP93}, pages 359--373, 1993.

\bibitem[FRTW88]{Foo88}
Norman Foo, Anand Rao, Andrew Taylor, and Adrian Walker.
\newblock Deduced relevant types and constructive negation.
\newblock In Robert~A. Kowalski and Kenneth~A. Bowen, editors, {\em Proceedings
  of the Fifth International Conference and Symposium on Logic Programming},
  pages 126--139, Seatle, 1988. ALP, IEEE, The MIT Press.

\bibitem[Gab85]{Gabbay85}
Dov~M. Gabbay.
\newblock N-{P}rolog: An extension of {P}rolog with hypothetical implications
  {II}. {L}ogical foundations and negation as failure.
\newblock {\em Journal of Logic Programming}, 2(4):251--283, December 1985.

\bibitem[Gab91]{Gabbay91elp}
Dov Gabbay.
\newblock Modal provability foundations for negation by failure, in extensions
  of logic programming.
\newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
  Programming: International Workshop, T{\"u}bingen FRG, December 1989}, volume
  475 of {\em Lecture Notes in Artificial Intelligence}, pages 179--222.
  Springer-Verlag, 1991.

\bibitem[GdQ92]{Gabbay92}
Dov~M. Gabbay and Ruy J. G.~B. de~Queiroz.
\newblock Extending the {Curry-Howard} interpretation to linear, relevant and
  other resource logics.
\newblock {\em The Journal of Symbolic Logic}, 57(4):1319--1365, December 1992.

\bibitem[GH78]{GH78}
J.~Guttag and J.~Horning.
\newblock The algebraic specification of abstract data types.
\newblock {\em Acta Informatica}, 10(1):27--52, 1978.

\bibitem[GL90]{Gelfond90}
Michael Gelfond and Vladimir Lifschitz.
\newblock Logic programs with classical negation.
\newblock In David H.D.~Szerdei Peter~Warren, editor, {\em Proceedings of the
  7th International Conference on Logic Programming (ICLP '90)}, pages
  579--597, Jerusalem, June 1990. MIT Press.

\bibitem[GMR92]{Giordano92}
L.~Giordano, A.~Martelli, and G.~Rossi.
\newblock Extending {Horn} clause logic with implication goals.
\newblock {\em Theoretical Computer Science}, 95(1):43--74, March 1992.

\bibitem[GO98]{Giordano98}
Laura Giordano and Nicola Olivetti.
\newblock Negation as failure and embedded implication.
\newblock {\em Journal of Logic Programming}, 36(2):91--147, August 1998.

\bibitem[GPR98]{Ghani98}
Neil Ghani, Valeria~De Paiva, and Eike Ritter.
\newblock Linear explicit subsitutions.
\newblock Technical Report CSR-98-2, University of Birmingham, School of
  Computer Science, March 1998.

\bibitem[GR84]{Gabbay84}
Dov~M. Gabbay and U.~Reyle.
\newblock N-{P}rolog: An extension of {P}rolog with hypothetical implications
  {I}.
\newblock {\em Journal of Logic Programming}, 1(4):319--355, December 1984.

\bibitem[GR87]{Gallier87}
Jean~H. Gallier and Stan Raatz.
\newblock Hornlog: {A} graph-based interpreter for general {Horn} clauses.
\newblock {\em Journal of Logic Programming}, 4(2):119--155, June 1987.

\bibitem[GS86]{Gabbay86}
Dov~M. Gabbay and Marek~J. Sergot.
\newblock Negation as inconsistency {I}.
\newblock {\em Journal of Logic Programming}, 3(1):1--35, April 1986.

\bibitem[Hal91]{Halnass91}
L.~Hallnas.
\newblock Partial inductive definitions.
\newblock {\em Theoretical Computer Science}, 87(1):115--147, July 1991.

\bibitem[Har89]{Harland89}
J.~Harland.
\newblock A {K}ripke-like {M}odel for {N}egation as {F}ailure.
\newblock In Ewing~L. Lusk and Ross~A. Overbeek, editors, {\em Proceedings of
  the North American Conference on Logic Programming}, pages 626--644,
  Cleveland, Ohio, USA, 1989.

\bibitem[Har91a]{Harland91iclp}
James Harland.
\newblock A clausal form for the completion of logic programs.
\newblock In Koichi Furukawa, editor, {\em Proceedings of the 8th International
  Conference on Logic Programming}, pages 711--725. MIT, June 1991.

\bibitem[Har91b]{Harland91phd}
James Harland.
\newblock {\em On Hereditary Harrop Formulae as a Basis for Logic Programming}.
\newblock PhD thesis, Edinburgh, January 1991.

\bibitem[Har92]{Harland92iclp}
James Harland.
\newblock On normal forms and equivalence for logic programs.
\newblock In Krzysztof Apt, editor, {\em Proceedings of the Joint International
  Conference and Symposium on Logic Programming}, pages 146--160, Washington,
  USA, 1992. The MIT Press.

\bibitem[Har93]{Harland93}
James Harland.
\newblock Success and failure for hereditary {Harrop} formulae.
\newblock {\em Journal of Logic Programming}, 17(1):1--29, October 1993.

\bibitem[Hel77]{Helman77}
G.~Helmann.
\newblock Completeness of the normal typed fragment of the $\lambda$-system
  $u$.
\newblock {\em Journal of Philosophical Logic}, 1977.

\bibitem[Hey56]{Heyting56}
A.~Heyting.
\newblock {\em Intuitionism, an Introduction}.
\newblock North-Holland, Amsterdam, 3 edition, 1956.

\bibitem[HHP93]{Harper93jacm}
Robert Harper, Furio Honsell, and Gordon Plotkin.
\newblock A framework for defining logics.
\newblock {\em Journal of the Association for Computing Machinery},
  40(1):143--184, January 1993.

\bibitem[HM90]{HM90}
Joshua~S. Hodas and Dale Miller.
\newblock Representing objects in a logic programming language with scoping
  constructs.
\newblock In Peter {Warren, David H.D.; Szerdei}, editor, {\em Proceedings of
  the 7th International Conference on Logic Programming ({ICLP} '90)}, pages
  511--528, Jerusalem, June 1990. MIT Press.

\bibitem[HM94]{Hodas94ic}
Joshua Hodas and Dale Miller.
\newblock Logic programming in a fragment of intuitionistic linear logic.
\newblock {\em Information and Computation}, 110(2):327--365, 1994.
\newblock A preliminary version appeared in the Proceedings of the Sixth Annual
  IEEE Symposium on Logic in Computer Science, pages 32--42, Amsterdam, The
  Netherlands, July 1991.

\bibitem[Hod94]{Hodas94phd}
Joshua~S. Hodas.
\newblock {\em Logic Programming in Intuitionistic Linear Logic: Theory,
  Design, and Implementation}.
\newblock PhD thesis, University of Pennsylvania, Department of Computer and
  Information Science, 1994.

\bibitem[HP96]{Hanus96RTA}
M.~Hanus and C.~Prehofer.
\newblock Higher-order narrowing with definitional trees.
\newblock In {\em Proc.\ Seventh International Conference on Rewriting
  Techniques and Applications (RTA'96)}, pages 138--152. Springer LNCS 1103,
  1996.

\bibitem[HP97]{Harland97cade}
J.~Harland and D.~Pym.
\newblock Resource-distribution via {Boolean} constraints.
\newblock In William McCune, editor, {\em Proceedings of the 14th International
  Conference on Automated deduction}, volume 1249 of {\em LNAI}, pages
  222--236, Berlin, July~13--17 1997. Springer.

\bibitem[HSH90]{Halnass90}
L.~Hallnas and P.~Schroeder-Heister.
\newblock A proof-theoretic approach to logic programming: Clauses as rules.
\newblock {\em Journal of Logic and Computation}, 1(2):635\--660, October 1990.

\bibitem[HSH91]{Halnass91jlp}
L.~Hallnas and P.~Schroeder-Heister.
\newblock A proof-theoretic approach to logic programming: Programs as
  definitions.
\newblock {\em Journal of Logic and Computation}, 1(5):261\--283, October 1991.

\bibitem[Isa98]{Isabelle}
Isabelle.
\newblock System home page, October 1998.
\newblock Version 98-1.

\bibitem[Jen91]{Jensen91}
Thomas~P. Jensen.
\newblock {Strictness Analysis in Logical Form}.
\newblock In John Hughes, editor, {\em {Functional Programming Languages and
  Computer Architectures}}, volume 523 of {\em Lecture Notes in Computer
  Science}, pages 352--366, Harvard, Massachusetts, USA, 1991. Springer,
  Berlin.

\bibitem[JLLM91]{Lassez91}
M.J.~Maher J-L.~Lassez and K.~Marriot.
\newblock Elimination of negation in term algebras.
\newblock In A.~Tarlecki, editor, {\em Mathematical Foundations of Computer
  Science}, pages 1--16, Berlin, jul 1991. Springer-Verlag.

\bibitem[Kah87]{KAHN87}
Gilles Kahn.
\newblock Natural semantics.
\newblock In {\em Proceedings of the Symposium on Theoretical Aspects of
  Computer Science}, pages 22--39. Springer-Verlag LNCS 247, 1987.

\bibitem[KL87]{Kir87}
Claude Kirchner and Pierre Lescanne.
\newblock Solving disequations.
\newblock In {\em Proceedings, Symposium on Logic in Computer Science}, pages
  347--352, Ithaca, New York, 22--25 June 1987. The Computer Society of the
  IEEE.

\bibitem[KNW93]{Kwon93}
Keehand Kwon, Gopalan Nadathur, and Debra~Sue Wilson.
\newblock Implementing a notion of modules in the logic programming language
  {$\lambda$Prolog}.
\newblock In E.~Lamma and P.~Mello, editors, {\em Proceedings of the Third
  International Workshop on Extensions of Logic Programming}, pages 359--393,
  Bologna, Italy, February 1993. Springer-Verlag LNAI 660.

\bibitem[Kre92]{Kreuger92}
Per Kreuger.
\newblock {GCLA} {II}. a definitional approach to control.
\newblock Technical Report R92:09, SICS, 1992.

\bibitem[Lia95]{Liang95}
Chuck Liang.
\newblock {\em Object-Level Substitution, Unification and Generalization in
  Meta-Logic}.
\newblock PhD thesis, University of Pennsylvania, August 1995.

\bibitem[Lif99]{Marek99}
Vladimir Lifschitz.
\newblock Answer set planning.
\newblock In D.~De Schreye, editor, {\em Proceedings of the International
  Conference on Logic Programming (ICLP'99)}, pages 23--35. MIT Press, 1999.

\bibitem[Llo93]{Lloyd87}
J.~W. Lloyd.
\newblock {\em Foundations of Logic Programming, Second Extended Edition}.
\newblock Springer-Verlag, 1993.

\bibitem[LM87]{Lassez87}
J.-L. Lassez and K.~Marriot.
\newblock Explicit representation of terms defined by counter examples.
\newblock {\em Journal of Automated Reasoning}, 3(3):301--318, September 1987.

\bibitem[LMR92]{Lobo91}
J.~Lobo, J.~Minker, and A.~Rajasekar.
\newblock {\em Foundations of Disjunctive Logic Programming}.
\newblock MIT press, Cambridge, Massachusetts, 1992.

\bibitem[LT84]{Lloyd84}
J.~W. Lloyd and R.~W. Topor.
\newblock Making {PROLOG} more expressive.
\newblock {\em LOGIC PROGRAM. (USA) ISSN: 0743-1066}, 1(3):225--40, October
  1984.

\bibitem[Lug94]{Lugiez94}
D.~Lugiez.
\newblock Higher-order disunification: Some decidable cases.
\newblock In J.-P. Jouannaud, editor, {\em Proceedings of the First
  International Conference on Constraints in Computational Logics}, pages
  121--135, Munich, Germany, September 1994. Springer-Verlag LNCS 845.

\bibitem[Lug95]{Lug95}
D.~Lugiez.
\newblock Positive and negative results for higher-order disunification.
\newblock {\em Journal of Symbolic Computation}, 20(4):431--470, October 1995.

\bibitem[Mah88]{Maher88}
M.~Maher.
\newblock {C}omplete {A}xiomatizations of the {A}lgebras of finite, infinite
  and rational {T}rees.
\newblock In {\em Proc. third Annual Symposium on Logic in Computer Science},
  pages 348--359. Computer Society Press, July 1988.

\bibitem[Mak87]{Mak87}
Johann~A. Makowsky.
\newblock Why {H}orn formulas matter in computer science: Initial structures
  and generic examples.
\newblock {\em Journal of Computer and System Sciences}, 34:266--292, 1987.

\bibitem[MAK91]{Aronson91}
L.~Hallnass Martin~Aronson, L-H.~Eriksson and P.~Kreuger.
\newblock A survey of {GCLA}: a definitional approach to logic programming.
\newblock In Peter Schroeder-Heister, editor, {\em Proceedings of the First
  International Workshop on Extensions of Logic Programming}, volume 1050 of
  {\em 475}, pages 19--34, Berlin, March28--30~ 1991. Springer.

\bibitem[Mal71]{Mal71}
A.I. Mal'cev.
\newblock Complete axiomatixation of classes of locally free algebrae of
  varioud type.
\newblock In {\em The metamathematics of algebraic systems: Collected papers,
  1936--1967}, pages 262--289. North-Holland, 1971.

\bibitem[McC88a]{Mc88a}
L.~Thorne McCarty.
\newblock Clausal intuistionistic logic: {I}. {F}ixed point semantics.
\newblock {\em Journal of Logic Programming}, 5(1):1--31, March 1988.

\bibitem[McC88b]{Mc88b}
L.~Thorne McCarty.
\newblock Clausal intuitionistic logic {II}. {T}ableau proof procedure.
\newblock {\em Journal of Logic Programming}, 5:93--132, 1988.

\bibitem[Mil89a]{Miller89iclp}
Dale Miller.
\newblock Lexical scoping as universal quantification.
\newblock In G.~Levi and M.~Martelli, editors, {\em Proceedings of the Sixth
  International Conference on Logic Programming}, pages 268--283, Lisbon,
  Portugal, June 1989. MIT Press.

\bibitem[Mil89b]{Miller91elp}
Dale Miller.
\newblock A logic programming language with lambda-abstraction, function
  variables, and simple unification.
\newblock In Peter Schroeder-Heister, editor, {\em Proceedings of the
  International Workshop on Extensions of Logic Programming}, pages 253--281,
  T{\"u}bingen, Germany, 1989. Springer-Verlag LNAI 475.

\bibitem[Mil89c]{Miller89jlp}
Dale Miller.
\newblock A logical analysis of modules in logic programming.
\newblock {\em Journal of Logic Programming}, 6(1-2):79--108, January 1989.

\bibitem[Mil91]{Miller91jlc}
Dale Miller.
\newblock A logic programming language with lambda-abstraction, function
  variables, and simple unification.
\newblock {\em Journal of Logic and Computation}, 1(4):497--536, 1991.

\bibitem[Mil92]{Miller92jsc}
Dale Miller.
\newblock Unification under a mixed prefix.
\newblock {\em Journal of Symbolic Computation}, 14:321--358, 1992.

\bibitem[Mil94]{Miller94}
Dale Miller.
\newblock A multiple-conclusion meta-logic.
\newblock In S.~Abramsky, editor, {\em Ninth Annual {IEEE} Symposium on Logic
  in Computer Science}, pages 272--281, Paris, France, July 1994.

\bibitem[MM82]{Martelli82}
Alberto Martelli and Ugo Montanari.
\newblock An efficient unification algorithm.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  4(2):258--282, April 1982.

\bibitem[MM97]{McDowell97lics}
Raymond McDowell and Dale Miller.
\newblock A logic for reasoning with higher-order abstract syntax: An extended
  abstract.
\newblock In Glynn Winskel, editor, {\em Proceedings of the Twelfth Annual
  Symposium on Logic in Computer Science}, pages 434--445, Warsaw, Poland, June
  1997.

\bibitem[MM00]{McDowell00}
Raymond McDowell and Dale Miller.
\newblock Cut-elimination for a logic with definitions and induction,.
\newblock {\em Theoretical Computer Science}, 231(231):91--119, 2000.

\bibitem[MMP88]{Mancarella88}
Paolo Mancarella, Simone Martini, and Dino Pedreschi.
\newblock {C}omplete logic {P}rograms with domain-closure {A}xiom.
\newblock {\em Journal of Logic Programming}, 5:263--276, 1988.

\bibitem[MN89]{Mal89}
J.~Maluszy{\'n}ski and T.~N{\"a}slund.
\newblock Fail {S}ubstitutions for {N}egation as {F}ailure.
\newblock In Ewing~L. Lusk and Ross~A. Overbeek, editors, {\em Proceedings of
  the North American Conference on Logic Programming}, pages 461--476,
  Cleveland, Ohio, USA, 1989.

\bibitem[MNPS91]{Miller91apal}
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.
\newblock Uniform proofs as a foundation for logic programming.
\newblock {\em Annals of Pure and Applied Logic}, 51:125--157, 1991.

\bibitem[Mom92]{Momigliano92}
Alberto Momigliano.
\newblock Minimal negation and hereditary {H}arrop formulae.
\newblock In Anil Nerode and Mikhail Taitslin, editors, {\em Proceedings of
  Logical Foundations of Computer Science (Tver '92)}, volume 620 of {\em
  LNCS}, pages 326--335, Berlin, Germany, July 1992. Springer.

\bibitem[MP88]{MP88}
Paolo Mancarella and Dino Pedreschi.
\newblock An algebra of logic programs.
\newblock In Robert~A. Kowalski and Kenneth~A. Bowen, editors, {\em Proceedings
  of the Fifth International Conference and Symposium on Logic Programming},
  pages 1006--1023, Seattle, 1988. ALP, IEEE, The MIT Press.

\bibitem[MP91]{Michaylov91}
Spiro Michaylov and Frank Pfenning.
\newblock Natural semantics and some of its meta-theory in {Elf}.
\newblock In L.-H. Eriksson, L.~Halln{\"a}s, and P.~Schroeder-Heister, editors,
  {\em Proceedings of the Second International Workshop on Extensions of Logic
  Programming}, pages 299--344, Stockholm, Sweden, January 1991.
  Springer-Verlag LNAI 596.

\bibitem[MP93]{Michaylov93}
Spiro Michaylov and Frank Pfenning.
\newblock Higher-order logic programming as constraint logic programming.
\newblock In {\em Position Papers for the First Workshop on Principles and
  Practice of Constraint Programming}, pages 221--229, Newport, Rhode Island,
  April 1993. Brown University.

\bibitem[MPRT90a]{MP90}
Paolo Mancarella, Dino Pedreschi, Marina Rondinelli, and Marco Tagliatti.
\newblock Algebraic properties of a class of logic programs.
\newblock In Saumya Debray and Manuel Hermenegildo, editors, {\em Proceedings
  of the 1990 North American Conference on Logic Programming}, pages 23--39,
  Austin, 1990. ALP, MIT Press.

\bibitem[MPRT90b]{Mancarella90}
Paolo Mancarella, Dino Pedreschi, Marina Rondinelli, and Marco Tagliatti.
\newblock Algebraic properties of a class of logic programs.
\newblock In Saumya Debray and Manuel Hermenegildo, editors, {\em Proceedings
  of the 1990 North American Conference on Logic Programming}, pages 23--39,
  Austin, 1990. ALP, MIT Press.

\bibitem[Myc80]{Mycroft80}
Alan Mycroft.
\newblock The theory and practice of transforming call-by-need to
  call-by-value.
\newblock In {\em Proceedings of the 4th International Symposium on
  Programming}, volume~83 of {\em Lecture Notes in Computer Science}, pages
  269--281. Springer Verlag, 1980.

\bibitem[Nai86]{Naish86}
Lee Naish, editor.
\newblock {\em Negation and Control in {P}rolog}, volume 238 of {\em Lecture
  Notes in Computer Science}.
\newblock Springer Verlag, 1986.

\bibitem[Nel49]{Nelson49}
D.~Nelson.
\newblock Constructive falsity.
\newblock {\em Journal of Symbolic Logic}, pages 16--26, 1949.

\bibitem[Nip91]{Nipkow91lics}
Tobias Nipkow.
\newblock Higher-order critical pairs.
\newblock In G.~Kahn, editor, {\em Sixth Annual {IEEE} Symposium on Logic in
  Computer Science}, pages 342--349, Amsterdam, The Netherlands, July 1991.

\bibitem[Nip93]{Nipkow93tlca}
Tobias Nipkow.
\newblock Orthogonal higher-order rewrite systems are confluent.
\newblock In M.~Bezem and J.F. Groote, editors, {\em Proceedings of the
  International Conference on Typed Lambda Calculi and Applications}, pages
  306--317, Utrecht, The Netherlands, May 1993.

\bibitem[NL92]{Olivetti92}
Olivetti N. and Terracini L.
\newblock N-{P}rolog and the equivalence of logic program.
\newblock {\em Journal of Logic Language and Information}, 5:253\--3392, 1992.

\bibitem[NL95]{Nadathur95lics}
Gopalan Nadathur and Donald~W. Loveland.
\newblock Uniform proofs and disjunctive logic programming.
\newblock In D.~Kozen, editor, {\em Proceedings of the Tenth Annual Symposium
  on Logic in Computer Science}, pages 148--155, San Diego, California, June
  1995. IEEE Computer Society Press.
\newblock Available as Technical Report CS-1994-40, Department of Computer
  Science, Duke University, December 1994.

\bibitem[NM88]{Nadathur88}
Gopalan Nadathur and Dale Miller.
\newblock An overview of {$\lambda$Prolog}.
\newblock In Kenneth~A. Bowen and Robert~A. Kowalski, editors, {\em Fifth
  International Logic Programming Conference}, pages 810--827, Seattle,
  Washington, August 1988. MIT Press.

\bibitem[O'K85]{OKeefe85}
R.~A. O'Keefe.
\newblock Towards an algebra for constructing logic programs.
\newblock In {\em Proceedings of the International Symposium on Logic
  Programming}, pages 152--161. IEEE Computer Society, Technical Committee on
  Computer Languages, The Computer Society Press, July 1985.

\bibitem[PE88]{Pfenning88pldi}
Frank Pfenning and Conal Elliott.
\newblock Higher-order abstract syntax.
\newblock In {\em Proceedings of the {ACM SIGPLAN '88} Symposium on Language
  Design and Implementation}, pages 199--208, Atlanta, Georgia, June 1988.

\bibitem[Pea90]{Pearce?}
David Pearce.
\newblock Reasoning with negative information, {II}: Hard negation, strong
  negation and logic programs.
\newblock In H.~{Pearce, D.; Wansing}, editor, {\em Proceedings of the
  International Workshop on Nonclassical Logics and Information Processing},
  volume 619 of {\em LNAI}, pages 63--79, Berlin, FRG, November 1990. Springer
  Verlag.

\bibitem[Pet81]{Peterson81}
G.~L. Peterson.
\newblock Myths about the mutual exclusion problem.
\newblock {\em Information Processing Letters}, 12(3):115--116, June 1981.

\bibitem[Pfe89]{Pfenning89lics}
Frank Pfenning.
\newblock {Elf}: A language for logic definition and verified meta-programming.
\newblock In {\em Fourth Annual Symposium on Logic in Computer Science}, pages
  313--322, Pacific Grove, California, June 1989. IEEE Computer Society Press.

\bibitem[Pfe91a]{Pfenning91lf}
Frank Pfenning.
\newblock Logic programming in the {LF} logical framework.
\newblock In G\'{e}rard Huet and Gordon Plotkin, editors, {\em Logical
  Frameworks}, pages 149--181. Cambridge University Press, 1991.

\bibitem[Pfe91b]{Pfenning91lics}
Frank Pfenning.
\newblock Unification and anti-unification in the {Calculus} of
  {Constructions}.
\newblock In {\em Sixth Annual {IEEE} Symposium on Logic in Computer Science},
  pages 74--85, Amsterdam, The Netherlands, July 1991.

\bibitem[Pfe92]{Pfenning94un}
Frank Pfenning.
\newblock Computation and deduction.
\newblock Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May
  1992.

\bibitem[Pfe93]{Pfenning93types}
Frank Pfenning.
\newblock Refinement types for logical frameworks.
\newblock In Herman Geuvers, editor, {\em Informal Proceedings of the Workshop
  on Types for Proofs and Programs}, pages 285--299, Nijmegen, The Netherlands,
  May 1993.

\bibitem[Pfe99]{Pfenning99handbook}
Frank Pfenning.
\newblock Logical frameworks.
\newblock In Alan Robinson and Andrei Voronkov, editors, {\em Handbook of
  Automated Reasoning}. Elsevier Science Publishers, 1999.
\newblock In preparation.

\bibitem[PG86]{Poole85}
David~L. Poole and Randy Goebel.
\newblock Gracefully adding negation and disjunction to {P}rolog.
\newblock In Ehud Shapiro, editor, {\em Proceedings of the Third International
  Conference on Logic Programming}, Lecture Notes in Computer Science, pages
  635--641, London, 1986. Springer-Verlag.

\bibitem[Plo71]{Plotkin71}
G.~D. Plotkin.
\newblock A further note on inductive generalization.
\newblock In {\em Machine Intelligence}, volume~6, pages 101--124. Edinburgh
  University Press, 1971.

\bibitem[PM90]{Pareschi90}
Remo Pareschi and Dale Miller.
\newblock Extending definite clause grammars with scoping constructs.
\newblock In David H.~D. Warren and Peter Szeredi, editors, {\em Proceedings of
  Seventh International Conference on Logic Programming}, pages 373--389,
  Jerusalem, Israel, June 1990. MIT Press.

\bibitem[Pym99]{Pym99}
David~J. Pym.
\newblock On bunched predicate logic.
\newblock In G.~Longo, editor, {\em Proceedings of the 14th Annual Symposium on
  Logic in Computer Science (LICS'99)}, pages 183--192, Trento, Italy, July
  1999. IEEE Computer Society Press.

\bibitem[Rei78]{Reiter78}
R.~Reiter.
\newblock On closed world databases.
\newblock In Gallaire and Minker, editors, {\em Logic and Databases}, pages
  55--76. Plenum Press, New York, 1978.

\bibitem[RL92]{Reed92}
David~W. Reed and Donald~W. Loveland.
\newblock A comparison of three {P}rolog extensions.
\newblock {\em Journal of Logic Programming}, 12(1-2):25--50, January 1992.

\bibitem[Rob65]{Robinson65}
J.~Alan Robinson.
\newblock A machine-oriented logic based on the resolution principle.
\newblock {\em Journal of the ACM}, 12(1):23--41, January 1965.

\bibitem[RP96]{Rohwedder96esop}
Ekkehard Rohwedder and Frank Pfenning.
\newblock Mode and termination checking for higher-order logic programs.
\newblock In Hanne~Riis Nielson, editor, {\em Proceedings of the European
  Symposium on Programming}, pages 296--310, Link{\"o}ping, Sweden, April 1996.
  Springer-Verlag LNCS 1058.

\bibitem[Sch00]{Schurmann00phd}
Carsten Sch{\"u}rmann.
\newblock {\em Automating the meta theory of deductive systems}.
\newblock PhD thesis, Carnegie Mellon University, 2000.

\bibitem[SD94]{DeSchreye94}
Danny~De Schreye and Stefaan Decorte.
\newblock Termination of logic programs: the never-ending story.
\newblock {\em The Journal of Logic Programming}, 19 \& 20:199--260, May 1994.

\bibitem[SH93]{SchroederHeister93lics}
Peter Schroeder-Heister.
\newblock Rules of definitional reflection.
\newblock In M.~Vardi, editor, {\em Proceedings of the Eighth Annual {IEEE}
  Symposium on Logic in Computer Science}, pages 222--232, Montreal, Canada,
  June 1993.

\bibitem[She85]{Shepherdson85}
John~C. Shepherdson.
\newblock Negation as failure {II}.
\newblock {\em The Journal of Logic Programming}, 2(3):185--202, Oktober 1985.

\bibitem[She88]{Shepherdson88}
J.~C. Shepherdson.
\newblock Negation in logic progamming.
\newblock In J.~Minker, editor, {\em Found. of Deductive Databases and Logic
  Programming}, page~19. Morgan Kaufmann, San Mateo, CA, 1988.

\bibitem[She89]{Shepherdson89}
J.~C. Shepherdson.
\newblock A sound and complete semantics for a version of negation as failure.
\newblock {\em Theoretical Computer Science}, 65(3):343--371, July 1989.

\bibitem[Sny91]{Snyder91}
Wayne Snyder.
\newblock {\em A proof theory for general unification}.
\newblock Birkhauser, Boston, 1991.

\bibitem[SP98]{Schurmann98cade}
Carsten Sch{\"u}rmann and Frank Pfenning.
\newblock Automated theorem proving in a simple meta-logic for {LF}.
\newblock In Claude Kirchner and H{\'e}l{\`e}ne Kirchner, editors, {\em
  Proceedings of the 15th International Conference on Automated Deduction
  (CADE-15)}, pages 286--300, Lindau, Germany, July 1998. Springer-Verlag LNCS
  1421.

\bibitem[ST84]{Sato84}
T.~Sato and H.~Tamaki.
\newblock Transformational logic program synthesis.
\newblock In {\em International Conference on Fifth Generation Computer
  Systems}, 1984.

\bibitem[St{\"a}92]{Staerk92}
R.~F. St{\"a}rk.
\newblock {\em The Proof Theory of Logic Programs with Negation}.
\newblock PhD thesis, University of Berne, Switzerland, 1992.

\bibitem[Sti88]{Stickel88}
Mark~E. Stickel.
\newblock A {P}rolog {T}echnology {T}heorem {P}rover: implementation by an
  extended {P}rolog compiler.
\newblock {\em Journal of Automated Reasoning}, 4:353--380, 1988.

\bibitem[Stu95]{Stuckey95}
Peter~J. Stuckey.
\newblock Negation and constraint logic programming.
\newblock {\em Information and Computation}, 118(1):12--33, April 1995.

\bibitem[SW92]{Sannella92}
D.~T. Sannella and L.~A. Wallen.
\newblock A calculus for the construction of modular {P}rolog programs.
\newblock {\em Journal of Logic Programming}, 12(1-2):147--177, January 1992.

\bibitem[Thi84]{Thiel84}
Jean~Jacques Thiel.
\newblock Stop losing sleep over incomplete data type specifications.
\newblock In Ken Kennedy, editor, {\em Conference Record of the 11th Annual
  {ACM} Symposium on Principles of Programming Languages}, pages 76--82, Salt
  Lake City, UT, jan 1984. ACM Press.

\bibitem[TMM89]{Kuo89}
Kuo Tsung-Min and Prateek Mishra.
\newblock {Strictness Analysis: A New Perspective Based on Type Inference}.
\newblock In {\em {FPCA '89, Functional Programming Languages and Computer
  Architecture}}, London, UK, September 11--13, 1989. ACM Press, New York.

\bibitem[TS84]{Tamaki84}
H.~Tamaki and T.~Sato.
\newblock Unfold/fold transformation of logic programs.
\newblock In Sten-{\AA}ke T{\"a}rnlund, editor, {\em Proceedings of the Second
  International Conference on Logic Programming}, pages 127--138, Uppsala,
  1984.

\bibitem[Vir99]{Virga99phd}
Roberto Virga.
\newblock {\em Higher-Order Rewriting with Dependent Types}.
\newblock PhD thesis, Department of Mathematical Sciences, Carnegie Mellon
  University, 1999.
\newblock Forthcoming.

\bibitem[Wad90]{Wadler90}
P.~Wadler.
\newblock Is there a use for linear logic.
\newblock Technical report, University of Glasgow, 1990.

\bibitem[Wal87]{Wallace87}
M.~Wallace.
\newblock Negation by constraints: {A} sound and efficient implementation of
  negation in deductive databases.
\newblock In {\em Proceedings of the Fifth International Conference and
  Symposium on Logic Programming}, pages 253--263, San Francisco, August -
  September 1987. IEEE, Computer Society Press.

\bibitem[Wan93]{Wansing93}
Heinrich Wansing.
\newblock {\em The logic of information structures}, volume 681 of {\em Lecture
  Notes in Artificial Intelligence and Lecture Notes in Computer Science}.
\newblock Springer-Verlag Inc., New York, NY, USA, 1993.
\newblock Revision of the author's doctoral thesis (Fachbereich Philosophie und
  Sozialwissenschaften I of the Free University of Berlin).

\bibitem[WBF93]{Wright93}
D.~A. Wright and C.~A. Baker-Finch.
\newblock Usage analysis with natural reduction types.
\newblock In {\em Lecture Notes in Computer Science}, volume 724, pages
  254--266, 1993.

\bibitem[WM91]{Wos91}
Larry Wos and William McCune.
\newblock Automated theorem proving and logic programming: {A} natural
  symbiosis.
\newblock {\em Journal of Logic Programming}, 11(1):1--53, July 1991.

\bibitem[Wri91]{Wright91}
D.~A. Wright.
\newblock A new technique for strictness analysis.
\newblock In {\em TAPSOFT '91}. Springer-Verlag, New York, NY, 1991.
\newblock Lecture Notes in Computer Science 494.

\bibitem[Wri92]{Wright92}
D.~A. Wright.
\newblock {\em Reduction types and intensionality in the lambda-calculus}.
\newblock PhD thesis, University of Tasmania, September 1992.

\bibitem[Wri96]{Wright96}
David~A. Wright.
\newblock Linear, strictness and usage logics.
\newblock In Michael~E. Houle and Peter Eades, editors, {\em Proceedings of
  Conference on Computing: The Australian Theory Symposium}, pages 73--80,
  Townsville, January~29--30 1996. Australian Computer Science Communications.

\end{thebibliography}
