Negation Elimination in Equational Formulae (Extended Abstract)

Hubert Comon and Maribel Fernández^{∗}

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 ∨ 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 form 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 permutative equations E.

Introduction

Terms with variables serve as a basis in many areas of computer science to denote the (possibly infinite) set of their ground instances. This is for example the case in all functional or logic programming languages. Therefore basic operations on terms are fundamental in many programming activities. Examples of such operations are the computation of the greatest lower bound (unification) and the computation of the smallest upper bound (anti-unification) of two terms. Let [[t_{1}, …, t_{n}]] be the set of all ground instances of t_{1}, …, t_{n}. The first operation (unification) can be reflected at the level of ground instances: to unify s and t (which are defined up to literal similarity) corresponds to the computation of [[s]] ∩ [[t]].

Another (less well-known) operation on terms has revealed to be fundamental: the term complement, i.e. the computation of the difference set [[t]] − [[u_{1}, …, u_{m}]]. Some applications of such computations are described in [3, 9]. This difference cannot always be expressed as a finite set [[v_{1}, …, v_{k}]] and Lassez and Marriott gave in [10] a precise characterization of the cases in which the difference is expressible within the same formalism.

The computation of term complement, as well as unification and other operations are actually nothing but particular cases of solving equational formulae. An equational formula is a first-order formula constructed over a finite alphabet F of function symbols and only one relational symbol: the equality. It has been shown that the validity of an equational formula in the free term algebra T (F) is decidable [12, 4, 11], leading to a complete axiomatization of T (F). The technique of [4] consists in reducing the formula (according to a set of rewrite rules) until a solved form is reached. In the unification case, a solved form can be for example a formula x_{1} = t_{1} ∧ … ∧ x_{n} = t_{n} where x_{1}, …, x_{n} are variables which occur only once. Such a solved form represents a most general unifier in a straightforward way (see [7] for more information about solved forms of unification problems). In this view, solving equational formulae encompasses unification, as unification consists only in solving an equation s = t, but also encompasses term complement as the computation of [[t]]−[[u_{1}, …, u_{m}]] consists in solving the formula

∗CNRS and LRI, Bat. 490, Université de Paris Sud, 91405 ORSAY cedex, France. E-mail {comon,maribel}@lri.lri.fr

∃Var(t), ∀Var(u_{1}, …, u_{m}) : x = t ∧ x ≠ u_{1} ∧ … ∧ x ≠ u_{m}

where Var(t), Var(u_{1}, …, u_{m}) denote the set of variables in t and u_{1}, …, u_{n} respectively.

However there are good reasons for which we would like the solved forms to have an additional property: to involve only equations, if this is possible. More precisely, let [[ϕ]] be the set of ground assignments σ to the free variables of ϕ such that T (F) ⊧ ϕσ. We would like that a solved form ϕ′ of ϕ does not contain any disequation whenever there is such a formula ψ satisfying [[ψ]] = [[ϕ]]. Indeed, for a formula ϕ that satisfies these requirements, there are finitely many substitutions θ_{1}, … θ_{k} such that [[ϕ]] is exactly the set of ground instances of θ_{1}, …, θ_{k}. In other words, we would like to compute a finite set of generating substitutions θ_{1}, …, θ_{k} as soon as such a finite set exists. In the case of complement problems, this implies that we compute a finite set of terms v_{1}, … v_{k} such that [[t]] − [[u_{1}, …, u_{m}]] = [[v_{1}, …, v_{k}]] as soon as such a set exists.

Good reasons for these additional requirements on solved forms are described in [9], but let us mention another motivation. Constraints systems are very useful in logic programming languages because they provide with adequate notations for specific computation domains. In particular, strategies can be expressed using constraints over T (F). In the same way constraints enhance both efficiency and expressiveness in equational logic computations [8]. For example, a single constrained equation can be used in place of a huge (or even infinite) set of equations. However, the drawback is the failure of the critical pair lemma: in any constrained version of rewriting, there are constrained rules without critical pairs (in the classical sense) which do not define a locally confluent rewrite system. Recent trends in rewrite systems theory undertake this problem^{1}. A simple way for handling the problem is to assume that every constraint can (eventually) be turned into equations only. Indeed, this means that, when necessary, it is possible to turn the constrained equations into unconstrained ones. Of course, for such constraints systems, the expressivity of equational logic is not really increased, but it is still possible to delay expensive computations until they are necessary (with the hope that they will never be necessary). This is widely demonstrated in [8]. Now, since equational formulae are a possible constraint language, it is worthwhile to study the ability of turning such formulae into equations only, which is the subject of this paper.

For all these reasons, the main goal of our work is to give a terminating set of rules on equational formulae for which the irreducible formulae do not contain disequations if they are equivalent in T (F) or T (F)/_{=_{E}} to a formula which does not contain any disequation. The first step towards this goal is to eliminate the quantifiers: using a procedure such as those described in [4], it is possible to transform any equational formula into a (semantically equivalent) purely existential formula. Therefore, we have only to consider purely existential formulae. Unfortunately, we were not able to solve the general case of existential formulae (this is still an open question^{2}); our paper shows how to achieve our goal for formulae which do not contain subformulae of the form s = t∨u ≠ v. We can still show that this case covers all known solved cases; for example complement problems fall into the scope of our work. For such problems, our technique works in a different way than [10]: Lassez and Marriott reduce some conjunctions of equations and disequations to complement problems for which they give syntactic conditions for eliminating negation. We proceed in the reverse way: complement problems are reduced to existential formulae which are in turn simplified to solved forms. These solved forms do not involve negation iff the original complement problem can be expressed without negation. As in [10] they had to prove some results on non-expressibility by means of equations of some complement problems, we have to show some non-equivalence results of some formulae by means of equations only. These results, which give necessary conditions for negation elimination to be possible, are interesting for their own.

1There is not any published paper yet, but the problem of constrained completion of rewrite systems was one of the major themes of the 1st Int. Workshop on Constraint Theorem Proving, Dagstuhl, Oct.

1991.

2In the meantime it has been solved for T (F) by M. Tajine [13]

Also, in a final section, we extend our results to quotient algebras. But in order to preserve decidability we assume that the congruence =_{E} is generated by a permutative set of equations (in Mal’cev’s sense [12] ). With such a restriction, all previous results which were established for T (F) carry over T (F)/_{=_{E}}.

We give some basic definitions about equational formulae in section 1. Then we give our set of transformation rules in section 2. In section 3 we state some basic results about non-equivalence with negation-free problems and show the completeness of the set of transformation rules. In section 4 we show how to extend our results to some quotient algebras.

1 Equational Formulae

1.1 Syntax

We refer to [5] for missing definitions and notations. F will always be a finite set of function symbols together with their (fixed) arity. T (F) is the set of (ground) terms over this alphabet. It will be assumed infinite. Variables are an infinite distinguished set of constants X. The set of terms built on F and X is denoted T (F, X).

An equation s = t is a pair of terms s, t ∈ T (F, X). A disequation s ≠ t is a pair of terms s, t ∈ T (F, X). An equational formula is a first order formula whose atoms are equations or disequations. For simplicity, we will always assume that each variable is bound at most once in a formula and cannot occur both free and bound in the same formula. We use abbreviations such as x⃗, w⃗, y⃗ to denote finite sets of variables. We will consider a number of particular fragments, corresponding to specific syntactic constructions of formulae:

• An equational problem is either ⊤, ⊥ or a formula ∃x⃗, ∀y⃗ : P where P (the matrix of the problem) is a conjunction of disjunctions of equations and disequations. This conjunctive normal form of P will always be assumed to be kept along transformations, by using the appropriate normalization rules. ≡ will denote the equality of equational problems (modulo the normalization rules) as well as the equality of trees.

• An existential formula is a disjunction of equational problems that do not involve the quantifier ∀.

• An equational problem P is w.e.d. (“without equations in disjunctions”) if its matrix is a conjunction of equations and disjunction of disequations. In other words, the matrix of a w.e.d. problem should not contain disjunctions of the form s = t ∨ u ≠ v.

• A unification problem is an existential formula which does not contain any disequation.

1.2 Semantics

Given an F-algebra A, an A-assignment is a mapping σ which associates to each variable an element of A. Such mappings are lifted to F-homomorphisms from T (F, X) to A in the usual way. When A is T (F, X) itself, and when {x ∈ X | xσ ≢ x} = Dom(σ) (called the domain of σ) is finite, σ is called a substitution. When A = T (F), σ is called a ground assignment. The set of all ground assignments (resp. substitutions) is denoted by Σ_{g} (resp. Σ). Substitutions and assignments will be used in postfix notation.

