Christopher Lynch ; Polina Strogova - SOUR graphs for efficient completion

dmtcs:247 - Discrete Mathematics & Theoretical Computer Science, January 1, 1998, Vol. 2 -
SOUR graphs for efficient completionArticle

Authors: Christopher Lynch 1; Polina Strogova 2

  • 1 Computer Science Department [Potsdam NY]
  • 2 Constraints, automatic deduction and software properties proofs

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.

Volume: Vol. 2
Published on: January 1, 1998
Imported on: March 26, 2015
Keywords: SOUR graphs,completion algorithms,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

1 Document citing this article

Consultation statistics

This page has been seen 322 times.
This article's PDF has been downloaded 253 times.