\begin{thebibliography}{10}

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

\bibitem{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{Bar90}
R.~Barbuti, P.~Mancarella, D.~Pedreschi, and F.~Turini.
\newblock {A} transformational approach to negation in logic programming.
\newblock {\em Journal of Logic Programming}, 8:201--228, 1990.

\bibitem{Bonner94}
A.~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}
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{Gabbay85}
D.~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, Dec. 1985.

\bibitem{Giordano98}
L.~Giordano and N.~Olivetti.
\newblock Negation as failure and embedded implication.
\newblock {\em Journal of Logic Programming}, 36(2):91--147, August 1998.

\bibitem{Harland91phd}
J.~Harland.
\newblock {\em On Hereditary Harrop Formulae as a Basis for Logic Programming}.
\newblock PhD thesis, Edinburgh, Jan. 1991.

\bibitem{Harper93jacm}
R.~Harper, F.~Honsell, and G.~Plotkin.
\newblock A framework for defining logics.
\newblock {\em Journal of the Association for Computing Machinery},
  40(1):143--184, Jan. 1993.

\bibitem{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, Sept. 1987.

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

\bibitem{Miller91apal}
D.~Miller, G.~Nadathur, F.~Pfenning, and A.~Scedrov.
\newblock Uniform proofs as a foundation for logic programming.
\newblock {\em Annals of Pure and Applied Logic}, 51:125--157, 1991.

\bibitem{Momigliano00phd}
A.~Momigliano.
\newblock {\em Elimination of Negation in a Logical Framework}.
\newblock PhD thesis, Carnegie Mellon University, 2000.
\newblock Forthcoming.

\bibitem{Momigliano99}
A.~Momigliano and F.~Pfenning.
\newblock The relative complement problem for higher-order patterns.
\newblock In D.~D. Schreye, editor, {\em Proceedings of the 1999 International
  Conference on Logic Programming (ICLP'99)}, pages 389--395, La Cruces, New
  Mexico, 1999. MIT Press.

\bibitem{Nadathur88}
G.~Nadathur and D.~Miller.
\newblock An overview of {$\lambda$Prolog}.
\newblock In K.~A. Bowen and R.~A. Kowalski, editors, {\em Fifth International
  Logic Programming Conference}, pages 810--827, Seattle, Washington, Aug.
  1988. MIT Press.

\bibitem{Pfenning99handbook}
F.~Pfenning.
\newblock Logical frameworks.
\newblock In A.~Robinson and A.~Voronkov, editors, {\em Handbook of Automated
  Reasoning}. Elsevier Science Publishers, 2000.
\newblock In preparation.

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

\bibitem{Schurmann00phd}
C.~Sch{\"u}rmann.
\newblock {\em Automating the Meta-Theory of Deductive Systems}.
\newblock PhD thesis, Carnegie-Mellon University, 2000.
\newblock forthcoming.

\bibitem{Schurmann98cade}
C.~Sch{\"u}rmann and F.~Pfenning.
\newblock Automated theorem proving in a simple meta-logic for {LF}.
\newblock In C.~Kirchner and H.~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.

\end{thebibliography}
