Prolog, acronyme de PROgrammation LOGique, est lÕun des principaux langages de programmation logique. Un de ces concepts de base est \emph{l'unification des ter mes} qui consiste à instancier les variables de deux termes afin que ces derniers soient syntaxiquement égaux. Techniquement parlant, l'unification est équivalente à la résolution de conjonctions d'équations dans la théorie des arbres finis ou infinis. Nous présentons dans ce papier une extension au premier ordre du mécanisme de l'unification des termes par un algorithme de résolution de contraintes du premier ordre (toute quantification et t out symbole logique) dans une théorie étendue $T$ d'arbres finis ou infini s. Pour cela, nous étendons tout d'abord la théorie des arbres finis ou in finis par la relation $\fini(t)$ qui permet de contraindre le terme $t$ à être un arbre fini et présentons une axiomatisation au premier ordre de cette théorie étendue. Nous montrons ensuite la complétude de $T$ par un solveur de contraintes du premier ordre sous forme de 16 règles de réécriture. Nous terminons ce papier par une implémentation en CHR de notre solveur. CHR (Constraint Handling Rules) est un langage de programmation logique à base de règles de réécriture qui a fait ses preuves dans la résolution de plusieurs problèmes complexes en IA. Cependant, il n'existe à c e jour aucun solveur CHR de contraintes du premier ordre. La complexité et l a puissance de nos 16 règles de réécriture posent un véritable challenge pour CHR et ses programmeurs. Nous montrons alors comment représenter en CHR la structure complexe des formules du premier ordre et comment traduire chaque règle de notre solveur en règles CHR afin d'obtenir le premier solveur CHR de contraintes du premier ordre !