AC Complement Problems: Satisfiability and Negation Elimination

Maribel Fernández

LRI, Bât. 490, CNRS / Université de Paris-Sud, 91405 ORSAY Cedex, France. E-mail: maribel@lri.fr

Abstract. We show that negation elimination is decidable for linear complement problems interpreted in T (F)/_{=_{AC}}, where AC is a set of associative and commutative axioms. For this, we present a system of rewrite rules that transforms any linear complement problem into a simple formula, and we give a test for deciding whether a simple formula is satisfiable in T (F)/_{=_{AC}} or not. This test serves as a basis for the development of a negation elimination algorithm.

1 Introduction

Complement problems arise in several domains of Computer Science: in algebraic specifications (the problem of sufficient completeness is nothing but solving a complement problem, and also in the test of ground reducibility complement problems are used [1]), functional programming (e.g. in compilation of pattern matching [12]), logic programming (in particular for the implementation of constructive negation [10]) and constraint programming (to represent solutions of systems of equations and disequations [11]). See [10] for a survey of applications of complement problems.

Actually, as remarked in [1], the computation of term complement is a particular case 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: equality. The complement problem t/t_{1}, …, t_{n}, which represents the set of ground instances of t that are not instances of t_{1}, …, t_{n}, is equivalent to the equational formula ∀y⃗ : t ≠ t_{1} ∧ … ∧ t ≠ t_{n} where y⃗ are the variables appearing in t_{1}, …, t_{n}. An algorithm for deciding whether an equational formula has solutions in the ground term algebra T (F), which solves in particular complement problems, is given in [1]. See also [11] for a decision algorithm for complement problems in T (F).

Complement problems serve, in general, as a means of representing knowledge, but this way of expressing knowledge has an important drawback: it is not explicit. The transformation of a complement problem into an equivalent explicit representation is an interesting problem (see [10]) and it is decidable in T (F): as shown in [11], t/t_{1}, …, t_{n} is equivalent to a finite disjunction of terms iff for 1 ≤ i ≤ n, the most general unifier of t and t_{i} is linear in the variables of t.

However, as pointed out in [9] and in [8], in most applications of complement problems the involved function symbols are not free. There exists, in general, some “background knowledge” that provides information about the properties of the operators, i.e. we have to interpret complement problems in the quotient of T (F) by an equational theory E (denoted by T (F)/_{=_{E}}) and not simply in T (F).

Finding a finite explicit representation for a complement problem is the same as eliminating negation from the corresponding equational formula. In [3] it is shown that when E is a permutative theory of Mal’cev (a class of equational theories that includes and generalizes commutative theories), negation elimination is decidable for complement problems interpreted in T (F)/_{=_{E}}. Particularly important is the case where E is a set of associative and commutative axioms. AC complement problems, that is, complement problems interpreted in T (F)/_{=_{AC}}, have been a subject of active research in the last years (see e.g. [9] and [13], where two different algorithms for solving linear AC complement problems are presented). Here we study negation elimination in AC complement problems.

The necessary and sufficient condition of [11] for negation elimination in T (F) generalizes easily to T (F)/_{=_{E}} when E is a permutative theory of Mal’cev (by taking E-unifiers instead of syntactical unifiers), but in the case of T (F)/_{=_{AC}} this condition is no longer sufficient. For example, if + is AC, a is a constant and f is a free unary function symbol, we can not eliminate negation from ∀y : x ≠ y + a. In this paper we show that negation elimination is decidable for linear complement problems interpreted in T (F)/_{=_{AC}} (a complement problem t/t_{1}, …, t_{n} is linear if t_{1}, …, t_{n} do not contain multiple occurrences of the same variable). For non-linear problems the question is still open.

Our approach is inspired by [1], [3] and [2], where the algorithms for solving complement problems in T (F) are expressed by means of transformation rules. As a first step towards the definition of an algorithm for negation elimination we give a set of transformation rules over equational formulae, which reduces any complement problem to a simple formula. Then, we show how to test whether a simple formula is satisfiable in T (F)/_{=_{AC}} or not, that is, we give an algorithm for solving AC complement problems. Our algorithm is based on “test sets”, as the algorithm presented in [9], but it yields some theoretical and practical improvements: on one hand, the use of transformation rules allows simpler proofs of completeness and termination, on the other hand, the complexity of the procedure is smaller. The algorithm for negation elimination is obtained by stepwise refinement of the decision test.

The paper is organized as follows: section 2 contains a concise description of the syntax and semantics of complement problems; section 3 deals with satisfiability and negation elimination in AC complement problems: transformation rules and decision tests; in section 4 we generalize our algorithms to a wider class of equational formulae.

2 AC Complement Problems

2.1 Syntax

We consider a finite set F of function symbols with fixed arity. T (F) is the infinite set of ground terms over this alphabet. Terms are identified with finite labeled trees as usual. The symbol at position p is denoted t(p), the subterm of t at position p is denoted t|_{p} and the result of replacing t|_{p} with u at position p in t is denoted t[u]_{p}. Variables are an infinite distinguished set X of symbols. The set of terms built on F and X is denoted T (F, X). V ar(t) denotes the set of variables appearing in t. A substitution σ is a mapping from a finite subset of X, called its domain and written dom(σ), into T (F, X). Such a mapping is written {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}. Substitutions are extended to T (F, X) in the usual way. The set of all substitutions is denoted by Σ. By σ|_{V} we denote the restriction of a substitution σ to the set V of variables. Substitutions are used in postfix notation. By Im(σ) we denote the set {xσ | x ∈ dom(σ)}. We say that Im(σ) is linear if for all x ∈ dom(σ) xσ is linear and V ar(x_{i}σ) ∩ V ar(x_{j}σ) = ∅ for all x_{i} ≠ x_{j}. A substitution is idempotent if σσ = σ. A substitution is ground if it assigns ground terms to all the variables in its domain. It is ground for a set V of variables if it assigns ground terms to all variables in V. We refer to [5] for missing definitions and notations.

An equation is an unordered pair of terms, written s = t. A disequation is also an unordered pair of terms, written s ≠ t. 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 are interested in two particular fragments of equational formulae: complement problems and unification problems. A complement problem is either ⊤, ⊥ or a formula ∀y⃗ : t ≠ t_{1} ∧ … ∧ t ≠ t_{n} where V ar(t) = x⃗ is the set of free variables (or unknowns) of the formula and V ar(t_{1})∪…∪V ar(t_{n}) = y⃗. Without loss of generality we can assume that V ar(t_{i}) ∩ V ar(t_{j}) = ∅ for all i ≠ j, then a complement problem is linear if for 1 ≤ i ≤ n, t_{i} does not contain multiple occurrences of the same variable. A unification problem is an existential formula which does not contain any disequation.

2.2 Semantics

Let ϕ be an equational formula and V the set of free variables of ϕ. The set of solutions of ϕ is the set of ground substitutions σ such that V ⊆ dom(σ) and T (F) ⊧ ϕσ. It is denoted by [[ϕ]].

We consider interpretations in quotient algebras T (F)/_{=_{AC}} where =_{AC} is the smallest congruence on T (F, X) such that it is closed by instantiation and contains the set of equations {f(x, y) = f(y, x)/f ∈ F′} ∪ {f(x, f(y, z)) = f(f(x, y), z)/f ∈ F′} for a subset F′ of F containing only binary symbols. The symbols in F′ are called AC function symbols and the theory of =_{AC} is called AC equational theory. An AC-solution of ϕ is a ground substitution σ for the set of free variables of ϕ, such that T (F)/_{=_{AC}} ⊧ ϕσ. The set of AC-solutions of ϕ is denoted [[ϕ]]_{AC}.

In the following the prefix AC will be used to indicate that we are considering the algebra T (F)/_{=_{AC}}. Two equational formulae ϕ and ψ are equivalent (resp. AC-equivalent) if they have the same set of solutions (resp. AC-solutions). This is written ϕ ∼ ψ iff [[ϕ]] = [[ψ]] (resp. ϕ ∼_{AC} ψ iff [[ϕ]]_{AC} = [[ψ]]_{AC}). A generator (resp. AC-generator) of a set of solutions (resp. AC-solutions) of ϕ is a substitution σ whose ground instances are solutions (resp. AC-solutions) of ϕ. A set S of generators is complete (for ϕ) if every solution of ϕ is an instance of some generator σ ∈ S. Complete sets of AC-generators of unification problems will be called complete sets of AC-unifiers^{1}. We say that σ is more general (modulo AC) than μ on V or that μ is an AC-instance of σ on V, written σ ⪯_{AC}^{V} μ, if there exists a substitution ρ such that (σρ) |_{V} =_{AC} μ |_{V} (the definition of =_{AC} extends to substitutions as usual). A complete set of most general AC-unifiers of a unification problem ϕ (abbreviated CSU_{AC}(ϕ)) is a minimal complete set of AC-unifiers of ϕ, that is, for all σ, μ ∈ CSU_{AC}(ϕ), σ ⪯_{AC}^{V ar(ϕ)} μ implies σ ≡ μ. Any unification problem has a finite set of idempotent most general AC-unifiers, i.e. AC-unification is decidable and finitary.

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

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

– f(x, y) ≠ g(z) which is equivalent to ⊤

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

– ∀y : x ≠ y ∨ x ≠ f(y) which is equivalent to ∀y : x ≠ f(x). This formula is in turn equivalent to x ≠ f(x) which is equivalent to ⊤

– ∀y : x ≠ y + a which is equivalent to (∃w_{1}, w_{2}, ∀y : x = w_{1} + w_{2} ∧ w_{1} + w_{2} ≠ y + a) ∨ x = a if F = {a, +}, and this is equivalent to x = a if + is AC.

We are interested in two semantic properties of AC-complement problems: Satisfiability, that is, the existence of at least one solution of the problem in the algebra T (F)/_{=_{AC}}, and AC-E_{U} (AC-equivalence to unification problems), that is, the existence of a unification problem with the same set of solutions in T (F)/_{=_{AC}}. Given a complement problem P ≡ ∀y⃗ : t ≠ t_{1} ∧ … ∧ t ≠ t_{n}, if there is a unification problem (a positive formula) ϕ such that P ∼_{AC} ϕ we say that negation can be eliminated from P.

3 Satisfiability and Negation Elimination

In order to decide if a complement problem is satisfiable in T (F)/_{=_{AC}}, or, in general, if a complement problem has the AC-E_{U} property, first we use a set

1 AC-unifiers are usually defined as solutions of unification problems in T (F, X)/_{=_{AC}}. Of course, our AC-unifiers are also AC-unifiers according to this definition.

R_{EAC} of rules which transforms any complement problem into an equivalent finite set of simplified formulae, which will be called simple, and then we apply a decision test over simple formulae.

Although negation elimination is more general than satisfiability (in that the answer to the latter problem can be deduced from the answer to the former) we present first a decision test for satisfiability alone, because it illustrates the method and facilitates the presentation and proofs concerning elimination of negation. By refining this test we obtain a test for AC-E_{U}.

Hereafter we assume that the complement problems we want to decide are linear. However R_{EAC} can also be applied to non-linear problems. The hypothesis of linearity is needed only for the tests.

A simple formula is either ⊤, ⊥ or ∃w⃗, ∀y⃗ : ( ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}))∧x_{1} = v_{1}∧

… ∧ x_{n} = v_{n} where

1. K, L_{k} are finite sets of indexes,

2. w_{kl} are existentially quantified variables, V ar(v_{1}) ∪ … ∪ V ar(v_{n}) = w⃗, and x_{1}, …, x_{n} are unknowns,

