# Negation elimination in equational formulae

## Abstract

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*.

## Keywords

Transformation Rule Equational Problem Ground Instance Equational Formula Logic Programming Language## Preview

Unable to display preview. Download preview PDF.

## References

- [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]Hubert Comon. Complete axiomatization.s of some quotient term algebras. In
*Proc. ICALP, Madrid, LNCS 510*, July 1991.Google Scholar - [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]Hubert Comon and Pierre Lescanne. Equational problems and disunification.
*J. Symbolic Computation*, 7:371–425, 1989.zbMATHMathSciNetCrossRefGoogle Scholar - [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]Maribel Fernández. Equational disunification. To appear in
*Applicable Algebra in Engineering, Communications and Computing*, 1991.Google Scholar - [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]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]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]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]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]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]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