Les règles de transformation des problèmes equationnels sont donnes permettant, en particulier, de décider de l'existence d'une solution fermée. Comme première application, il est montre comment calculer une grammaire pour le langage des termes fermes irréductibles par un système de réécriture. D'autres applications et extensions sont ensuite envisagées. En particulier, en programmation logique et dans les spécifications algébriques

Il existe de nombreux systèmes de preuves par induction visant à automatiser la preuve de théorèmes mathématiques. Cependant, un système de preuve ne peut pas être réellement automatique si plusieurs interactions humaines -- telles que l'apport de lemmes, de généralisations, ou de schémas d'induction -- sont nécessaires pour prouver des théorèmes qui semblent triviaux pour un être humain. Par exemple, la preuve de la commutativité de la multiplication (y * x = x * y) doit notamment recourir à des lemmes exprimant la distributivité de la multiplication ainsi que la distributivité et la commutativité de l'addition. Dans cette thèse, nous proposons des apports aux méthodes de preuve par induction dans le sens d'une plus grande automatisation. Ces apports sont constitués de deux heuristiques efficaces et surtout de deux algorithmes corrects. Le premier algorithme calcule des généralisations correctes pour des théories non-conditionnelles. Le second est une méthode d'induction originale -- la "partition de termes"-- permettant la preuve automatique de théorèmes inductifs.