3. for all k, l, V ar(u_{kl}) ⊆ y⃗; and there exist k ∈ K, l ∈ L_{k} such that u_{kl} is not ground,

4. each variable appears at most once in a disjunction.

An intermediate formula is either ⊤, ⊥ or ∃w⃗, ∀y⃗ : ( ⋀_{k∈K}( ⋁_{l∈L_{k}}t_{kl} ≠ u_{kl})) ∧

x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n} where

1. K, L_{k} are finite sets of indexes,

2. for all k, l, V ar(t_{kl}) ∩ y⃗ = ∅; x_{1}, …, x_{n} are unknowns and V ar(v_{1}) ∪ … ∪ V ar(v_{n}) = w⃗,

3. for all k, l, V ar(u_{kl}) ⊆ y⃗,

4. each variable in y⃗ appears at most once in a disjunction.

Note that a linear complement problem ∀y⃗ : t ≠ t_{1} ∧ … ∧ t ≠ t_{n} with unknowns x_{1}, …, x_{m} is equivalent to the intermediate formula ∃w⃗, ∀y⃗ : (t ≠ t_{1}∧ … ∧ t ≠ t_{n}){x_{1} ↦ w_{1}, …, x_{m} ↦ w_{m}} ∧ x_{1} = w_{1} ∧ … ∧ x_{m} = w_{m}. In the following both kinds of formulas will be called complement problems. It will be clear from the context (when not explicitly written) which is the representation we are considering.

3.1 Transformation Rules

Every intermediate formula (and then every complement problem) which is not a simple formula can be reduced using the set R_{EAC} of transformation rules (see figure 1). It contains some classical rules for eliminating universally quantified variables and reorganizing formulae (see e.g. [4] for more details) and some additional rules which are specific for complement problems modulo AC, such as the explosion and decomposition rules. The empty disjunction is denoted by ⊥ and the empty conjunction by ⊤.

Universal Quantifier Elimination (QE)

(QE_{1}) ∀y : P → P
If y ∉ V ar(P).

(QE_{2}) ∀y⃗ : P ∧ (y ≠ t ∨ d) → ∀y⃗ : P ∧ d{y ↦ t}

If d is a disjunction of disequations, y ∈ y⃗ and y ∉ V ar(t).

Reorganization (RO)

(RO_{1}) P ∧ ⊥ → ⊥ (RO_{2}) P ∧ ⊤ → P
(RO_{3}) P ∨ ⊤ → ⊤ (RO_{4}) P ∨ ⊥ → P

Decomposition (D)

(D_{1}) ∃w⃗, ∀y⃗ : P ∧ (t ≠ u ∨ d) → ∃w⃗, ∀y⃗ : P ∧ d
If t, u ∉ X and there exists θ ∈ CSU_{AC}(t = u ∧ ¬d) such that θ does not

instantiate existentially quantified variables.

(D_{2}) ∃w⃗∀y⃗ : P ∧ (t ≠ u ∨ d) → ∃w⃗∀y⃗∀z⃗ : P ∧  ⋀_{θ∈CSU_{AC} (t=u∧¬d)}( ⋁_{w_{j} ∈dom(θ)} w_{j} ≠ w_{j}θ)

If t, u ∉ X and D_{1} does not apply. z⃗ are the variables introduced by θ_{1}, …, θ_{n}.

Explosion (E)

(Ex_{∀}) ∃w⃗, ∃w^{(i)}, ∀y⃗ : P → ⋁_{f∈F}∃w⃗, ∃ \overrightarrow{w^{′(i+1)}}, ∀y⃗ : P \{w^{(i)} ↦ f(\overrightarrow{w^{′(i+1)}})\}

If the formula is not simple, there is a disequation w^{(i)} ≠ u in P such that

V ar(u) ∩ y⃗ ≠ ∅, u ∉ X and i ≤ K; no other rule can be applied and \overrightarrow{w^{′(i+1)}} are fresh variables (different for each function symbol).

(Ex_{gr}) ∃w⃗, ∃w^{(i)}, ∀y⃗ : P → ⋁_{f∈F}∃w⃗, ∃ \overrightarrow{w^{′(i+1)}}, ∀y⃗ : P \{w^{(i)} ↦ f(\overrightarrow{w^{′(i+1)}})\}

If the formula is not simple, there is a disequation w^{(i)} ≠ u in P such that u is a

ground term, no other rule except Ex_{∀} can be applied, \overrightarrow{w^{′(i+1)}} are fresh variables (different for each function symbol), and if i = K there is no disequation w^{(i)} ≠ v

where w^{(i)} is a variable, v is not a variable and V ar(v) ∩ y⃗ ≠ ∅.

Fig. 1. Transformation rules for AC complement problems.

There are two decomposition rules:

- D_{1} is based on the fact that if t = u has an AC-unifier σ which does not instantiate the variables in t then there is no solution for the complement problem ∀y⃗ : t ≠ u where V ar(u) = y⃗, because for all ground substitution ρ for the variables of t, σρ unifies tρ and u).

- D_{2} decomposes a disequation t ≠ u according to the set of AC-unifiers of t = u. Unlike for complement problems in T (F), in T (F)/_{=_{AC}} new universally quantified variables may be introduced. To avoid non-termination problems caused by successive applications of explosion and decomposition rules, we add a label 0 to each existentially quantified variable in the starting problem, and we require that the existentially quantified variables introduced in the application of an explosion rule to a variable x^{(i)} have a label i + 1. Moreover, we do not allow the application of an explosion rule to a variable labeled by i if i > K for a given K. K can be arbitrarily chosen since it is used only to ensure the termination of the process. If the starting problem is ∀y⃗ : t ≠ t_{1} ∧ … ∧ t ≠ t_{n} we will choose K = max_{i}{depth(t_{i})}, where depth(t_{i}) is the depth of the tree corresponding to the term t_{i}. Please note that D_{2} applies also when the set of AC-unifiers is empty, and in this case its effect is the elimination of the disjunction containing t ≠ u.

