\begin{thebibliography}{999}
\footnotesize
% 130 items
\bibitem {Acz77} Aczel A. An Introduction to Inductive Definitions.
In {\em Handbook 
of Mathematical Logic}, Barwise J. (ed.), North-Holland, 1977.

\bibitem {Aka88} S. Akama. On the Proof Method for Constructive 
Falsity. {\em ZML} 34, 385--392, 1988.

\bibitem {Apt82}  A.K. Apt   \&  Van Emden M.H. Contributions to the 
Theory of Logic Programming. { \em JACM}, vol. 29, no. 3, pp. 
841\--862, 1982.  

\bibitem {Apt88} A.K. Apt , Blair H. A. \& Walker A.   Towards a 
Theory of Declarative Knowledge. In: {\em Foundations of Deductive 
Databases and Logic Programming}, Minker J. (ed.), pp. 89\--148, 
Morgan Kaufmann, 1988.

\bibitem  {Apt90} A.K. Apt  Logic Programming, {\em Handbook 
of Theoretical Computer Science},  Leuween J. (ed.), Elsevier, 1990.

\bibitem  {Apt95} A.K. Apt  \& Bol R. Logic Programming and Negation: 
A Survey. {\em Journal of Logic Programming}, \ldots 1995.

\bibitem {Aro91}  Aronson M. , Eriksson L-H. , Halln�ss L. \&   
Kreuger P. A Survey of GCLA: a Definitional Approach to Logic 
Programming.  In: {\em Extensions of Logic Programming}, 
Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.

\bibitem  {Bar87} Barbuti R., Mancarella P., Pedreschi D. \& 
Turini F.  Intensional Negation of Logic Programs. {\em Tapsoft87}, 
LNCS vol. 259, Springer Verlag , pp. 96--110,1987.


\bibitem  {Bar90} Barbuti R., Mancarella P., Pedreschi D. \& 
Turini F.   A Transformational Approach to Negation in Logic 
Programming. {\em Journal of Logic Programming}, 8(3), pp. 201\--228, 
1990.

\bibitem {Bon90} Bonner A. J. \&  McCarthy L. T. Adding  NF to 
Intuitionistic Logic Programmninhg. {\em Proc. North American Conf. 
on Logic Programming}, pp. 681-- 73, MIT Press 1990.

\bibitem {Bre88} Brezau-Tannen V. Combining Algebra and \ho types. In 
{\em Proceedings of the IEEE Symposium on Logic in Computer Science, 
1988}, pp. 82--90, 1988.

\bibitem {Bro90} A. Brogi, P. Mancarella, D. Pedreschi \& F. Turini.
\newblock Universal Quantification by Case Analysis.\newblock {\em 
ECAI-90}, pp. 111--116, 1990.

\bibitem {Bru93}  F.  Bruscoli,  F.  Levi,  G. Levi  and   M.C. Meo. 
\newblock Intensional Negation in Constraint Logic Programming. 
\newblock {\em Proceedings of GULP93}, D. Sacca', ed., pp. 359--373, 
1993.

\bibitem {Bur88} B\'{u}rchert H.J. Solving Disequations in Equational 
Theories. {\em CADE88}, LCNS 310, pp. 517--526, Spriger Verlag.

\bibitem {Cha88} D. Chan.  \newblock Constructive Negation Based on 
the Completed Database.  \newblock In {\em Proceedings of the Fifth 
International Conference and Symposium on Logic Programming}, R. 
Kowalski and K. Bowen, eds., pp.  111--125, MIT Press, 1988.

\bibitem {Cha89} D. Chan.  \newblock An Extension of Constructive 
Negation and its Application in Coroutining.  \newblock In {\em 
Proceedings of North American Conference on Logic Programming}, E. 
Lusk and R. Overbeek, eds., pp.  477--493, MIT Press,1989.

\bibitem {Cla78} Clark K.L.   Negation as Failure. In:  {\em Logic 
and Data Bases}, Gallaire H. \& 
Minker J. (eds.), Plenum Press, New York, pp. 293\--322, 1978. 

\bibitem {Col84} A. Colmerauer. Equations and Disequations on finite 
and infinite trees. {\em FGCS84}, pp.85--99, 1984.

\bibitem {Com88} Comon H. Unification et  Disunification: Theorie et 
Applications.  {\em Thesis de Doctorat}, I.N.P.\ de Grenoble, 1988.

\bibitem {CL89} H. Comon  \& Lescanne P. Equational Problems and 
Disunification. {\em Journal of Symbolic Computation}, {\bf 7}, 
371--425, 1989. 

\bibitem {CLu9?} H. Comon  \& D. Lugiez P. AC-complements\ldots.

\bibitem {Com91} H. Comon  Disunification: A Survey. In: {\em 
Computational Logic}, Lassez \& Plotkin (eds.), MIT Press 1991.

\bibitem {Com91b} H. Comon  Ground Normal Form Languages Application to 
Inductive Proof. Part 1: Complement Problem. {\em Rapport de 
Recherche}, n\circ 698, Universite de Paris Sud, 1991.

\bibitem {Com93} H. Comon.  Elimination of Negation in Equational
Theories. {Technical Report}, Paris-Sud, 1993.

\bibitem {Con86} Constable R. et al. {\em Implementing Mathematics
with the Nuprl Development System}. Prentice-Hall, 1986.

\bibitem {Dar92} Dart P.W. \& Zobel J. A Regular Type Language for 
Logic Programs. In {\em Types in Logic Programming}, F. Pfenning 
(ed.), pp. 157\--187, MIT Press, 1992.

\bibitem {Dow94} Dowek G. , Hardin T. \& Kirchner C. Higher-Order
Unification via Explicit Substitution. ?

\bibitem {Dou93} Dougherty D.J. Higher-Order
Unification via Combinators. {\em Theoretical Computer Science},
113:273--298, 1993.

\bibitem {Dra95}. Drabent, W. What is Failure ? An Approach to 
Constructive Negation. {\em Acta Informatica}, 32, pp. 27--59, 
Springer Verlag, 1995.


\bibitem {Er91} L. -H. Erikkson. {\em Finitary Partial Definition and 
General Logic}. {\em Extensions of Logic Programming}, 
Schroeder-Heister P. (ed), LNAI, vol. 475, Springer-Verlag, 1991.


\bibitem {Er93} L. -H. Erikkson. {\em Finitary Partial Definition and 
General Logic}. Ph.D. thesis, Royal Institute of Technology, 
Stockholm, 1993.

\bibitem {Fel91} Felty A. Encoding Dependent Types in an 
Intuitionistic Logic. In: {\em Logical Frameworks}, Huet \& Plotkin 
(eds.), Cambridge University Press, pp. 215\--251, 1991.

\bibitem {Foo88}  Foo N, Rao A., Taylor A.  \&  Walker A. Deduced 
Relevant Types and Constructive Negation. {\em Proc. 5th Conf. Logic 
Programming}, Kowalski B. \& Bowen K. (eds.), pp.126\--139, 1988.

\bibitem {Gab90} D.M. Gabbay. Modal Provability Interpretations
of {\em NF}.  In: {\em Extensions of Logic Programming}, 
Schroeder-Heister P. (ed), LNAI, vol. 475, Springler-Verlag, 1991.


\bibitem {Gab84}  D.M. Gabbay.  \&  Reyle U. N-Prolog: an Extension 
of Prolog with Hypothetical Implications: 1. {\em Journal of Logic 
Programming}, 4, pp. 319\--355, 1984

\bibitem {Gab86}  D. M. Gabbay \& Sergot M. Negations as Inconsistency: 
I. {\em Journal of Logic Programming}, pp. 1\--36, 1986.

\bibitem {Gab8?} D.M. Gabbay. What is Negation.  In: {\em Logic 
Colloquium}\ldots.

\bibitem {Gab90} D.M. Gabbay. Modal Provability Interpretations
of {\em NF}.  In: {\em Extensions of Logic Programming}, 
Schroeder-Heister P. (ed), LNAI, vol. 475, Springler-Verlag, 1991.

\bibitem {Gab90} D.M. Gabbay. et al. Handbook of Logic In AI\ldots

