**CONTEJEAN Evelyne**
Ph.D

Group : Toccata

*Elements for Decidability of Unification modulo Distributivity*
Starts on 01/09/1988

Advisor :

**Funding :**
**Affiliation :** Université Paris-Saclay

**Laboratory :**
**Defended** on 03/04/1992, committee :

Gérard HUET, Président

Alain COLMERAUER

Mehmet DINCBAS

Marie-Claude GAUDEL

Jean-Pierre JOUANNAUD

Claude KIRCHNER

Leszec PACHOLSKI

**Research activities :**
- Automated deduction

- Rewriting

**Abstract :**
In this thesis, we give some tools for unification (or equations solving) modulo distributivity (or modulo D) of a symbol f on a symbol g. This theory is one of the last for which it remains still unkown whether it is decidable or not.

In the first part, we study some particular problems obviously decidable, balanced problems containing only some terms without the g symbol. We precisely describe the set of solutions, which is possibly infinite. This is done with structures for which there is a property of unique maximal decomposition with respect to a AC1 operator. In a second part, the notions of indexation and stratification are introduced and are used in order to characterize the equality modulo D of two terms. Then we prove, thanks to stratification, the completeness of a set of transformation rules. This set reduces a problem to a babanced problem, and a balanced problem is solved by AC1 unification on structures. For technical reasons, we only handle a particular sort of problems, caracterized by a condition of acyclicity.

Finally, we describe a new, efficient algorithm for solving systems of linear Diophantine equations.