Une axiomatisation de la réécriture abstraite
Institution:
Evry-Val d'EssonneDisciplines:
Directors:
Abstract EN:
In this thesis, we present a logic-independent framework for rewriting. Firstly, we define a 'mould', based on formal systems, for the logics adapted to rewriting. Then, we give conditions on permutation of the logics inference rules, which allow to select the predicates which are appropriate for rewriting. We obtain a generalised version of Birkhoff's logicality theorem for these predicates. In this framework, we re-define the standard notions of rewriting (rewrite system, derivation, termination, confluence, etc. ) and we obtain a generalised version of several rewriting results (the Church-Rosser property, the Diamond lemma, etc. ). Finally, we generalise D. Knuth and P. Bendix's completion by means of a set of inference rules inspired by L. Bachmair and J. Hsiang's completion rules.
Abstract FR:
Dans cette thèse, nous présentons un cadre d'étude de la réécriture indépendant de la logique sous-jacente. Nous définissons d'abord un <<moule>> pour les logiques adaptées à la réécriture, sur la base des systèmes formels. Puis, nous donnons des conditions de permutation des règles d'inférence qui permettent de déterminer les prédicats appropriés pour la réécriture. Nous obtenons une version généralisée du théorème de logicalité de G. Birkhoff pour ces prédicats. Dans ce cadre, nous redéfinissons les notions usuelles de la réécriture (système de réécriture, dérivation, terminaison, confluence, etc. ) et obtenons une forme générale des résultats fondamentaux de la réécriture (propriété de Church-Rosser, lemme de Newman, etc. ). Enfin, nous présentons une généralisation de la complétion de D. Knuth et P. Bendix à l'aide d'un ensemble de règles d'inférence inspiré des règles de L. Bachmair et J. Hsiang.