The set of solutions of an equational formula ϕ is the set of ground assignments σ such that T (F) ⊧ ϕσ. The set of solutions of ϕ will be denoted [[ϕ]]. We also consider interpretations in quotient algebras T (F)/_{=_{E}} where =_{E} is the smallest congruence on T (F, X) containing the set of equations E. Then, an E-solution of ϕ is a ground assignment σ such that T (F)/_{=_{E}} ⊧ ϕσ. The set of E-solutions of ϕ is denoted [[ϕ]]_{E}.

Two equational formulae ϕ and ψ are equivalent (resp. E-equivalent) if they have the same set of solutions, i.e., ϕ ∼ ψ iff [[ϕ]] = [[ψ]] (resp. ϕ ∼_{E} ψ iff [[ϕ]]_{E} = [[ψ]]_{E}). For example, every unification problem is equivalent to either ⊤ or ⊥ or to a finite disjunction of formulae of the form ∃z_{1}, …, z_{m} : x_{1} = t_{1} ∧ … ∧ x_{n} = t_{n} where x_{1}, …, x_{n} are the free variables of the unification problem and occur only once in the conjunction. This latter kind of formula can be identified with the substitution σ = {x_{1} ↦ t_{1}; … x_{n} ↦ t_{n}} which is called a generator of the set of solutions: [[∃z_{1}, …, z_{m} : x_{1} = t_{1} ∧ … ∧ x_{n} = t_{n}]] = {σθ | θ ∈ Σ_{g}}. More generally, a generator of a set of solutions (resp. E-solutions) of ϕ is a substitution σ whose all ground instances are solutions (resp. E-solutions) of ϕ. A set of generators S is complete (for ϕ) if all solutions (resp. E-solutions) of ϕ are instances of some generator σ ∈ S.

An equational formula ϕ has the E_{U} (“equivalent to unification problems”) property if there is a unification problem ψ such that ϕ ∼ ψ.

Example 1 The following formulae do all have the E_{U} property and will demonstrate some transformation rules in the following:

• x ≠ y ∨ x ≠ f(y) which is equivalent to ⊤

• x ≠ 0 which is equivalent to ∃z : x = s(z) if F = {0, s}

• ∃w_{1}, w_{2}, ∀y : (y ≠ f(w_{1}, w_{1}) ∨ y ≠ f(w_{2}, w_{2})) ∧ x = g(w_{1}) which is equivalent to ∃w_{1} : x = g(w_{1})

• ∃z : y ≠ s(x) ∨ x = s(z) which is equivalent to ∃z : x = s(z) ∨ y = 0 ∨ y = s(s(z)) if F = {0, s}

The three first problems are w.e.d. Therefore, our algorithm will find the equivalent unification problems. However it will fail on the last problem which is not w.e.d.

2 Transformation Rules

2.1 From Equational formulae to existential formulae

Using the set of rules which are given in e.g. [4], it is possible to transform any equational formula into an equivalent finite set of existential formulae. Moreover, the transformation enjoys a number of interesting properties. We summarize them below.

Lemma 1 There is a terminating set of transformation rules which yields, when applied to an equational formula ϕ, a finite set of formulae ϕ_{1}, …, ϕ_{n} such that

• Each ϕ_{i} is of the form ∃ \overrightarrow{x_{i}} : P_{i} where P_{i} is quantifier-free

• [[ϕ]] = [[ϕ_{1}]] ∪ … ∪ [[ϕ_{n}]]

• If ϕ is w.e.d. then every ϕ_{i} is w.e.d.

• ϕ has the property E_{U} iff every ϕ_{i} has the property E_{U}.

Replacements (R)

(R_{1}) ∃w⃗ : z = t ∧ P → ∃w⃗ : z = t ∧ P {z ↦ t}

If z ∉ V ar(t), z ∈ V ar(P), and either t is not a variable or t occurs in P or else z ∈ w⃗ and t ∉ w⃗.

(R_{2}) ∃w⃗ : P ∧ (z ≠ t ∨ Q) → ∃w⃗ : P ∧ (z ≠ t ∨ Q{z ↦ t})

If 1. , z ∉ V ar(t), z ∈ V ar(Q) 2. there is no variable occurring both in z ≠ t ∨ Q and as a member of an equation of P 3. If t is a variable, then t occurs in Q.

Figure 1: Replacement rules

