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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D. Chan, Constructive Negation based on Completed Database, Proc. 5th Symposium on Logic Programming, 111–125, 1988.
D. Chan, An Extension of Constructive Negation and its Application in Coroutining, Proc. North American Conf. on Logic Programming, Cleveland, 477–493, 1989.
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.
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.
H. Comon, Disunification: A Survey, in: Computational Logic, J-L. Lassez & G. Plotkin (Eds.), MIT Press, 1991.
N. Dershowitz and J-P. Jouannaud, Rewrite Systems. Handbook of Theoretical Computer Science, (J. van Leeuwen Ed.), Elsevier Science Publishers, 243–320.
A. Frisch & C.D. Page Jr., Generalization with Taxonomic Information, Proc. AAAI-90, Boston, 755–761, 1990.
J.V. Guttag, Abstract Data Types and the Development of Data Structures. Communications of the ACM, 20(6), 396–404, 1977.
G. Huet, Résolution d'Equations Dans Des Langages D'Ordre 1,2,..., ω (Thèse d'Etat), Université de Paris VII, 1976.
G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, JACM, Vol. 27, No. 4, Oct. 1980, 797–821.
J. Jaffar & J-L. Lassez, Constraint Logic Programming, Proc. Conf. on Principles of Programming Languages, 111–119, 1987.
J. Jaffar, J-L. Lassez & J.W. Lloyd, Completeness of the Negation as Failure Rule, Proc. IJCAI, Karlsruhe, 500–506, 1983.
D. Kapur, P. Narendran and H. Zhang, On Sufficient Completeness and Related Properties of Term Rewriting Systems. Acta Informatica 24, 395–415, 1987.
E. Kounalis, An Algorithm For Learning from Examples and Counter Examples, manuscript, 1989.
E. Kounalis, Pumping Lemmas For Tree Languages Generated by Rewrite Systems, Mathematical Foundations of Computer Science, 1990.
E. Kounalis and M. Rusinowitch, Discovering New Facts For First Order Knowledge Based Systems, 4th International Symposium on AI, Spain, 1990.
E. Kounalis, Completeness in Data Type Specifications. Proc. of EUROCAL '85 Conference, Lecture Notes in Computer Science Vol. 204, Springer-Verlag, 348–362, 1985.
K. Kunen, Answer Sets and Negation as Failure, Proc. 4th. Int. Conf. on Logic Programming, Melbourne, 219–228, 1987.
K. Kunen, Negation in Logic Programming, Journal of Logic Programming, 4, 289–308, 1987.
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.
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.
J-L Lassez, K. McAloon, A Constraint Sequent Calculus LICS 90. Philadelphia.
J-L. Lassez and K. McAloon, A Canonical Form for Generalized Linear Constraints, Journal of Symbolic Computation, to appear.
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.
A. Lazrek, P. Lescanne and J-J. Thiel, Tools for Proving Inductive Equalities, Relative Completeness, and ω-Completeness. Information and Computation 84, 47–70, 1990.
J.W. Lloyd, Foundations of Logic Programming, Springer-Verlag, 1987.
D. Lugiez, A Deduction Procedure for First Order Programs, Proc. ICLP-6, 585–599, 1989.
M.J. Maher, Logic Semantics for a Class of Committed-choice Programs, Proc. 4th. Int. Conf. on Logic Programming, Melbourne, 858–876, 1987.
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.
M.J. Maher, On Parameterized Substitutions, IBM Research Report, T.J. Watson Research Center, 1990.
M.J. Maher & P.J. Stuckey, On Inductive Inference of Cyclic Structures, International Symposium on Artificial Intelligence and Mathematics, Ft. Lauderdale, 1990.
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.
L. Naish, Negation and Control in Prolog, Lecture Notes in Computer Science 238, Springer-Verlag, 1986.
C.D. Page Jr. & A. Frisch, Generalizing Atoms in Constraint Logic, Proc. Conf. on Knowledge Representation and Reasoning, San Mateo, 1991.
S.L. Peyton Jones, The Implementation of Functional Programming Languages, Prentice Hall, 1987.
G.D. Plotkin, A Note on Inductive Generalization, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970, 153–163.
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.
J.C. Reynolds, Transformational Systems and the Algebraic Structure of Atomic Formulas, Machine Intelligence 5, (B. Meltzer & D. Michie Eds.), 1970, 135–152.
T. Sato & H. Tamaki, Transformational Logic Programming Synthesis, Proc. FGCS'84, Tokyo, 195–201, 1984.
Ph. Schnoebelen, Refined Compilation of Pattern-matching for Functional Languages, Proc. Workshop on Algebraic and Logic Programming, LNCS 343, 233–243, 1988.
P.J. Stuckey, Constructive Negation for Constraint Logic Programming, Proc. 6th Symp. on Logic in Computer Science, to appear.
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.
M. Wallace, Negation By Constraints: A Sound and Efficient Implementation of Negation in Deductive Databases, Proc. 1987 Symposium on Logic Programming, 253–263, 1987.
Author information
Authors and Affiliations
Editor information
Rights 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