There are two explosion rules in R_{EAC}. Ex_{∀} generalizes the explosion rule of [2]. Besides, now 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. For example, assuming F = {0, s}, the formula x ≠ 0 is equivalent to ∃w : x = s(w). This is expressed by the rule Ex_{gr}. Since complement problems are represented by intermediate formulas where the free variables appear only in equations, we do not need to consider explosions on free variables.

Property 1 (Correctness, termination, irreducible formulae) Let ϕ be a linear complement problem.

1. If ϕ →_{R_{EAC}}^{∗} ψ then [[ϕ]]_{AC} = [[ψ]]_{AC}, i.e. R_{EAC} preserves solutions.

2. There is no infinite sequence ϕ →_{R_{EAC}} ϕ_{1} →_{R_{EAC}} … ϕ_{n} →_{R_{EAC}} . . ..

3. Any irreducible form of ϕ is a finite disjunction of simple formulae.

As a consequence of property 1:

Theorem 1. R_{EAC} transforms any linear complement problem into an equivalent finite disjunction of simple formulae.

3.2 Solving simple formulae

By theorem 1, satisfiability of linear AC complement problems reduces to satisfiability of simple formulae. Let us consider a (non-trivial) simple formula

ϕ ≡ ∃w⃗, ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n}

Then ϕ is satisfiable if and only if ψ ≡ ∃w⃗, ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) is. The

decision test we are going to show is inspired by [9]. We will prove that in order to decide satisfiability of ψ it is sufficient to consider a finite set of substitutions instead of the set of all ground substitutions with domain w⃗.

Terms involving AC function symbols will be represented in flattened form [7]: flat(t), for a term t, is the normal form of (the tree) t for the convergent tree rewriting system

f(x_{1}, …, x_{p−1}, f(y_{1}, …, y_{q}), x_{p+1}, …, x_{n}) → f(x_{1}, …, x_{p−1}, y_{1}, …, y_{q}, x_{p+1}, …, x_{n})

for any integers p, q and n such that 1 ≤ p ≤ n, and for any AC operator f. In other words, AC-symbols are treated as varyadic symbols in flattened forms.

The notion of flattening extends to substitutions in the natural way: flat(σ) assigns flat(xσ) to each variable x ∈ dom(σ).

Let d = max_{k,l}{depth(flat(u_{kl}))} + 1, and let k be the maximal number of arguments of an AC symbol in flat(u_{kl}) for u_{kl} in ψ. We can now define the finite sets A(ψ) = {flat(r) | r ∈ T (F, X), r is linear, depth(flat(r)) ≤ d, AC-symbols have at most k + 1 arguments, and variables can occur only at depth d}. S_{w⃗,y⃗,A(ψ)} = {σ ∈ Σ | dom(σ) = w⃗, Im(σ) ⊆ A(ψ) and Im(σ) is linear, and V ar(Im(σ)) ∩ y⃗ = ∅}.

Lemma 2 below shows that for deciding satisfiability of ψ it is sufficient to consider only the substitutions in S_{w⃗,y⃗,A(ψ)}.

Lemma 2. Let ϕ and ψ be as above. T (F)/_{=_{AC}} ⊧ ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl} = u_{kl}) iff

for all λ ∈ S_{w⃗,y⃗,A(ψ)}, T (F)/_{=_{AC}} ⊧ ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl}).^{2}

Let us call C the condition of lemma 2: “for all λ ∈ S_{w⃗,y⃗,A(ψ)}, T (F)/_{=_{AC}} ⊧ ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl})”. From lemma 2 we deduce that ¬C, i.e. ∃λ ∈ S_{w⃗,y⃗,A(ψ)}

such that T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl}), is a necessary and sufficient

condition for satisfiability of ϕ:

Theorem 3. Let ϕ be as above. ϕ has solutions in T (F)/_{=_{AC}} iff ∃λ ∈ S_{w⃗,y⃗,A(ψ)}

such that T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl}).

Theorem 3 suggests an algorithm for solving simple formulae: it is sufficient

to test for each λ ∈ S_{w⃗,y⃗,A(ψ)} whether T (F)/_{=_{AC}} ⊧ ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl}) or,

equivalently (since all the variables in w_{kl}λ are deeper than those in u_{kl} and the

2 Linearity is fundamental here. Without linearity we have only a sufficient (but not necessary) condition.

terms u_{kl} are linear), whether there is σ such that ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ =_{AC} u_{kl}σ).

A substitution σ satisfying this condition is usually called an AC-matcher. So, Theorem 3 can be reformulated in other words: a simple formula ϕ is satisfiable iff there exists λ ∈ S_{w⃗,y⃗,A(ψ)} such that the AC-matching problem ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ =_{AC} u_{kl}) has no solution. AC-matching is a well-known decidable

problem [6].

In fact, this decision test can be applied to the irreducible forms of R_{AC} = R_{EAC} −{Ex_{gr}}, since Ex_{gr} is only needed to eliminate negation. R_{AC} is correct and terminating. Its irreducible forms differ from those of R_{EAC} in that now all the terms u_{kl} can be ground, i.e. condition 3 in the definition of simple formulae is no longer valid. Now, if for all k, l, u_{kl} is ground, ϕ has solutions since for all terms u, t such that ¬(u =_{AC} t) there is a solution of u ≠ t in T (F)/_{=_{AC}}. Otherwise we apply the test.

This decision test can be written as a set T of transformation rules to be added to R_{AC}, see figure 2.

Test (T)

(T_{0}) P ≡ ∃w⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n} → ⊤

If P is irreducible by R_{AC} and all u_{kl} are ground terms.

(T_{1}) P ≡ ∃w⃗, ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n} → ⊥

If P is irreducible by R_{AC}, there exists k, l such that u_{kl} is not ground, and condition C holds.

(T_{2}) P ≡ ∃w⃗, ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n} → ⊤

