Negation elimination in equational formulae

Extended abstract
  • Hubert Comon
  • Maribel Fernández
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 629)


An equational formula is a first order formula over an alphabet F of function symbols and the equality predicate symbol. Such formulae are interpreted in the algebra T(F) of finite trees. An equational formula is w.e.d. (without equations in disjunctions) if its solved forms do not contain any subformula s = t V u ≠ v. A unification problem is any equational problem which does not contain any negation (in particular, it should not contain any disequation). We give a terminating set of transformation rules such that a w.e.d. formula φ is (semantically) equivalent to a unification problem iff its irreducible forn is a unification problem. This result can be formulated in another way: our set of transformation rules computes a finite complete set of “most general unifiers” for a w.e.d. formula each time such a finite set exists. Such results extend Lassez and Marriott results on “explicit representation of terms defined by counter-examples” [10]. The above results are extended to quotients of the free algebra by a congruence =e which can be generated by a set of shallow permulative equations E.


Transformation Rule Equational Problem Ground Instance Equational Formula Logic Programming Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    H. Comon and M. Fernandez. Negation elimination in equational formulae. Research Report 716, Laboratoire de Recherche en Informatique, Univ. Paris-Sud, France, December 1991.Google Scholar
  2. [2]
    Hubert Comon. Complete axiomatization.s of some quotient term algebras. In Proc. ICALP, Madrid, LNCS 510, July 1991.Google Scholar
  3. [3]
    Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.Google Scholar
  4. [4]
    Hubert Comon and Pierre Lescanne. Equational problems and disunification. J. Symbolic Computation, 7:371–425, 1989.zbMATHMathSciNetCrossRefGoogle Scholar
  5. [5]
    Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.Google Scholar
  6. [6]
    Maribel Fernández. Equational disunification. To appear in Applicable Algebra in Engineering, Communications and Computing, 1991.Google Scholar
  7. [7]
    Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991.Google Scholar
  8. [8]
    Claude Kirchner, Helene Kirchner, and Michael Rusinowitch. Deduction with symbolic constraints. Revue Française d'Intelligence Artificielle, 4(3):9–52, 1990. Special issue on automatic deduction.Google Scholar
  9. [9]
    J.-L. Lassez, M. Maher, and K. Marriott. Elimination of negation in term algebras. In Proc. 16th Mathematical Foundations of Computer Science 91, Warsaw. Springer-Verlag, 1991.Google Scholar
  10. [10]
    J.-L. Lassez and K. G. Marriott. Explicit representation of terms defined by counter examples. J. Automated Reasoning, 3(3):1–17, September 1987.MathSciNetCrossRefGoogle Scholar
  11. [11]
    M. J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, pages 348–357, July 1988.Google Scholar
  12. [12]
    A. I. Mal'cev. Axiomatizable classes of locally free algebras of various types. In The Metamathematics of Algebraic Systems. Collected Papers. 1936–1967, pages 262–289. North-Holland, 1971.Google Scholar
  13. [13]
    M. Tajine. Representation explicite de certains langages de termes: théorie et applications. Thèse de l'université Louis Pasteur de Strasbourg, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Hubert Comon
  • Maribel Fernández
    • 1
  1. 1.CNRS and LRI, Bat. 490Université de Paris SudOrsay cedexFrance

Personalised recommendations