Abstract FR:

Présentation d'un système d'inférence réalisant la complétion de théories équationnelles dans une structure générale. Il est montré que ce système peut être appliqué aux termes et aux polynômes et permet d'y définir une famille d'algorithmes de complétion du type de ceux de Kmith-Bendix et Buchberger. Ce système a été implémenté en CAML. La seconde partie traite la généralisation de termes et de formules logiques. Deux systèmes d'inférence sont proposés. Enfin, une méthode de généralisation de formules du calcul des prédicats du premier ordre, basée sur le formalisme polynomial en logique, est introduite