ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/4 - 2003  - pp.401-433  - doi:10.3166/tsi.22.401-433
TITRE
Une approche générique de la réécriture

RÉSUMÉ
Dans cet article, nous étudions la réécriture en tant que système de preuve opérationnel de façon générique (c'est-à-dire indépendamment de la logique sous-jacente). Dans ce but, nous proposons des conditions simples qui permettent de caractériser les logiques où ce type de preuve effective peut être appliqué. Ces conditions sont fondées sur une propriété définie sur les arbres de preuve, que nous appelons semi-commutation. Nous montrons alors comment axiomatiser les notions usuelles de terminaison, confluence et confluence locale au sein de ce métaformalisme. Cela nous permet de retrouver les résultats fondamentaux de Church-Rosser et Newman et de proposer une méthode de complétion de Knuth et Bendix générique.


ABSTRACT
In this paper we study rewriting as an operational proof system in a generic (i.e. logic-independent) way. To do this, we propose simple conditions which allow to characterise logics were this kind of effective proof can be applied. This conditions are based on a proof tree property, that we call semi-commutation. We then show how to define the standard notions of termination, confluence and local confluence in this meta-formalism. It allows us to obtain the fundamental results of Church-Rosser and Newman and to propose a generic Knuth and Bendix completion method.


AUTEUR(S)
Marc AIGUIER, Diane BAHRAMI

MOTS-CLÉS
réécriture abstraite, logicalité, propriété de Church-Rosser, lemme de Newman, système de Knuth et Bendix, complétion de Knuth et Bendix.

KEYWORDS
abstract rewriting, logicality, Church-Rosser property, Diamond lemma, Knuth and Bendix system, Knuth and Bendix completion.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (369 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier