Negation elimination in equational formulae
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” . 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.
KeywordsTransformation Rule Equational Problem Ground Instance Equational Formula Logic Programming Language
Unable to display preview. Download preview PDF.
- 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
- Hubert Comon. Complete axiomatization.s of some quotient term algebras. In Proc. ICALP, Madrid, LNCS 510, July 1991.Google Scholar
- 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
- 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
- Maribel Fernández. Equational disunification. To appear in Applicable Algebra in Engineering, Communications and Computing, 1991.Google Scholar
- 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
- 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
- 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
- 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
- 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
- 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