La technique du renommage, appliquée exhaustivement, permet d'obtenir une forme clausale polynomiale. Nous choisissons de l'appliquer partiellement, de façon a minimiser certains criteres syntaxiques, principalement le nombre de clauses, tout en conservant une complexité polynomiale. Nous montrons qu'un algorithme efficace permet d'obtenir le nombre optimal de clauses sur les formules linéaires. Enfin, nous étudions l'influence de ces transformations sur les réfutations par la methode de resolution, autant théoriquement expérimentalement

Dans une première partie, nous montrons qu'il est possible d'établir une correspondance naturelle entre les preuves en déduction naturelle de la validité d'une formule et les réfutations par resolution d'un ensemble de clauses obtenues en appliquant a la négation de cette formule une mise sous forme clausale non standard utilisant une technique de renommage. En particulier, nous montrons qu'il est possible de simuler le fonctionnement d'un calcul des sequents proche de celui de Gentzen par la resolution et nous montrons comment traduire des réfutations par resolution en preuve en déduction naturelle. De plus, nous proposons plusieurs ameliorations de cette mise sous forme clausale avec renommage permettant de faciliter la recherche d'une réfutation par resolution. Dans une deuxième partie, nous décrivons en détail des techniques permettant une mise en œuvre efficace de la resolution avec sortes ordonnées ainsi qu'un principe d'indexation des clauses permettant de résoudre efficacement de nombreux problèmes-clés (tels ceux poses par la subsomption, l'utilisation de systèmes de réécriture...). Ces algorithmes ont ete utilises dans l'implémentation d'un démonstrateur par resolution que nous avons réalisé dans le cadre d'atinf