Negation Elimination in Empty or Permutative Theories

An equational formula is a first-order formula over an alphabet of function symbols and the equality predicate. Such formulae are interpreted in the algebraT( ) of ground terms. A unification problem is an equational formula which does not contain negation (in particular no disequation). We give a terminating set of transformation rules such that a formula is semantically equivalent to a unification problem iff its irreducible form is a unification problem. More precisely, our set of transformation rules computes a finite complete set of most general unifiers for an equational formula each time such a finite set exists, thus extending the results of Lassez and Marriott on explicit representation of terms defined by counter examples. We extend the above results also to equational formulae interpreted inT( )/ = E, the quotient of the free algebra by a congruence generated by a setEof shallow permutative equations (commutative axioms are a particular case).