SOUR graphs for efficient completion

Christopher Lynch 1 Polina Strogova 2
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We introduce a data structure called \emphSOUR graphs and present an efficient Knuth-Bendix completion procedure based on it. \emphSOUR graphs allow for a maximal structure sharing of terms in rewriting systems. The term representation is a dag representation, except that edges are labelled with equational constraints and variable renamings. The rewrite rules correspond to rewrite edges, the unification problems to unification edges. The Critical Pair and Simplification inferences are recognized as patterns in the graph and are performed as local graph transformations. Our algorithm avoids duplicating term structure while performing inferences, which causes exponential behavior in the standard procedure. This approach gives a basis to design other completion algorithms, such as goal-oriented completion, concurrent completion and group completion procedures.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 1998, 2, pp.1-25
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00958899
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 13 mars 2014 - 15:52:02
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 13 juin 2014 - 11:51:08

Fichier

dm020101.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00958899, version 1

Collections

Citation

Christopher Lynch, Polina Strogova. SOUR graphs for efficient completion. Discrete Mathematics and Theoretical Computer Science, DMTCS, 1998, 2, pp.1-25. 〈hal-00958899〉

Partager

Métriques

Consultations de la notice

325

Téléchargements de fichiers

196