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

En algorithmique distribuée, le modèle asynchrone par envoi de messages et à pannes est connu et utilisé dans de nombreux articles de par son réalisme,par ailleurs il est suffisamment simple pour être utilisé et suffisamment complexe pour représenter des problèmes réels. Dans ce modèle, les n processus communiquent en s'échangeant des messages, mais sans borne sur les délais de communication, c'est-à-dire qu'un message peut mettre un temps arbitrairement long à atteindre sa destination. De plus, jusqu'à f processus peuvent tomber en panne, et ainsi arrêter définitivement de fonctionner. Ces pannes indétectables à cause de l'asynchronisme du système limitent les possibilités de ce modèle. Dans de nombreux cas, les résultats connus dans ces systèmes sont limités à une stricte minorité de pannes. C'est par exemple le cas de l'implémentation de registres atomiques et de la résolution du renommage. Cette barrière de la majorité de pannes, expliquée par le théorème CAP, s'applique à de nombreux problèmes, et fait que le modèle asynchrone par envoi de messages avec une majorité de pannes est peu étudié. Il est donc intéressant d'étudier ce qu'il est possible de faire dans ce cadre.Cette thèse cherche donc à mieux comprendre ce modèle à majorité de pannes, au travers de deux principaux problèmes. Dans un premier temps, on étudie l'implémentation d'objets partagés similaires aux registres habituels, en définissant les bancs de registres x-colorés et les α-registres. Dans un second temps, le problème du renommage est étendu en renommage k-redondant, dans ses versions à-un-coup et réutilisable, et de même pour les objets partagés diviseurs, étendus en k-diviseurs. / In distributed computing, asynchronous message-passing model with crashes is well-known and considered in many articles, because of its realism and it issimple enough to be used and complex enough to represent many real problems.In this model, n processes communicate by exchanging messages, but withoutany bound on communication delays, i.e. a message may take an arbitrarilylong time to reach its destination. Moreover, up to f among the n processesmay crash, and thus definitely stop working. Those crashes are undetectablebecause of the system asynchronism, and restrict the potential results in thismodel.In many cases, known results in those systems must verify the propertyof a strict minority of crashes. For example, this applies to implementationof atomic registers and solving of renaming. This barrier of a majority ofcrashes, explained by the CAP theorem, restricts numerous problems, and theasynchronous message-passing model with a majority of crashes is thus notwell-studied and rather unknown. Hence, studying what can be done in thiscase of a majority of crashes is interesting.This thesis tries to analyse this model, through two main problems. The first part studies the implementation of shared objects, similar to usual registers,by defining x-colored register banks, and α-registers. The second partextends the renaming problem into k-redundant renaming, for both one-shotand long-lived versions, and similarly for the shared objects called splitters intok-splitters.