Doctoral Dissertations

Keywords and Phrases

Complete Sets of Reductions; Knuth-Bendix Procedure; E-Completion; E-Unification; Conditional Reductions; Finite Termination Property; Church-Rosser Property

Abstract

"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.

Advisor(s)

Wilkerson, Ralph W.

Committee Member(s)

Kellogg, Ronald Thomas
Dekock, Arlan R.
Ho, C. Y. (Chung You), 1933-1988
Zobrist, George W. (George Winston), 1934-

Department(s)

Computer Science

Degree Name

Ph. D. in Computer Science

Publisher

University of Missouri--Rolla

Publication Date

Summer 1988

Pagination

ix, 125 pages

Note about bibliography

Includes bibliographical references (pages 122-124).

Rights

© 1988 Timothy B. Baird, All rights reserved.

Document Type

Dissertation - Open Access

File Type

text

Language

English

Thesis Number

T 5737

Print OCLC #

20142341

Download

Share

 
COinS