\bibitem {Gec84} Gecseg F. \& Steinby M. {\em Tree Automata}. 
Akademiai Kiado, Budapest, 1984.

\bibitem {Gel90} M. Gelfond \& V. Lifschitz. Logic Programming with 
Classical Negation. In: {\em  Proc ICLP90}, MIT Press, 1990.

\bibitem {Gin91}  Ginsberg M L. Negative Subgoals with Free 
Variables, {\em Journal of Logic Programming},11, pp. 271\--293, 1991.

\bibitem {Gio92} Giordano L. \& Olivetti  N.  NF in Intuitionistic
Logic Programming. In Apt  K. (Ed.), {\em JCSLP92}, pp. 431--445,
MIT Press 1992.

\bibitem{Gir91} J-H. Girard Y. Lafont \& P. Taylor. {\em Proof and 
Types}, Cambridge University Press, 1991.

\bibitem{GH78} J. Gougen \& J.J. Horning. The Algebraic Specification 
of Abstract Data Types. {\em Acta Informatica},10:27--55,1978.

\bibitem {Gur77} Y. Gurevich, Intutionistic Logic with Strong 
Negation. {\em Studia Logica}36, pp. 49--59, 1977.

\bibitem {Jac93} Jacobs B. \& Melham T. Translating Dependant
Type Theory into Higher-Order Logic. In: Typed $\lambda$-Calculi
and Applications, Bezem \& Groote (eds.), pp. 209\--229, Springler-
Verlag, 1993.

\bibitem {Jaf83}  Jaffar J., Lassez J-L.  \&  Lloyd J.W. Completeness 
of the Negation as Failure Rule. In: {\em IJCAI-83}, Karlsurhe, pp. 
500\--506, 1983. 

\bibitem {Jgr91}  J\"{a}ger G. Between Constructive Mathematics
and PROLOG. {\em Arch Math. Logic}, 30:297-310, 1991.

\bibitem {Jgr93}  J\"{a}ger G. Some Proof-Theoretic Aspects of Logic 
Programming. In: H. Schwichtenberg (ed.) {\em Algebra And Logic of 
Specification}, Springer-Verlag, Berlin 1993.

\bibitem {Joh36}  Johansonn I. Der Minimal Kalkul, ein Reduzierter 
Intuitionistischer Formalismus, {\em Compositio Mathematica}, vol. 4, 
pp. 119\--136, 1936.

\bibitem {Hal91a} L. Halln\"as. Partial Inductive Definitions. {\em 
Theoretical Computer Science},  v. 87 no. 1, pp. 115\--147, 1991.

\bibitem  {Hal90} L. Halln\"as  \& P. Schroeder-Heister.   A 
Proof-Theoretic Approach to Logic Programming: Clauses as Rules. {\em 
Journal of Logic and Computation},  v.1 no. 2. pp. 261\--283, 1990.

\bibitem  {Hal91b} L. Halln\"as  \& P. Schroeder-Heister.  A 
Proof-Theoretic Approach to Logic Programming: Programs as 
Definitions. {\em Journal of Logic and Computation},  v.1 no. 5. pp. 
635\--660,1991.

\bibitem  {Har91a }J.  Harland..   {\em On Hereditary Harrop
 Formulae as a Basis for Logic Programming.} PhD Thesis, Edinburgh 
1991.

\bibitem {Har91b} J. Harland.  \newblock A Clausal Form of the 
Completion of Logic Programs.  \newblock In {\em Proceedings of the 
Eighth International Conference on Logic Programming (ICLP'91)}, pp.  
711 --725, MIT Press, 1991.

\bibitem  {Har92} J.  Harland.. Towards a Static Proof System for 
Negation as Failure. {\em Citri/TR-92-49}, University of Melburne, 
1992.

\bibitem {Har93} Harper R., Honsell F. \& Plotkin G. A Framework
for Defining Logics. {\em JACM}, 40(1):143--184, 1993.

\bibitem {Hei92} Heintze N. \& Jaffar J. Semantic Types for Logic 
Programs. In {\em Types in Logic Programming}, F. Pfenning 
(ed.), pp. 141\--156, MIT Press, 1992.

\bibitem {Hil94} P.M. Hill and J.W. Lloyd. {\em The {G}\"odel 
Programming Language}, MIT Press, 1994.

\bibitem {Kir87} Kirchner C. \& Lescanne P. Solving Disequations. 
{\em  Proceedings of the IEEE Symposium on Logic in Computer Science, 
1987},
pp. 347--352, 1987.
\bibitem {Kk90} Kirchner C. \& Klay  F. Syntactic Theories and 
Unification. {\em  Proceedings of the IEEE Symposium on Logic in 
Computer Science, 1990},
pp. ??--??, 1990.

\bibitem  {Kun87} Kunen K.   Negation in Logic Programming. 
{\em Journal of Logic Programming},  4, pp. 289\--308, 1987.


\bibitem  {Kun87b} Kunen K. Answer Sets and NF. In: {\em Proceeding 
of ICLP87}, pp. 219-228, MIT Press,1987.

\bibitem {Kro} M.R. Krom. \newblock THe Decision Problem for a Class 
of First-Order Formulas in 
which all Disjunctions are Binary. \newblock  {\em Zeit. math. 
Logik}, {\bf 13},15--20, 1967.


\bibitem{Kup88} Kuper G.M., McAloon K.W., Palem K.V. \& Perry  K.J.
Efficient Parallel Algorithms for Anti-Unification and Relative 
Complement. {\em Proceedings of the IEEE Symposium on Logic in 
Computer Science, 1988}, pp. 112--120, 1988.


\bibitem {Las84}  J.-L. Lassez.  \&  Maher M J. Closure and Fairness 
in the Semantics of Logic Programming, $TCS$, 29:167\--184  1984.

\bibitem {Las87} J-L. Lassez. \& Marriot K.
Explicit Representation of Terms Defined by Counter Examples.   {\em 
Journal of Automated 
Reasoning}, 3, (3), pp. 301\--317, 1987.

\bibitem {Las88} J-L. Lassez., Maher M.J. \& Marriot K.
Unification Revisited.   In: {\em Foundations of Deductive 
Databases and Logic Programming}. Minker J. (ed.), Morgan Kaufmann, 
pp. 587 \--626, 1988.

\bibitem {Las91} J-L. Lassez., Maher M.J. \& Marriot K.
Elimination of Negation in Term Algebras.   In: {\em Mathematical 
Foundations of Computer Science}. Tarlecki A. (ed.), Springer-Verlag,
 pp. 1\--16, 1991.

\bibitem {Lev92} Levi F. Constructive Negation and Universal 
Quantification. M.S. Thesis, Universita' di Pisa, 1992.

\bibitem {Llo87} J-W. Lloyd.   {\em Foundations of Logic 
Programming}. Second Extended Edition, Springer-Verlag, Berlin, 1987. 

\bibitem {Llo84}  J-W. Lloyd.  \&  Topor R.W. Making Prolog more 
Expressive. {\em Journal of Logic Programming}, 1, 3, pp. 
225\--240,1984.

\bibitem {Llo86}  J-W. Lloyd.  \&  Topor R. W. A Basis for Deductive 
Database Systems I and II. {\em Journal of Logic Programming}, 2, 2, 
pp. 93\--109, 3, 1, pp. 56\--67, 1986.

\bibitem {Llo91}  J-W. Lloyd.  \& Shepherdson J. Partial Evaluation In 
Logic Programming, {\em Journal of Logic Programming}, v.11, pp. 
217\--242, 1991.

\bibitem  {Lov88} Loveland D. Near-Horn Prolog and Beyond, 
{\em Technical Report CS-1988-25}, Duke University, 1988.

\bibitem {Lug95} Lugiez D. Positive and Negative results for 
Higher-Order Disunfication. {\em Journal of Symbolic Computation}, 
1995.


\bibitem {Mah88} Maher M. J. Complete Axiomatization of the Algebras 
of Finite, Rational and Infinite Trees. In: {\em Proceedings of the 
IEEE Symposium on Logic in Computer Science, 1988}, pp. 348--357, 
1988.

\bibitem {Mal71} Mal'cev A.I. Axiomatixable Classes of Locally Free 
Algebrae. In {\em The Metamathematics of Algebraic Systems: Collected 
Papers, 1936--1937}, pp. 262--289, North-Holland, 1971.

\bibitem {Mal89}  Maluzinski J.  \&  Naslund T. Fail Substitutions 
for Negation as Failure. {\em Proceedings of  NACLP '89}, Lusk \& 
Overbeek (eds.), MIT Press, pp. 461\--476, 1989.

\bibitem{Man88} Mancarella P. , Martini S. \& Pedreschi D.  Complete 
Logic Programs with Domain Closure Axiom. {\em Journal of Logic 
Programming}, 5, pp. 263\--276, 1988.

\bibitem {McC86} McCarty L. F. Fixed Point Semantics and Tableau 
Proof Procedures for a Clausal Intuitionistic Logic, Technical
Report LRP-TR-18, Rutgers,1986.

\bibitem {Mil89} D. Miller. A Logical Analysis of Modules in Logic 
Programming. {\em Journal of Logic Programming}, pp. 79\--108, 1989.

\bibitem {Mil91a} D. Miller. A Logical Programming Language with 
Lambda-Abstraction, Function Variables and Simple Unification. In:
Schroder-Heister P. (ed.) {\em Extensions of Logic Programming}, LNAI 
475, Springer-Verlag, pp. 253--281, 1991.

\bibitem  {Mil91b}D. Miller., Nadathur G., F. Pfenning , Scedrov A.   
Uniform Proofs as a Foundation for Logic Programming. {\em 
Annals of Pure and Applied Logic}, 51, pp. 125\--157, 1991.

\bibitem {Mil93}  D. Miller. FORUM etc...
LICS93
\bibitem {Min82}  Minker J. On Indefinite Data Bases and the Closed 
World Assumption. {\em Proc. 6th Conf. Automated Deduction}, LNCS 
138, Springer-Verlag, Berlin, 1982.

\bibitem  {Min91} Minker J., Rajasekar A. \& Lobo J. A Theory of 
Disjunctive Logic  Programs, in: {\em Computational Logic},   Lassez
 J.L. \& Plotkin G. (eds.), MIT  Press, 1991.

\bibitem{Mis84} Mishra P. Towards a Theory of Types in Prolog.
In: {\em Proc. of the 1984 Symposium on Logic Programming}, pp.
289--298, 1984.

\bibitem  {Mom89}  A. Momigliano. {\em Prolog and Negation}, M. S.\ 
Thesis, Computing Laboratory, Department of  Mathematics, Oxford 
University, 1989.

\bibitem  {Mom92} A. Momigliano. Hereditary Harrop 
Formulae and Minimal Negation, in: {\em Logic Foundations of 
Computer Science}, Nerode A. (ed.) LNCS no. 676, Springler-Verlag, 
1992.

\bibitem  {Mom93} A. Momigliano. {\em Some Remarks on 
Uniform Proofs and Constructive Negation} ,  M. S.\  Thesis, 
Department of Philosophy, Carnegie Mellon University, 1993.


\bibitem  {Mom94a} A. Momigliano. \& Ornaghi M.  Regular Search Spaces 
as a Foundation of Logic Programming. In: {\em Extensions of Logic 
Programming},  Dyckhoff R. (ed.), LNAI no. 425, Springler-Verlag, 
1994.

\bibitem  {Mom95} A. Momigliano. \& Ornaghi M.  Regular Search Spaces 
and Constructive Negation. {\em Journal of Logic and Computation}, 7, 
3, 367--403, 1998.

\bibitem  {Mor94} Moreno Navarro J.J. Default Rules: An Extension of 
Constructive Negation for Narrowing-Based Languages, {\em ICLP94}, 
MIT Press, 1994.

\bibitem  {Mur93} Murthy C. Classical Logic as a Programming 
Language: Typing Nonlocal Control, {\em submitted}, 1993.

\bibitem  {Nad93} Nadathur G. A Proof Procedure for the Logic of 
Hereditary Harrop Formulas, {\em Journal of Automated 
Reasoning}, 11, pp. 115-145, 1993.

\bibitem  {Nai85} Naish L. {\em Negation and Control in Prolog}. LNCS 
no. 239, Springer-Verlag, 1985.

\bibitem {Nip93} T. Nipkow. Functional Unification of Patterns. 
\emph{LICS93}, 1993.

\bibitem {Oli92} Olivetti N. \& Terracini L. N-Prolog and the 
Equivalence of
Logic Program. I. {\em Logic Language and Information}, pp.
253\--339, 1992.  

\bibitem{PW90} D. Pearce \& G. Wagner. Logic Programming with Strong 
Negation. In: {\em Extensions of Logic Programming}, P. 
Schroeder-Heister (ed.) Springer LNAI 475, pp. 311-26, 1990.

\bibitem{Pfe88} F. Pfenning  \& Elliot C. Higher-Order Abstrct Syntax, 
in: {\em Proc. of SIGPLAN'88}, ACM Press, pp. 537\--551, 
1988. 

\bibitem {Pfe91a} F. Pfenning  Logic Programming in the LF 
Logical Framework, in: {\em Logical Frameworks}, Huet \& Plotkin 
(eds.) pp. 149-182, Cambridge University Press 1991.

\bibitem {Pfe91b} F. Pfenning    Unification and Anti-Unification
in the Calculus of Constructions. {\em  Proceedings of the IEEE 
Symposium on Logic in Computer Science, 1991}, pp. 74\--85, 1991.

\bibitem {Pfe92} F. Pfenning  \& Rohwedder E. Implementing the 
Metatheory of Deductive Systems. In {\em CADE-11}, Kapur (ed.), LNAI, 
Springer-Verlag, pp. 537\--551,  1992.

\bibitem {Pfe92b} Pfenning F (ed.). {\em Types In Logic Programming}, 
MIT Press, 1992.

\bibitem {Pfe93} F. Pfenning   Refinement Types for Logical 
Frameworks. In: Geuvers H. (ed.) {\em Informal Proceedings of the 
1993 Workshop on Types for Proofs and Programs},  University of 
Nijmegen, pp. 285--299, 1993.

\bibitem {Pfe9?}  F. Pfenning  Computation and Deduction, Manuscript 
199?.

\bibitem  {Pla88} Plaisted D.A.  Non Horn Logic Programming
without Contrapositives. {\em Journal of Automated Reasoning}, 4, pp. 
287-325, 1988.

\bibitem{Ras74} H. Rasiowa. {\em An Algebraic Approach to 
Non-Classical Logics}. North-Holland, Amsterdam, 1974.

\bibitem  {Ree92} Reed D. W. \& Loveland W.D. A Comparison 
of three Prolog Extensions. {\em Journal of Logic Programming},  
12, pp. 25-50, 1992.


\bibitem {Rei78}  Reiter R. On Closed World Data Bases. In  {\em 
Logic and Data Bases}, Gallaire  \&  Minker (eds.), Plenum Press, New 
York, 1978. 

\bibitem {Rob65}  Robinson J. A. A Machine-Oriented Logic Based on 
the Resolution Principle. {\em JACM}, 12, (1), pp. 23\--41, 1965.

\bibitem{Sa92} D. Shalin, T. Franzen \& S. Haradi. An Intuitionistic 
Predicate Logic Theorem Prover. {\em Journal of Logic and 
Computation}, pp. 619--656, 2, 1992.

\bibitem {Sat84} Sato T. \& Tamaki H.   Transformational Logic 
Program Synthesis. {\em Proc. Int. Conf. on Fifth Generation Computer 
Systems}, 1984. 

\bibitem {SH93} P. Schroeder-Heister. Rules of Definitional 
Reflection. In: {\em Proceedings of the IEEE Symposium on Logic in 
Computer Science}, pp. 222--232, 1993.

\bibitem {SH93} P. Schroeder-Heister. Definitional Reflection and the 
Completion. In: {\em Extensions of Logic Programming},  Dyckhoff R. 
(ed.), pp. 333--347, LNAI no. 425, Springler-Verlag, 1994.

\bibitem  {Sch92} Schwichtenberg H. Proofs as Programs. In:  {\em 
Proof Theory. A Selection of Papers from the Leeds Proof Theory 
Program 1990},  S. Wainer (Ed.), Cambridge University Press 1992.

\bibitem {She85}  Shepherdson J.C.  Negation as Failure. (II) {\em 
Journal of Logic Programming},  3, pp.185\--202, 1985. 

\bibitem {She88} Shepherdson J.C. Negation in Logic 
Programming. In: {\em Foundations of Deductive Databases 
and Logic Programming}, Minker J. (ed.), Morgan Kaufmann, 1988.

\bibitem {She89}  Shepherdson J.C. A Sound and Complete Semantics for 
a Version of NF. {\em TCS}, 65(3): 343\--371, 1989

\bibitem {Sny89} W. Snyder \& J.H. Gallier. Higher-Order Unification 
Revisited: Complete Sets of Transformations. {\em Journal of Symbolic 
Computation}, 8:101-140, 1989.

\bibitem  {Sny91} W. Snyder. {\em A Proof Theory for General 
Unification}. Birkhauser, Boston 1991.

\bibitem  {St92a} St\"{a}rk  R. {\em The Proof-Theory of Logic 
Programs with Negation}. PhD. Thesis, University of Bern, 1992.

\bibitem  {St92b} St\"{a}rk  R. Cut-Property and Negation as Failure, 
{\em Technical Report}, University of Bern, 1992.

\bibitem  {St93} St\"{a}rk  R. From Logic Programs to Inductive 
Definitions. {\em Technical Report}, University of M\"{u}nchen, 199e.

\bibitem  {Sti88} Stickel M. A Prolog Technology Theorem 
Prover: a New Exposition and Implementation in Prolog. {\em 464 SRI 
International, Technical Note}, 46, 4. Menlo Park, California, 1989. 

\bibitem {Stu91}  Stuckey P. Constructive Negation for Constraint 
Logic Programming, {\em Proceedings of the IEEE Symposium on Logic in 
Computer Science}, pp. 328\--339, 1991.

\bibitem {Tam84} Tamaki H. \& Sato T.   Unfold/Fold Transormation of 
Logic Programs. {\em Proc. ICLP84}, pp. 127\--138, 1984.

\bibitem {Tar77}  Tarnlund S. A. Horn Clause Computability. {\em 
BIT}, 17, 2 pp. 215\--226, 1977.

\bibitem {Thi84} J.J. Thiel. Stop Losing Sleep over Incomplete 
Specifications. {\em Proc. of 11th POPL}, 1984.

\bibitem {Tro88} Troesltra A.S. \& van Dalen D. {\em 
Constructivism in Mathematics,} vol 1-2. North-Holland, Amsterdam, 
1988.

\bibitem {Van76}  Van Emden M.H.  \&  Kowalski R.A. The Semantic of 
Predicate Logic as a Programming Language. {\em JACM}, vol. 23, no. 
4, pp. 733\--742, 1976. 

\bibitem{Wag91a}  G. Wagner. A Database Needs two kinds of Negation. 
In: {\em Proc. of Mathematical Fundamentals of Database and Knowledge 
Systems}, Springer, LNCS 495, pp. 357--371, 1991. 

\bibitem{Wag91}  G. Wagner. Logic Programming with Strong Negation 
and Inexact Predicates, {\em JLC}, pp. 835-8601,6, 1991. 

\bibitem {Wal87}  Wallace M. Negation by Constraints: a Sound and 
Efficient Implementation of Negation in Deductive Databases. {\em 
Proc. 1987 Symp. on Logic Programming}, Computer Society Press, pp. 
253\--263, 1987.

\bibitem {Wan91} H. Wansig. {\em The Logic of Information 
Structures}, Springer LNAI 681, 1991.

\bibitem {Wos91} Wos L. \& McCune W. Automated Theorem 
Proving and Logic Programming: A Natural Symbiosis. {\em Journal 
of Logic Programming}, pp. 1\--53, 1991.

\bibitem{Yar91} Yardeni E. \& Shapiro E. A Type System for Logic 
Programs. {\em Journal of Logic Programming}, 10, pp. 125--153, 1991.


\end{thebibliography}