If P is irreducible by R_{AC}, there exists k, l such that u_{kl} is not ground, and ¬C.

Fig. 2. Decision test for satisfiability of simple formulae

A careful analysis of the algorithm issued from R_{AC} ∪ T shows that the complexity of the transformation process is given by the complexity of AC-unification (which is known to be doubly exponential in general, but is only exponential in the linear case), and that the complexity of T is O(n^{a^{d}}), where n is the number of function symbols in the signature and a = max{max_{f∈F}{arity(f)}, k}. It is then clear that only by decreasing the values of d and k one can improve significantly the efficiency of the algorithm.

In this sense, our method improves from [9]: the bounds d and k we use for constructing the test set are smaller than those used in [9], since we do not consider the original problem but the smaller problems obtained after application of R_{AC}^{3}.

3.3 Negation Elimination in Simple Formulae

Negation elimination in AC complement problems reduces to negation elimination in finite disjunctions of simple formulae (by theorem 1). Moreover, as a consequence of the following lemma, each disjunct can be treated separatedly, which simplifies even more the problem.

Lemma 4. Let P be a linear AC-complement problem and ⋁_{j∈J}P_{j} be an

irreducible form by R_{EAC} of P. Then, P has the AC-E_{U} property if and only if every P_{j} has the AC-E_{U} property.

Proof. The “if” part is trivial. Let us prove the “only if”: Correctness of R_{EAC} implies [[P]]_{AC} = [[ ⋁_{j∈J}P_{j}]]_{AC}, which implies that P has the AC-E_{U} property if

and only if ⋁_{j∈J}P_{j} does. Now, the only rules that introduce a disjunction are

the explosions, but if P →E ⋁_{f∈F}P_{f} then P is AC-E_{U} if and only if each P_{f} is

(because explosion consists essentially in adding an equation). The thesis follows by a simple induction on the number of applications of E. □

Now we are faced to the problem of negation elimination in one simple formula. Let us consider a non-trivial simple formula ϕ ≡ ∃w⃗, ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠

u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n}. The formula ψ ≡ ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) will

be called the kernel of ϕ. Remark that now there are no existentially quantified variables in ψ. The following is a very important property:

Lemma 5. ϕ has the AC-E_{U} property if and only if ψ does.

So, the first step towards obtaining a positive formula equivalent to ϕ is eliminating negation from ψ. If ∃w⃗ : ψ →T⊥ then ϕ ∼_{AC}⊥ and we are finished. But if ∃w⃗ : ψ →T ⊤, i.e. if ϕ has solutions, then it must be rule T_{2} which applies (not T_{0} because at least one of the u_{kl} is not ground). Then, since the condition of rule T_{2} holds, there exists L = {λ_{1}, …, λ_{h}} ⊆ S_{w⃗,y⃗,A(ψ)} such that

for 1 ≤ i ≤ h, T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ_{i} = u_{kl}). We will use L to

eliminate negation from ψ.

3 For linear complement problems the transformation process can not increase the values of k and d.

Before presenting the formal description of the negation elimination algorithm, let us illustrate the ideas behind it with an example.

Example 2. Let F = {+, a, b, c, d, e} where + is AC and the other symbols are constants, and let us consider a formula having the AC-E_{U} property:

ψ ≡ ∀y : w ≠ a+a+y∧w ≠ b+b+y∧w ≠ c+c+y∧w ≠ d+d+y∧w ≠ e+e+y

In this example d = 2 and k + 1 = 4.

A(ψ) = { a, b, c, d, e, a + a, a + b, a + c, a + d, a + e, b + b, b + c, b + d, b + e, …

a + a + a, a + a + b, a + a + c, a + a + d, a + a + e, a + b + b, …
a + a + a + a, a + a + a + b, …}

S_{w,y,A(ψ)} is the set of all the substitutions with domain {w} and image in A(ψ).

L = {{w ↦ P } | P ∈ {a, b, c, d, e}} ∪ {{w ↦ P + Q} | P, Q ∈ {a, b, c, d, e}} ∪ {{w ↦ P + Q + R} | P, Q, R ∈ {a, b, c, d, e}, and P, Q, R are pairwise distinct constants}∪ {{w ↦ P + Q + R + S} | P, Q, R, S ∈ {a, b, c, d, e}, and P, Q, R, S are pairwise distinct constants}

Since L ≠ ∅, ψ has solutions in T (F)/_{=_{AC}}. We are faced now to the problem of deciding whether ψ has the AC-E_{U} property or not, and in case it has, finding a finite complete set of generators for ψ. L will serve to this purpose. Of course, L is not a complete set of generators of ψ in general. It is clear in this example that the substitutions in L can not generate a solution with more than 4 arguments, as, for instance {w ↦ a + b + c + d + e} (which is a solution of ψ).

At first glance one could think that to overcome this incompleteness problem it is sufficient to add new variables as arguments in all the AC symbols with k + 1 arguments (k + 1 is the bound used in the construction of S_{w⃗,y⃗,A(ψ)}). We obtain in this way a set L^{∗} which is certainly complete, but nothing guarantees that the substitutions in L^{∗} will generate only solutions of ψ. In case they are generators the problem is solved, but in the other case we have to consider a bigger test set (with k′ > k): if in example 2 we take k′ = 4 and we repeat the construction above, we obtain a set L′ of substitutions which is a complete set of generators of ψ.

Formally, let ψ ≡ ∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) be the kernel of a simple formula

ϕ, and assume there exists L = {λ_{1}, …, λ_{h}} such that L ⊆ S_{w⃗,y⃗,A(ψ)} and for

1 ≤ i ≤ h, T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ_{i} = u_{kl}). Since the variables in

Im(λ_{i}) are strictly deeper than those in u_{kl} and each variable in u_{kl} appears at most once in a conjunction, for 1 ≤ i ≤ h:

(1) T (F)/_{=_{AC}} |̸= ∃V ar(Im(λ_{i})), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ_{i} = u_{kl})

