Abstract FR:

Cette these est une etude de l'unification et de ses rapports et liens avec la theorie de la demonstration. Premierement, nous regardons en details les problemes de decision pour l'unification des termes du second ordre en situant avec precision la frontiere qui separe la decidabilite de l'indecidabilite. Nous appliquons alors ces resultats au cas des predicats du second ordre et obtenons un resultat d'indecidabilite. Deuxiemement, nous montrons les liens existants entre la e-unification rigide et la logique lineaire du second ordre par un codage direct et simple. Finalement, nous appliquons ces resultats au cas de la logique lineaire multiplicative (et multiplicative-additive) du second ordre avec quantification du premier ordre pour en obtenir l'indecidabilite des que le langage contient une constante de fonction d'arite au moins egale a deux