Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité.<br /><br />L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations.<br /><br />Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo. <br /><br />Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.

Depuis les travaux de Martelli et Montanari en 1982, la resolution de problemes de E-unification s'effectue souvent par transformation de systemes d'equations. L'objectif de cette these est de presenter des nouvelles regles de transformations qui de- crivent de facon unifiee comment appliquer des axiomes a la ra- cine des termes. Les proprietes theoriques de ces regles sont etablies (correction, completude...). Nous prouvons egalement que cette approche, basee sur la notion de presentations strictement resolventes, est plus generale que des algorithmes tres connus (Root-Rewriting [J. Gallier & W. Snyder ], Mutation Syntaxique [C. Kirchner ]). Une analyse du comportement de ces regles per- met d'etablir l'inter^et de l'application d'axiomes a la racine et de definir le type de presentations strictement resolventes qui devraient fournir les meilleurs resultats. Ces presentations sont generees automatiquement. Pour ce faire, nous introduisons la notion de completion strictement resolvente. Elle permet de definir les proprietes theoriques des regles de completion donnees. Differentes strategies sont etu- diees, allant d'une strategie qui termine toujours a la strategie (parfois divergente) conduisant a une presentation tres efficace. Des recherches theoriques peuvent s'effectuer dans ce (nouveau) formalisme general. Elles s'appliquent aux algorithmes subsumes par cette approche. Par exemple, les avantages vis a vis du parallelisme sont etablis et conduisent a une presentation compacte de l'ensemble des unificateurs. Des optimisations theoriques plus complexes sont egalement etudiees. La detection des instanciations inutiles des variables lors de l'unification d'un terme avec les t^etes de regles est la plus importante. Elle permet d'etablir la completude des solutions donnees pour un probleme m^eme si la presentation n'est pas strictement resol- vente (completion divergente). Les resultats experimentaux mettent en valeur la simplicite et la generalite de cette nouvelle approche. Sa generalite permet egalement de comparer les differents algorithmes et de justifier l'utilisation de la strategie non complete de generation des re- gles. L'etude de cas particuliers montre que l'on peut ainsi ob- tenir des resultats tres interessants en un temps tout a fait raisonnable. On peut donc envisager d'utiliser ce module de E- unification au sein d'un demonstrateur.

Cette thèse décrit trois travaux de formalisation en Coq. Le premier chapitre s'intéresse à l'implémentation d'une procédure de décision efficace pour les algèbres de Kleene, pour lesquelles le modèle des langages réguliers est initial : il est possible de décider la théorie équationelle des algèbres de Kleene via la construction et la comparaison d'automates finis. Le second chapitre est consacré à la définition de tactiques pour la réécriture modulo associativité et commutativité en utilisant deux composants : une procédure de décision réflexive pour l'égalité modulo AC, ainsi qu'un greffon OCaml implémentant le filtrage modulo AC. Le dernier chapitre esquisse une formalisation des circuits digitaux via un plongement profond utilisant les types dépendants de Coq ; on s'intéresse ensuite à prouver la correction totale de circuits paramétriques.

Cette thèse décrit trois travaux de formalisation en Coq. Le premier chapitre s'intéresse à l'implémentation d'une procédure de décision efficace pour les algèbres de Kleene, pour lesquelles le modèle des langages réguliers est initial : il est possible de décider la théorie équationelle des algèbres de Kleene via la construction et la comparaison d'automates finis. Le second chapitre est consacré à la définition de tactiques pour la réécriture modulo associativité et commutativité en utilisant deux composants : une procédure de décision réflexive pour l'égalité modulo AC, ainsi qu'un greffon OCaml implémentant le filtrage modulo AC. Le dernier chapitre esquisse une formalisation des circuits digitaux via un plongement profond utilisant les types dépendants de Coq ; on s'intéresse ensuite à prouver la correction totale de circuits paramétriques. / This thesis describe three formalisations in Coq. The first chapter is devoted to the implementation of an efficient decision procedure for Kleene algebras : as regular languages form the initial model of Kleene algebras, we can resort to finite automata algorithms to solve equations in an arbitrary Kleene algebra. The second chapter present a set of tools for rewriting modulo associativity and commutativity built using two components: a reflexive decision procedure for equality modulo AC and an OCaml plug-in for pattern matching modulo AC. The third chapter defines a deep-embedding of hardware circuits using dependent types that is used to model and prove the functional correctness of parametrised circuits.

(Résumé en français) "Exercices de style" est-elle une oeuvre simplement comique et acrobatique ? Sa réception positive mais plutôt superficielle auprès du public semble avoir dissimulé ses aspects plus profonds et plus problématiques. A nos yeux, en revanche, les 99 "Exercices" d'écriture sont tout à fait aptes à éclairer les problèmes essentiels de la création littéraire et de la transmission de l'énoncé qu'est la communication verbale. La structure multi-dimensionnelle du livre, où les "Exercices" s'enchaînent, se complètent et se répondent, nous rend sensibles non seulement aux réseaux intratextuels qu'entretiennent les "Exercices", mais également aux liens intertextuels qui lient cetains d'entre eux et les discours littéraires et non littéraires préexistants. D'autres "Exercices" témoignent du regard autoréflexif de l'écrivain, ceux qui peuvent être considérés comme autoparodie. Par ailleurs, la virtuosité des variations stylistiques exige parfois du lecteur une attention particulière - face à quelques variations hermétiques et presque inintelligibles, on devra recourir à d'autres composants du livre qui serviront de "traductions". La terme "traduction" devra être compris non seulement dans le sens de la transmission de messages entre différentes langues, mais aussi dans le sens de la transposition d'un signifiant dans d'autres signifiants, ou bien de la "réécriture" d'un énoncé, tout en restant dans la même langue. Si le principe des "Exercices de style" est de renouveler à l'infini des exercices d'écrire, ou plutôt de réécrire LE texte original - "qui est d'ailleurs inexistant" -, nous pouvons poser, semble-t-il, que la Littérature est basée sur le même procédé de tâtonnements,auquel le lecteur est enctraîné à participer. (Abstract in English) Is "Exercises in style" just a comic and acrobatic book ? The fact that the readers welcomed it so favourably - but rather superficially - seems to have overshadowed its more serious and problematic aspects. In our opinion indeed, Queneau's ninety-nine writing "Exercises" can clearly shed light on the essential problems of literary creation and utterance transmission, i.e. verbal communication. The book presents an intricate structure:the "Exercises" are linked together, echo each other and complement one another. Through this multidimensional structure, we can see the intratextual networks between the "Exercises" as well as their intertextual relations with pre-existent literary and non-literary discourses. Other "Exercises" show the author's autoreflective, autoparodic attitude. Furthermore, the virtuosity of the stylistic variations sometimes requires particular attention from the reader. To understand some abstruse, sometimes almost unintelligible "Exercises", the reader has to resort to other parts of the book, which will serve as "translation" for these enigmatic passages. The word "translation" here means not only transmission of messages from a language to another, but also transposition of a signifier to other signifiers - in other words, "rewriting" of an utterance in the same language. If the principle of "Exercices in style" is to practice writing endlessly, or rather rewriting of THE original text - "which actually does not exist" - , we can reasonably deduce that Literature is based on the same trial and error process the reader will inevitably take part in.