Discrete Mathematics & Theoretical Computer Science
Volume 2 n° 1 (1998), pp. 1-25
| author: | Christopher Lynch and Polina Strogova |
|---|---|
| title: | SOUR graphs for efficient completion |
| keywords: | SOUR graphs, completion algorithms |
| abstract: | We introduce a data structure called SOUR graphs and present an efficient Knuth-Bendix completion procedure based on it. SOUR 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. |
| reference: | Christopher Lynch and Polina Strogova (1998), SOUR graphs for efficient completion, Discrete Mathematics and Theoretical Computer Science 2, pp. 1-25 |
| ps.gz-source: | dm020101.ps.gz |
| ps-source: | dm020101.ps (281 K) |
| pdf-source: | dm020101.pdf (321 K ) |
The first source gives you the `gzipped' PostScript, the second the plain PostScript and the third the format for the Adobe accrobat reader. Depending on the installation of your web browser, at least one of these should (after some amount of time) pop up a window for you that shows the full article. If this is not the case, you should contact your system administrator to install your browser correctly.
Automatically produced on Tue Jan 19 17:49:02 MET 1999 by gustedt