\begin{thebibliography}{10}

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

\bibitem{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{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{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{Kunen87}
K.~Kunen.
\newblock Answer sets and negation-as-failure.
\newblock In Jean-Louis Lassez, editor, {\em Proceedings of the Fourth
  International Conference on Logic Programming ({ICLP} '87)}, pages 219--228,
  Melbourne, Australia, May 1987. MIT Press.

\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, September 1987.

\bibitem{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{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{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{Momigliano99phd}
Alberto Momigliano.
\newblock {\em Elimination of negation in a logical framework}.
\newblock PhD thesis, Carnegie Mellon University, Forthcoming.

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

\end{thebibliography}