Let us add a different sub-index to each occurrence of an AC function symbol with k + 1 arguments in Im(λ_{1}), …, Im(λ_{h}). If +_{i_{1}}, …, +_{i_{m}} occur in Im(λ_{i}), we define λ_{i}^{I}, I ⊆ {i_{1}, …, i_{m}}, such that it is the same as λ_{i} but for the subterms whose root is +_{i_{j}} with i_{j} ∈ I, where there is one more argument: a new variable x_{i_{j}}. L^{∗} is the set {λ_{i}^{I} | λ_{i} ∈ L, I ⊆ {i_{1}, …, i_{m}}}.

If there is no λ_{i}^{I} ∈ L^{∗} such that

(2) T (F)/_{=_{AC}} ⊧ ∃V ar(Im(λ_{i}^{I})), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ_{i}^{I} = u_{kl})

then L∪L^{∗} is a complete set of generators for ψ (we will prove below, in theorem 8, its correctness and completeness). Otherwise, we will prove, also in theorem 8 below, that there exists k′ > k such that if we define A′(ψ), S_{w⃗,y⃗,A′(ψ)}, L′ and L^{′∗} in the same way as A(ψ), S_{w⃗,y⃗,A(ψ)}, L and L^{∗} but using k′ instead of k, then

- ψ has the AC-E_{U} property iff there is no λ′_{i}^{I} ∈ L^{′∗} such that (2) holds,

- if ψ has the AC-E_{U} property then L′ ∪ L^{′∗} is a complete set of generators for ψ.

Let us show now how this k′ will be computed. First of all we have to define the notion of “correspondence” between arguments of AC symbols. More precisely, let + be an AC symbol and t, u be flattened terms t ≡ +(t_{1}, …, t_{n}) and u ≡ +(u_{1}, …, u_{m}), n ≥ m. An AC-correspondence ς : [1..n] → [1..m] between t and u is a partial function such that

- for all i ∈ dom(ς), t_{i} and u_{ς(i)} are AC-unifiable and

- ς is maximal, i.e., there is no ς′ : [1..n] → [1..m] such that t_{i} and u_{ς′(i)} are AC-unifiable and cardinal(dom(ς′)) > cardinal(dom(ς)).

Property 2 Given t, u, there exists n such that for all AC-correspondences ς between t and u, cardinal(dom(ς)) = n.

Intuitively, we want k′ such that if a substitution λ′ ∈ L′ has an AC-symbol +_{ij} with k′ + 1 arguments then one of these arguments does not correspond with any of the arguments of +_{ij} in u_{kl}, and as a consequence it can be added an arbitrary number of times in Im(λ′) and the resulting substitutions are still generators of ψ. (In the example 2, if λ′ = {w ↦ a+b+c+d+e} then no argument can be repeated, but let F = {a, f, +} where + is AC, f is a unary function symbol and a is a constant, and let us consider the formula ψ ≡ ∀y : w ≠ y+a+a which does not have the AC-E_{U} property. The substitution {w ↦ f(a)} is a solution of ψ and also {w ↦ f(a) + f(a)}, {w ↦ f(a) + f(a) + f(a)} … are solutions of ψ: f(a) can be added an arbitrary number of times.) We will show that in this case the only finite representation of these solutions of ψ is λ^{′∗}, which has a variable as an argument of +_{ij}. Let us develop this idea.

We know that (2) is equivalent to

∃V ar(Im(λ_{i}^{I})), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}flat(w_{kl}λ_{i}^{I}) =_{P} flat(u_{kl}))

and (1) is equivalent to

¬(∃V ar(Im(λ_{i})), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}flat(w_{kl}λ_{i}) =_{P} flat(u_{kl})))

If we have an equality with λ_{i}^{I} but not with λ_{i} it is because some arguments of u_{kl} which do not have a correspondent in w_{kl}λ_{i} are covered by a variable in λ_{i}^{I}. That is, there exists k ∈ K such that for all l ∈ L_{k} there are permutations \overline{flat(w_{kl}λ_{i})}, \overline{flat(u_{kl})} of flat(w_{kl}λ_{i}), flat(u_{kl}) respectively, such that all non variable positions of \overline{flat(w_{kl}λ_{i})} coincide with those of \overline{flat(u_{kl})} but there are some remaining arguments under some AC symbols +_{i_{j}} (i_{j} ∈ I) without a correspondent. The number n_{ij} of such arguments is computed as follows: if +_{i_{j}} is an AC symbol with k + 1 arguments that occurs at position q in \overline{flat(wλ_{i})} and \overline{flat(u_{kl})} (for all k, l such that w_{kl} ≡ w), that is, \overline{flat(wλ_{i})} |_{q}≡ +_{i_{j}}(t_{1} …, t_{k+1}) and \overline{flat(u_{kl})} |_{q}≡ +_{i_{j}}(s_{1}, …, s_{r_{kl}}), and for any AC-correspondence ς between \overline{flat(u_{kl})} |_{q} and \overline{flat(w_{kl}λ_{i})} |_{q},

cardinal(dom(ς)) = c_{kl}, then n_{ij} = ∑_{k,l s.t. w_{kl}≡w}r_{kl} − c_{kl}.

Let N_{ij} = n_{ij} − cardinal({w_{kl} | w_{kl} ≡ w}) + 1 and let N = max_{i,j}{N_{ij}}. We take k′ = k + N.