2.2 A short description of the set of rules

Now, we come to the set of transformation rules for existential formulae. We use a number of classical rules which are given in [4]. But eliminating negation requires some additional rules (which make the termination proof much more difficult than in [4]). Let us motivate and introduce these new rules.

• A problem such as x ≠ y ∨ x ≠ f(y) would be considered as the disjunction of two solved forms, according to [4] and, indeed, from the solvability point of view, we do not need any further simplification. However, this problem is obviously equivalent to ⊤, which is a unification problem. This shows that we need an additional rule: (R_{2}) in figure 1 will simplify such disjunctions, replacing x with y (or with f(y) in the disjunction: x ≠ y ∨ x ≠ f(y) →_{R_{2}} x ≠ y ∨ y ≠ f(y) →_{O_{2}} ⊤.

• Assuming that F = {0, s}, the formula x ≠ 0 is equivalent to ∃z : x = s(z) and negation can therefore be eliminated. More generally, we have to use the domain closure axiom, not only for quantifier elimination, but also for eliminating disequations whose one member is a ground term. That is what is expressed in the rule (Ex) of figure 2.

• Finally, it should be emphasized that some disequations can be removed because their variables are existentially quantified. For example ∃w_{1}, w_{2} : x = y ∧ w_{1} ≠ w_{2} is equivalent to x = y which is a unification problem. More generally, existentially quantified variables should be eliminated “as far as possible”. That what do the rules (EQE_{i}) in figure 2. The fact that they indeed have been eliminated “as far as possible” is part of the completeness result of the next section.

In addition to the rules of figures 1 and 2, we use the Merge, Decomposition, Clash, Occur-check and elimination of trivial equations or disequations rules which are recalled in figure 3. All these rules define in a self-evident way a rewrite system R on disjunctions of equational problems.

2.3 Correctness and termination

The first correctness result states that the set of solutions is always preserved by application of a rule in R. The second lemma shows that the restriction to w.e.d. problem is a sound assumption since it is preserved by application of R. Finally, the third lemma shows that each disjunct of an existential formula may be considered separately.

Explosion (E)

(Ex) ∃w⃗ : P → ⋁_{f∈F} ∃w⃗, w⃗′ : x = f(w⃗′) ∧ P {x ↦ f(w⃗′)}

If 1. P is quantifier-free and V ar(P) ∩ w⃗′ = ∅ 2. No other rule can be applied

3. There is a disequation x ≠ u in P where u is a ground term

Existential Quantifier Elimination (EQE)

(EQE_{1}) ∃w⃗, w : P → ∃w⃗ : P

If w ∉ V ar(P).

(EQE_{2}) ∃w⃗, w : w = t ∧ P → ∃w⃗ : P

If w ∉ V ar(P, t).

(EQE_{3}) ∃w⃗ : (d_{1} ∨ z_{1} ≠ u_{1}) ∧ … ∧ (d_{n} ∨ z_{n} ≠ u_{n}) ∧ P → ∃w⃗ : P

If 1. for all i, z_{i} is a variable and z_{i} ≢ u_{i}.

2. There is a variable w ∈ w⃗ ∩ V ar(z_{1}, u_{1}) ∩ … ∩ V ar(z_{n}, u_{n}) s.t. w ∉ V ar(P)

Figure 2: Explosion and Elimination of existential quantifier rules

Decompositions (D)

\begin{aligned}(D_{1}) & f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) & → & s_{1} = t_{1} ∧ … ∧ s_{n} = t_{n} \\ (D_{2}) & f(s_{1}, …, s_{n}) ≠ f(t_{1}, …, t_{n}) & → & s_{1} ≠ t_{1} ∨ … ∨ s_{n} ≠ t_{n} \end{aligned}

Clashes (C)

\begin{aligned}(C_{1}) & f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m}) & → & ⊥ & If f ≠ g \\ (C_{2}) & f(s_{1}, …, s_{n}) ≠ g(t_{1}, …, t_{m}) & → & ⊤ & If f ≠ g \end{aligned}

Trivial equations and disequations (T)

\begin{aligned}(T_{1}) & s = s & → & ⊤ \\ (T_{2}) & s ≠ s & → & ⊥ \end{aligned}

Occur-Check (O)

\begin{aligned}(O_{1}) & x = s[x]_{p} & → & ⊥ & If p ≠ Λ \\ (O_{2}) & x ≠ s[x]_{p} & → & ⊤ & If p ≠ Λ \end{aligned}

Merge (M)

\begin{aligned}(M_{1}) & z = t ∧ z = u & → & z = t ∧ t = u \\ (M_{2}) & z ≠ t ∨ z ≠ u & → & z ≠ t ∨ t ≠ u \\ (M_{3}) & z = t ∧ (z ≠ u ∨ d) & → & z = t ∧ (t ≠ u ∨ d) \end{aligned}

d is a (possibly empty) disjunction, z is a variable, t is not a variable and |t| ≤ |u|.

Figure 3: Classical rules on quantifier-free equational formulae Lemma 2 If ϕ →_{R} ψ, then [[ϕ]] = [[ψ]].

Lemma 3 If ϕ →_{R−{Ex}} ψ and if ϕ is w.e.d. then ψ is w.e.d.

Lemma 4 If ϕ →_{Ex} ⋁_{f∈F} ϕ_{f}, then ϕ is E_{U} iff each ϕ_{f} is E_{U}. If ϕ is w.e.d. then so are all ϕ_{f}.

Theorem 1 R terminates on w.e.d. formulae.

The termination proof is not easy. An account of it is given in [1].

2.4 Irreducible Formulae

Now, we inspect the irreducible (w.r.t. R) formulae, showing some properties which will be useful in the next section.

A simple formula is either ⊤, ⊥ or of the form ∃w⃗ : x_{1} = t_{1}∧…∧x_{n} = t_{n}∧d_{1}∧…∧d_{m} where

1. x_{1}, …, x_{n} are the free variables of the formula. They occur only once in the formula

2. Var(d_{1}, …, d_{m}) ⊆ Var(t_{1}, …, t_{n}) ⊆ w⃗

3. each d_{i} has the form z_{1} ≠ u_{1} ∨ … ∨ z_{k} ≠ u_{k} where each z_{j} is a variable which occurs only once in d_{i} and there is no u_{j} belonging to T (F).

In order to get simple formulae as irreducible forms w.r.t. R we have first to abstract every free variable: if ϕ is irreducible w.r.t. R, let ϕ ↓ be the formula ϕ on which the following rule has been applied as long as possible:

∃w⃗ : ϕ → ∃w⃗, ∃z : x = z ∧ ϕ{x ↦ z}

If x ∉ w⃗ and x ∈ Var(ϕ) is not solved in ϕ

This is only a trick which ensures that every free variable is solved. Then, if ϕ is a w.e.d equational problem, let ϕ↓_{R} be an irreducible form w.r.t. R and the above rule of an equivalent existential formula.

Lemma 5 ϕ ↓_{R} is a finite disjunction of simple formulae. ϕ has the E_{U} property iff each of these simple formulae has the E_{U} property.

3 Completeness of R

We have already shown that any w.e.d. problem is equivalent (with respect to T (F)) to a finite disjunction of simple formulae each of which has the E_{U} property iff the starting formula has the E_{U} property. Now, for R to be complete with respect to the elimination of negation we must show that negation cannot be eliminated from simple formulae which are not unification problems.

In the proof we will use some technical lemmas which state necessary conditions for a formula to have the E_{U} property. These lemmas express some fundamental properties of trees which may be used in other contexts. First of all, lemma 6 states the equivalence between the E_{U} property and the existence of a finite set of generators.

Lemma 6 A first order formula ϕ has the E_{U} property (or, equivalently, negation can be eliminated from ϕ) if and only if there exits a finite complete set of generators for ϕ.

Lemma 7 shows that negation can not be eliminated from the formula u ≠ t if u and t are non-ground terms without common variables such that u is an instance of t, and lemma 8 generalizes this condition to conjunctions of disequations. Lemmas 7 and 8 are consequences of the results in [10]. In lemma 9, the conditions are generalized to formulae of the form d_{1} ∧ … ∧ d_{n} where each d_{i} is a disjunction of disequations. Finally, in lemma 10 and 11 we consider formulae containing also equations. See [1] for more details.

Lemma 7 If t, u are non-ground terms such that u is an instance of t and Var(t) ∩ Var(u) = ∅ then negation can not be eliminated from u ≠ t.

