Abstract FR:

Les ensembles de termes lineaires et ordonnes en logique combinatoire sont etudies en vue d'un codage vectoriel dans les "machines de reduction". Une formalisation de l'egalite extensionnelle est enoncee permettant son utilisation dans un algorithme de generation de tels ensembles. Des conditions suffisantes de leurs finitudes sont demontrees. Les resultats de cet algorithme sont obtenus au moyen d'un nouveau systeme de calcul formel: ecole