\begin{thebibliography}{BMPT90}

\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[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[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[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[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[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[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[Gab85]{Gabbay85}
Dov~M. Gabbay.
\newblock N-{P}rolog: An extension of prolog with hypothetical implications
  {II}. logical foundations and negation as failure.
\newblock {\em Journal of Logic Programming}, 2(4):251--283, December 1985.

\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}, to appear, 1998.

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

\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[Har91]{Harland91phd}
James Harland.
\newblock {\em On Hereditary Harrop Formulae as a Basis for Logic Programming}.
\newblock PhD thesis, Edinburgh, January 1991.

\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[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[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[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[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[McC88a]{Mc88a}
L.~Thorne McCarty.
\newblock Clausal intuistionistic logic: {I}. fixed 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}. tableau proof procedure.
\newblock {\em Journal of Logic Programming}, 5:93--132, 1988.

\bibitem[Mil89]{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[MM97]{MacDowell97lics}
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[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[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[Nel49]{Nelson49}
D.~Nelson.
\newblock Constructive falsity.
\newblock {\em Journal of Symbolic Logic}, pages 16--26, 1949.

\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[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[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[Pfe91]{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[Pfe92]{Pfenning94un}
Frank Pfenning.
\newblock Computation and deduction.
\newblock Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May
  1992.

\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[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[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[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[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[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).

\end{thebibliography}