Lemma 8 Let P ≡ u_{1} ≠ t_{1} ∧ … ∧ u_{n} ≠ t_{n} such that for all i, u_{i}, t_{i} are non-ground terms, Var(t_{i}) ∩ Var(u_{i}) = ∅ and u_{i} ≡ t_{i}λ_{i}, with Im(λ_{i}) ∩ T (F) = ∅. Then negation can not be eliminated from P.

Lemma 9 Let P be d_{1}∧…∧d_{m} such that each d_{i} has the form z_{1i} ≠ t_{1i}∨…∨z_{n_{i}i} ≠ t_{n_{i}i} where z_{1i} … z_{n_{i}i} are different variables not occurring again in the terms t_{jk}, and for all i, j: t_{ji} ∉ T (F). Then negation can not be eliminated from P.

Lemma 10 Let P ≡ ∃w⃗ : P be an existential formula. Assume x is a variable not appearing in P and t is a term such that Var(t) ⊆ w⃗. ∃(w⃗ − Var(t)) : P has the E_{U} property if and only if ∃w⃗ : (P ∧ x = t) has the E_{U} property.

As a consequence of lemmas 9 and 10, we have:

Lemma 11 If P is a simple problem which is not a unification problem, then P does not have the E_{U} property.

Now, completeness of R is a consequence of lemma 11, since R-solved forms satisfy the hypothesis of lemma 11.

Theorem 2 (Completeness of R) Let ϕ be a w.e.d. equational problem. Then ϕ has the E_{U} property (i.e. negation can be eliminated from ϕ) iff ϕ↓_{R} is a unification problem.

4 Elimination of negation in permutative equational theories

We call elimination of negation in a theory E the problem of deciding whether a disequation is equivalent w.r.t. ∼_{E} to a unification problem. Previously we assumed that the tree algebra is free. Now we are going to extend the results to some quotient algebras T (F)/_{=_{E}} where =_{E} is a finitely generated congruence. However, we have to assume some further hypotheses since:

Proposition 1 Elimination of negation in equational theories is undecidable in general.

In fact, elimination of negation in a theory E is not even semi-decidable even for theories with decidable validity and unification problems. This result is a consequence of the following lemmas:

Lemma 12 ([6]) Solving disequations in T (F)/_{=_{E}} is semi-decidable even if E-unification and validity are decidable.

Lemma 13 If elimination of negation is semi-decidable in a theory E and E-unification is decidable then there is a decision procedure for solving disequations in T (F)/_{=_{E}}.

However, for a specific class of equational theories the results for elimination of negation in the free case can be generalized: Mal’cev (in [12]) studied some classes of permutative algebras in which, the axiom f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) ⇒ s_{1} = t_{1} ∧…∧s_{n} = t_{n} is replaced by f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) ⇒ ⋁_{ρ∈Π} s_{1} = t_{ρ(1)}∧…∧s_{n} = t_{ρ(n)} where Π is a subgroup of the symmetric group S_{n}. These theories include and generalize commutative theories. Satisfiability of any first order formula is decidable [2], which makes Mal’cev’s theories an interesting alternative for (constraint) logic programming languages. Moreover, permutative theories of Mal’cev are ω-complete (as a consequence of the results in [2]) and unification is finitary. For these theories there is a set of transformation rules R_{p} which is sound and complete for elimination of negation.

The transformation system R_{p} is obtained from R by slight modifications which are listed below:

• First, the decomposition rules are replaced according to the above new axiom scheme

• Then the trivial equations and disequations rules have to be replaced with (e.g. for T_{1}) s = t → ⊤ if s =_{E} t.

Lemma 14 R_{p} terminates and preserves the set of E-solutions when E is a permutative set of equations.

Lemmas 6 to 11 generalize, and we have:

Theorem 3 Let E be a set of permutative axioms. Negation can be eliminated from a w.e.d equational problem ϕ in the theory E iff all its irreducible forms w.r.t. R_{p} are unification problems.

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.

[2] Hubert Comon. Complete axiomatizations of some quotient term algebras. In Proc. ICALP, Madrid, LNCS 510, July 1991.

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

[4] Hubert Comon and Pierre Lescanne. Equational problems and disunification. J. Symbolic Computation, 7:371–425, 1989.

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

[6] Maribel Fernández. Equational disunification. To appear in Applicable Algebra in Engineering, Communications and Computing, 1991.

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

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

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

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

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

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

[13] M. Tajine. Representation explicite de certains langages de termes: théorie et applications. Thèse de l’université Louis Pasteur de Strasbourg, 1992.