AbstractExtended completion of term rewriting systems may abort or succeed for given input, depending on the strategy used for selecting a derivation step from the set of possible ones. Thus, some derivation steps are fatal} in the sense that they destroy the possibility of a successful derivation sequence. In this paper we characterize such steps. The results presented are of relevance to efficiency improvement, especially for implementations applying backtracking.
Categories and Subject Descriptors: F.4.2 [Mathematical Logic and Formal Languages]: Grammars and Other Rewriting Systems
Additional Key Words and Phrases: term rewriting systems, Knuth-Bendix completion, equational theories, rewriting modulo a congruence
Selected references
- L Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1-18, August 1988.
- Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In Proceedings, Symposium on Logic in Computer Science, pages 346-357, Cambridge, Massachusetts, 16-18 June 1986. IEEE Computer Society.
- Nachum Dershowitz, Leo Marcus, and Andrzej Tarlecki. Existence, uniqueness, and construction of rewrite systems. SIAM Journal on Computing, 17(4):629-639, August 1988.
- Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155-1194, November 1986.
- D. Kapur, D. R. Musser, and P. Narendran. Only prime superpositions need be considered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation, 6(1):19-36, August 1988.
- Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233-264, April 1981.