Example 3. Let us calculate k′ for the problem in the previous example. We have to consider the set of substitutions {{w ↦ P + Q + R + S} | P, Q, R, S ∈ {a, b, c, d, e} and P, Q, R, S are pairwise distinct constants} = { λ_{1} : {w ↦ a + b+c+d}, λ_{2} : {w ↦ a+b+c+e}, λ_{3} : {w ↦ a+c+d+e}, λ_{4} : {w ↦ a+b+d+e}, λ_{5} : {w ↦ b+c+d+e}}. Each one of these substitutions has one AC symbol with k + 1 arguments (recall that in this example, w_{k} ≡ w and r_{k} = 3 for all k). Now, for λ_{1}, c_{1} = c_{2} = c_{3} = c_{4} = 2 and c_{5} = 1 then n_{11} = 6 and N_{11} = 6 − 5 + 1 = 2. For λ_{2}, c_{1} = c_{2} = c_{3} = c_{5} = 2 and c_{4} = 1 then n_{21} = 6 and N_{21} = 2. In the same way, N_{31} = N_{41} = N_{51} = 2. Then N = 2 and k′ = 5.

Let L′ be the set of substitutions computed for ψ by using k′ instead of k. By definition, L′ = {λ′_{1}, …, λ′_{h′}} ⊆ S_{w⃗,y⃗,A′(ψ)} such that for 1 ≤ i ≤ h′,

(3) T (F)/_{=_{AC}} |̸= ∃V ar(Im(λ′_{i})), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ′_{i} = u_{kl})

Still we have to prove that L′ ∪ L^{′∗} is a complete set of generators for ψ when such a set exists. The following properties of L′ will be used in the proof.

Lemma 6. If λ′ ∈ L′ then proj_{k+1}(λ′) ∈ L.

Lemma 7. If there is λ′ ∈ L′ such that an AC symbol occurs in Im(λ′) with k′ + 1 arguments then there is a solution of ψ with k′ + 1 + i arguments for any i > 0.

Let us define by cases the set G of substitutions:

– G = L ∪ L^{∗} if there is no λ ∈ L^{∗} such that (2) holds.

– Otherwise, G = L′ ∪ L^{′∗} if there is no λ′ ∈ L^{′∗} such that (2) holds.

– Otherwise, G = ∅.

For instance, for the problem in example 2 G = L′ ∪ L^{′∗}. Now we are ready to prove the main result of this section.

Theorem 8. ψ has the AC-E_{U} property if and only if G ≠ ∅.

If G = {λ_{1}, …, λ_{n}} ≠ ∅ and ⋃_{i}V ar(Im(λ_{i})) = z⃗ then

ψ ∼_{AC} ⋁_{λ_{i}∈G}∃z⃗ : ⋀_{w_{j}∈dom(λ_{i})}w_{j} = w_{j}λ_{i}.

Proof. First we will prove that if G ≠ ∅ then ψ has the AC-E_{U} property, and more precisely, ψ ∼_{AC} ⋁_{λ_{i}∈G}∃z⃗ : ⋀_{w_{j}∈dom(λ_{i})}w_{j} = w_{j}λ_{i}, i.e. G is a complete set of

AC-generators of ψ when G ≠ ∅.

Correctness: We must show that for all λ ∈ G and for all μ such that λμ is a ground substitution, T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λμ = u_{kl}). By contradiction:

If

(∗) T (F)/_{=_{AC}} ⊧ ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λμ = u_{kl})

then, T (F)/_{=_{AC}} ⊧ ∃V ar(Im(λ)), ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ = u_{kl}), then, by (1) and

(3), λ ∉ L and λ ∉ L′. Thus, λ ∈ L^{∗}, but (∗) implies that (2) holds, which contradicts the fact that G ≠ ∅.

Completeness: We must show that for any AC solution μ of ψ there exists λ ∈ G such that μ is an AC-instance of λ. Let μ be a solution of ψ: T (F)/_{=_{AC}} |̸=

∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}μ = u_{kl}). Let us define μ′ ≡ proj_{k+1}(μ) in case G = L ∪ L^{∗},

and μ′ ≡ proj_{k′+1}(μ) in case G = L′ ∪ L^{′∗}.

1. If μ′ ≡ μ then there exists λ ∈ L or λ ∈ L′ such that λ ⪯_{AC} μ, because if max{depth(t) | t ∈ Im(μ′)} ≤ d then μ ∈ L or μ ∈ L′, and if max{depth(t) | t ∈ Im(μ′)} > d then, by definition of S_{w⃗,y⃗,A(ψ)}, S_{w⃗,y⃗,A′(ψ)}, there exists λ ∈ S_{w⃗,y⃗,A(ψ)} or λ ∈ S_{w⃗,y⃗,A′(ψ)} which coincides with μ till depth d−1 and has variables at depth d (i.e., λ ⪯_{AC} μ), and T (F)/_{=_{AC}} |̸= ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ =

u_{kl}) (i.e., λ ∈ G) because if there exists θ such that ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ =_{AC} u_{kl}θ),

then, since μ = λα, ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}μ = u_{kl}θα).

2. If μ ≢ μ′, as a consequence of lemma 6, μ′ is also a solution, then, using 1, there exists λ ∈ L if G = L ∪ L^{∗} or λ ∈ L′ if G = L′ ∪ L^{′∗}, such that λ ⪯_{AC} μ′. Then, there is λ^{∗} ∈ L^{∗} or λ^{∗} ∈ L^{′∗} such that λ^{∗} ⪯_{AC} μ.

Now it remains to prove that if G = ∅ then ψ does not have the AC-E_{U} property. Assume G = ∅ and ψ has the AC-E_{U} property. We will prove that this leads to a contradiction. Since ψ has the AC-E_{U} property and AC-unification is finitary, there exists a complete set Γ = {γ_{1}, …, γ_{n}} of generators of ψ. Since G = ∅, there is λ^{I} ∈ L^{∗} and λ^{′I′} ∈ L^{′∗} such that (2) holds. This implies that there exists μ′ ground, with dom(μ′) = V ar(Im(λ^{′I′})), such that

(4) ∃y⃗ : ⋁_{k∈K}( ⋀_{l∈L_{k}}w_{kl}λ^{′I′}μ′ =_{AC} u_{kl})

