Skip to main content

Elimination of negation in term algebras

  • Invited Lectures
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1991 (MFCS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 520))

Abstract

We give an informal review of the problem of eliminating negation in term algebras and its applications. The initial results appear to be very specialized with complex combinatorial proofs. Nevertheless they have applications and relevance to a number of important areas: unification, learning, abstract data types and rewriting systems, constraints and constructive negation in logic languages.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Chan, Constructive Negation based on Completed Database, Proc. 5th Symposium on Logic Programming, 111–125, 1988.

    Google Scholar 

  2. D. Chan, An Extension of Constructive Negation and its Application in Coroutining, Proc. North American Conf. on Logic Programming, Cleveland, 477–493, 1989.

    Google Scholar 

  3. H. Comon, Sufficient Completeness, Term Rewriting Systems and Anti-Unification. Proc. 8th Conference on Automated Deduction (J. Siekmann, Ed.), Lecture Notes in Computer Science Vol. 230, Springer-Verlag, 128–140, 1986.

    Google Scholar 

  4. H. Comon, An Effective Method for Handling Initial Algebras. Proc. 1st International Workshop on Algebraic and Logic Programming, Lecture Notes in Computer Science Vol. 343, Springer-Verlag, 108–118, 1988.

    Google Scholar 

  5. H. Comon, Disunification: A Survey, in: Computational Logic, J-L. Lassez & G. Plotkin (Eds.), MIT Press, 1991.

    Google Scholar 

  6. N. Dershowitz and J-P. Jouannaud, Rewrite Systems. Handbook of Theoretical Computer Science, (J. van Leeuwen Ed.), Elsevier Science Publishers, 243–320.

    Google Scholar 

  7. A. Frisch & C.D. Page Jr., Generalization with Taxonomic Information, Proc. AAAI-90, Boston, 755–761, 1990.

    Google Scholar 

  8. J.V. Guttag, Abstract Data Types and the Development of Data Structures. Communications of the ACM, 20(6), 396–404, 1977.

    Google Scholar 

  9. G. Huet, Résolution d'Equations Dans Des Langages D'Ordre 1,2,..., ω (Thèse d'Etat), Université de Paris VII, 1976.

    Google Scholar 

  10. G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, JACM, Vol. 27, No. 4, Oct. 1980, 797–821.

    Google Scholar 

  11. J. Jaffar & J-L. Lassez, Constraint Logic Programming, Proc. Conf. on Principles of Programming Languages, 111–119, 1987.

    Google Scholar 

  12. J. Jaffar, J-L. Lassez & J.W. Lloyd, Completeness of the Negation as Failure Rule, Proc. IJCAI, Karlsruhe, 500–506, 1983.

    Google Scholar 

  13. D. Kapur, P. Narendran and H. Zhang, On Sufficient Completeness and Related Properties of Term Rewriting Systems. Acta Informatica 24, 395–415, 1987.

    Google Scholar 

  14. E. Kounalis, An Algorithm For Learning from Examples and Counter Examples, manuscript, 1989.

    Google Scholar 

  15. E. Kounalis, Pumping Lemmas For Tree Languages Generated by Rewrite Systems, Mathematical Foundations of Computer Science, 1990.

    Google Scholar 

  16. E. Kounalis and M. Rusinowitch, Discovering New Facts For First Order Knowledge Based Systems, 4th International Symposium on AI, Spain, 1990.

    Google Scholar 

  17. E. Kounalis, Completeness in Data Type Specifications. Proc. of EUROCAL '85 Conference, Lecture Notes in Computer Science Vol. 204, Springer-Verlag, 348–362, 1985.

    Google Scholar 

  18. K. Kunen, Answer Sets and Negation as Failure, Proc. 4th. Int. Conf. on Logic Programming, Melbourne, 219–228, 1987.

    Google Scholar 

  19. K. Kunen, Negation in Logic Programming, Journal of Logic Programming, 4, 289–308, 1987.

    Google Scholar 

  20. J-L. Lassez, M.J. Maher & K.G. Marriott, Unification Revisited, in: Foundations of Deductive Database and Logic Programming, J. Minker (Ed.), Kauffman, 587–625, 1988. Also in Proc. Workshop on Foundations of Logic and Functional Programming, LNCS 306, 1986.

    Google Scholar 

  21. J-L. Lassez & K.G. Marriott, Explicit Representation of Terms Defined by Counter Examples, Journal of Automated Reasoning, 3, 301–317, 1987. Preliminary version in Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS 241, 1986.

    Google Scholar 

  22. J-L Lassez, K. McAloon, A Constraint Sequent Calculus LICS 90. Philadelphia.

    Google Scholar 

  23. J-L. Lassez and K. McAloon, A Canonical Form for Generalized Linear Constraints, Journal of Symbolic Computation, to appear.

    Google Scholar 

  24. A. Laville, Lazy Pattern Matching in the ML Language, Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, Pune, LNCS 287, 400–419, 1987.

    Google Scholar 

  25. A. Lazrek, P. Lescanne and J-J. Thiel, Tools for Proving Inductive Equalities, Relative Completeness, and ω-Completeness. Information and Computation 84, 47–70, 1990.

    Google Scholar 

  26. J.W. Lloyd, Foundations of Logic Programming, Springer-Verlag, 1987.

    Google Scholar 

  27. D. Lugiez, A Deduction Procedure for First Order Programs, Proc. ICLP-6, 585–599, 1989.

    Google Scholar 

  28. M.J. Maher, Logic Semantics for a Class of Committed-choice Programs, Proc. 4th. Int. Conf. on Logic Programming, Melbourne, 858–876, 1987.

    Google Scholar 

  29. M.J. Maher, Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees, Proc. 3rd. Symp. Logic in Computer Science, Edinburgh, 348–357, 1988. Full version: IBM Research Report, T.J. Watson Research Center.

    Google Scholar 

  30. M.J. Maher, On Parameterized Substitutions, IBM Research Report, T.J. Watson Research Center, 1990.

    Google Scholar 

  31. M.J. Maher & P.J. Stuckey, On Inductive Inference of Cyclic Structures, International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, 1990.

    Google Scholar 

  32. D.L. Musser, On Proving Inductive Properties of Abstract Data Types. Proc. 7th ACM Symp. on Principles of Programming Languages, ACM Press, 154–162, 1980.

    Google Scholar 

  33. L. Naish, Negation and Control in Prolog, Lecture Notes in Computer Science 238, Springer-Verlag, 1986.

    Google Scholar 

  34. C.D. Page Jr. & A. Frisch, Generalizing Atoms in Constraint Logic, Proc. Conf. on Knowledge Representation and Reasoning, San Mateo, 1991.

    Google Scholar 

  35. S.L. Peyton Jones, The Implementation of Functional Programming Languages, Prentice Hall, 1987.

    Google Scholar 

  36. G.D. Plotkin, A Note on Inductive Generalization, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970, 153–163.

    Google Scholar 

  37. H. Przymusinska & T. Przymusinski, Semantic Issues in Deductive Databases and Logic Programs, in: Sourcebook on the Formal Approaches in Artificial Intelligence, A. Banerji (Ed.), North-Holland, to appear.

    Google Scholar 

  38. J.C. Reynolds, Transformational Systems and the Algebraic Structure of Atomic Formulas, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970, 135–152.

    Google Scholar 

  39. T. Sato & H. Tamaki, Transformational Logic Programming Synthesis, Proc. FGCS'84, Tokyo, 195–201, 1984.

    Google Scholar 

  40. Ph. Schnoebelen, Refined Compilation of Pattern-matching for Functional Languages, Proc. Workshop on Algebraic and Logic Programming, LNCS 343, 233–243, 1988.

    Google Scholar 

  41. P.J. Stuckey, Constructive Negation for Constraint Logic Programming, Proc. 6th Symp. on Logic in Computer Science, to appear.

    Google Scholar 

  42. J-J. Thiel, Stop Losing Sleep Over Incomplete Data Type Specifications. Proc. 11th ACM Symp. on Principles of Programming Languages, ACM Press, 76–82, 1984.

    Google Scholar 

  43. M. Wallace, Negation By Constraints: A Sound and Efficient Implementation of Negation in Deductive Databases, Proc. 1987 Symposium on Logic Programming, 253–263, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Andrzej Tarlecki

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lassez, JL., Maher, M., Marriott, K. (1991). Elimination of negation in term algebras. In: Tarlecki, A. (eds) Mathematical Foundations of Computer Science 1991. MFCS 1991. Lecture Notes in Computer Science, vol 520. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54345-7_44

Download citation

  • DOI: https://doi.org/10.1007/3-540-54345-7_44

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54345-9

  • Online ISBN: 978-3-540-47579-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics