\pagestyle{empty}
\begin{center}
{\LARGE Re'sume'}
\end{center}

La surre'duction est une me'thode ge'ne'rale et comple`te, 
d'unification dans les syste`mes de re'e'criture confluents et 
noethe'riens. Dans ce travail, nous avons combine' le me'canisme 
de comple'tion dite ordonne'e, qui permet d'obtenir de tels 
syste`mes e'ventuellement infinis, et le me'canisme de 
surre'duction, pour obtenir une nouvelle me'thode d'unification, 
ge'ne'rale et comple`te. Nous avons travaille' dans le cadre 
contraint, ce qui nous a semble' e^tre le formalisme ide'al 
pour optimiser la me'thode en inte'grant la notion de basicite' 
: nous stockons les parties prote'ge'es d'un terme dans une 
contrainte associe'e au terme.

Notre proce'dure d'unification est de'crite par un syste`me de 
re`gles d'infe'rence, combinant la comple'tion ordonne'e 
basique et la surre'duction basique. Partant d'une the'orie 
e'quationnelle quelconque, d'un ordre de simplification et 
d'une e'quation a` re'soudre, notre proce'dure calcule, au bout 
d'un temps fini, toute solution donne'e. Ceci reste vrai me^me 
lorsque le syste`me d'e'quations initial n'admet pas de syste`me 
confluent et noethe'rien fini, car les e'tapes de surre'duction 
sont faites en me^me temps que la comple'tion de notre syste`me. 
Cette me'thode d'unification est implante'e dans notre logiciel 
UREVEAL.

Dans cette the`se, nous avons aussi pre'sente' par ailleurs, 
deux strate'gies pour ame'liorer l'efficacite' et la terminaison 
de la surre'duction. Elles sont toutes deux base'es sur la 
notion combinatoire de graphe~: l'une sur un graphe 
d'ope'rateurs et l'autre sur un graphe de termes. La seconde est 
meilleure que la premie`re, mais plus complique'e a` mettre en 
place. Nous construisons un graphe a` partir de l'ensemble 
d'e'quations de'crivant la the'orie e'quationnelle et 
l'e'quation a` re'soudre, puis gra^ce a` ce graphe, nous 
e'liminons des branches inutiles dans les e'tapes de 
surre'duction. C'est ce que nous appelons surre'duction dirige'e 
par un graphe. Ces strate'gies d'optimisation ne seront 
implante'es qu'ulte'rieurement.


Mots cle's : re'solution d'e'quations, unification, re'e'criture, 
surre'duction basique, comple'tion basique, contrainte, 
graphe d'ope'rateurs, graphe de termes.


\begin{center}
{\LARGE Abstract}
\end{center}

Narrowing is a general and complete tool for unification w.r.t. 
a canonical rewrite system. In this thesis, we combine ordered 
completion, which gives us a possibly infinite canonical 
rewrite system and narrowing, to deduce a complete procedure for 
general unification. We work in a constrained setup which seems 
to be an ideal formalism to optimize our method, by adapting 
the so-called basic strategy : we keep the protected part of a 
term in a constraint linked to the term.

We give a set of inference rules to describe our procedure, 
combining ordered basic completion and basic narrowing. Given 
any equational theory, a simplification ordering, and an 
equation to be solved, our procedure computes, in finite time, 
any solution. We do not assume here that the initial set of 
equations admits a finite canonical system, because steps of 
narrowing are computed simultaneously w.r.t. the completion 
steps. This method is implemented in our software UREVEAL.

In this thesis we also study two combinatorial strategies to 
improve efficiency and termination of narrowing. Both are based 
on the notion of a graph : first on a graph of operators, the 
other on a graph of terms. The second is better than the first, 
but more complicated to run. We build a graph with the set of 
equations discribing our equationnal theory and the equation to 
be solved; then with the graph we cut useless narrowing steps. 
This is called narrowing directed by a graph. Such strategies 
are not yet built into UREVEAL.

Keywords : equations solving, unification, term rewriting, 
basic narrowing, basic completion, constraint, 
graph of operators, graph of terms.