But if λ^{′I′} ∈ L^{′∗} then λ′ ∈ L′, that is, all the instances of λ′ are solutions of ψ, in particular λ′μ′. Besides, if λ^{′I′} ∈ L^{′∗}, Im(λ′) has an occurrence of an AC symbol with k′ + 1 arguments and by lemma 7, there is an argument of an AC symbol +_{j} that we can add n times for any n > 0 yielding always a solution, which we denote by (λ′μ′)^{n}.

Since Γ is finite, there exists γ_{i} such that infinitely many (λ′μ′)^{n} are AC instances of γ_{i}, that is, there are infinitely many ρ_{n} such that γ_{i}ρ_{n} =_{AC} (λ′μ′)^{n}.

If +_{j} occurs in w_{kl}λ′, w_{kl}γ_{i}ρ_{n} =_{AC} w_{kl}(λ′μ′)^{n} for infinitely many n.

We assume that all these substitutions are flattened, then flat(w_{kl}γ_{i}ρ_{n}) =_{P} flat(w_{kl}(λ′μ′)^{n}) for infinitely many n. Then, they can be made identical by permutations: \overline{flat(w_{kl}γ_{i}ρ_{n})} ≡ \overline{flat(w_{kl}(λ′μ′)^{n})}.

Assume +_{j} occurs at position p in \overline{flat(w_{kl}(λ′μ′)^{n})}. Then either ∃q ≤ p such that \overline{w_{kl}γ_{i}} |_{q}≡ x ∈ X or \overline{w_{kl}γ_{i}}(p) = +_{j} and ∃q such that |q |= 1 and \overline{w_{kl}γ_{i}}(p.q) = x ∈ X, and x occurs only once in Im(γ_{i}) since we are adding arguments only to the +_{j} occurring at position p. Then, in both cases γ_{i} ⪯_{AC} λ^{′I′}μ′. But λ^{′I′}μ′ is not a solution of ψ by (4). This contradicts the fact that Γ is a set of generators of ψ. □

As a consequence of theorem 8 negation elimination is decidable in linear AC complement problems. We can write the test stated in theorem 8 as a transformation rule to be added to R_{EAC}, see figure 3. The system R_{EAC} ∪ {T} is obviously terminating. When applied to a linear AC complement problem P, it yields a positive formula equivalent to P whenever such a formula exists, and a finite disjunction of simple formulae equivalent to P in case P does not have the AC-E_{U} property.

4 Generalization

The most interesting generalization of the previous results, the non-linear case, is still open. But our decision algorithms for satisfiability and negation elimination in linear AC complement problems generalize easily to a wider class of formulae in Σ_{2}: the ∀-linear formulae. These are formulae ∃w⃗, ∀y⃗ : t_{1} ≠ t′_{1} ∧ … ∧ t_{n} ≠ t′_{n} where t′_{1}, …, t′_{n} do not contain existentially quantified variables and each universally quantified variable occurs only once. R_{EAC} is correct and terminating for ∀-linear formulae. Moreover, the irreducible forms are again simple formulae. Then validity and negation elimination are decidable for ∀-linear formulae in T (F)/_{=_{AC}}.

This is another advantage of an approach based on transformation rules: the decomposition of the problem into simplification rules and decision test over

Test (T)

\begin{aligned}(T) & P ≡ (∃w⃗∀y⃗ : ⋀_{k∈K}( ⋁_{l∈L_{k}}w_{kl} ≠ u_{kl}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n}) ∨ d & → \\ & (∃w⃗ : ( ⋁_{λ_{i}∈G}∃z⃗ : ⋀_{w_{j} ∈dom(λ_{i})}w_{j} = w_{j}λ_{i}) ∧ x_{1} = v_{1} ∧ … ∧ x_{n} = v_{n}) ∨ d \end{aligned}

If P is irreducible by R_{EAC} and G ≠ ∅.

Fig. 3. Negation elimination in simple formulae

irreducible forms allows a very easy generalization of the results when a wider class of formulae has the same irreducible forms.

Acknowledgments: I wish to thank Alexandre Boudet and Hubert Comon for many fruitful discussions about AC-unification algorithms and complement problems. Special thanks to Hubert Comon for reading the first drafts of this article, and for many valuable comments and suggestions.

References

1. Hubert Comon. Unification et disunification: Théorie et applications. Thèse de Doctorat, Institut National Polytechnique de Grenoble, France, 1988.

2. Hubert Comon. Ground normal forms and inductive proofs. part I: complement problems. Submitted to Journal of Symbolic Computation, 1991.

3. Hubert Comon and Maribel Fernández. Negation elimination in equational formulae. In Proc. 17th Mathematical Foundations of Computer Science, Praha, 1992.

4. Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of 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. J.-M. Hullot. Associative commutative patern matching. In Proc. 6th IJCAI (Vol. I), Tokyo, pages 406–412, August 1979.

7. Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.

8. Emmanuel Kounalis. Learning from examples and counterexamples with equational background knowledge. In Proc. 2nd IEEE Conference on Tools for Artificial Intelligence, 1990.

9. Emmanuel Kounalis, Denis Lugiez, and L. Pottier. Complement problems modulo associativity and commutativity. In Proc. 16th Mathematical Foundations of Computer Science, Warsaw. Springer-Verlag, 1991.

10. Jean-Louis Lassez, M. Maher, and K. Marriott. Elimination of negation in term algebras. In Proc. 16th Mathematical Foundations of Computer Science, Warsaw. Springer-Verlag, 1991.

11. Jean-Louis Lassez and K. G. Marriott. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):1–17, September 1987.

12. A. Laville. Lazy pattern matching in the ML language. In Proc. 7th Conf. Found. of Software Technology and Theoretical Computer Science, Pune, INDIA, LNCS 287, December 1987.

13. D. Lugiez and J.-L. Moysset. Complement problems and tree automata in AC-like theories. In Proc. Symp. on Theoretical Aspects of Computer Science, Würzburg, 1993.

This article was processed using the LaTEX macro package with LLNCS style