Keywords and Phrases
Complete Sets of Reductions; Knuth-Bendix Procedure; E-Completion; E-Unification; Conditional Reductions; Finite Termination Property; Church-Rosser Property
"In this paper we present a generalization of the Knuth-Bendix procedure for generating a complete set of reductions modulo an equational theory. Previous such completion procedures have been restricted to equational theories which generate finite congruence classes. The distinguishing feature of this work is that we are able to generate complete sets of reductions for some equational theories which generate infinite congruence classes. In particular, we are able to handle the class of equational theories which contain the associative, commutative, and identity laws for one or more operators.
We first generalize the notion of rewriting modulo an equational theory to include a special form of conditional reduction. We are able to show that this conditional rewriting relation restores the finite termination property which is often lost when rewriting in the presence of infinite congruence classes. We then develop Church-Rosser tests based on the conditional rewriting relation and set forth a completion procedure incorporating these tests. Finally, we describe a computer program which implements the theory and give the results of several experiments using the program"--Abstract, page ii.
Wilkerson, Ralph W.
Kellogg, Ronald Thomas
Dekock, Arlan R.
Ho, C. Y. (Chung You), 1933-1988
Zobrist, George W. (George Winston), 1934-
Ph. D. in Computer Science
University of Missouri--Rolla
ix, 125 pages
© 1988 Timothy B. Baird, All rights reserved.
Dissertation - Open Access
Print OCLC #
Link to Catalog Record
Baird, Timothy B., "Complete sets of reductions modulo A class of equational theories which generate infinite congruence classes" (1988). Doctoral Dissertations. 694.