Abstract FR:

Dans ce mémoire nous étudions deux aspects de la réécriture. Le premier travail est une contribution à l'étude structurelle de certaines classes de réécriture. Nous montrons comment certains problèmes d'accessibilité se traitent à la lumière des automates finis d'arbres. De plus nous avons construit un logiciel nommé Valerian résolvant certains de ces problèmes en temps réel. Le second travail consiste en la mise en oeuvre d'un système de démonstration automatique de théorème basé sur un calcul par superposition et fonctionnant pour des clauses logiques du premier ordre avec équations