Doctoral Dissertations

Abstract

"The Knuth-Bendix completion procedure produces complete sets of reductions but can not handle certain rewrite rules such as commutativity. In order to handle such theories, completion procedure were created to find complete sets of reductions modulo an equational theory. The major problem with this method is that it requires a specialized unification algorithm for the equational theory. Although this method works well when such an algorithm exists, these algorithms are not always available and thus alternative methods are needed to attack problems. A way of doing this is to use a completion procedure which finds complete sets of constrained reductions. This type of completion procedure neither requires specialized unification algorithms nor will it fail due to unorientable identities.

We present a look at complete sets of reductions with constraints, developed by Gerald Peterson, and the implementation of such a completion procedure for use with HIPER - a fast completion system. The completion procedure code is given and shown correct along with the various support procedures which are needed by the constrained system. These support procedures include a procedure to find constraints using the lexicographic path ordering and a normal form procedure for constraints.

The procedure has been implemented for use under the fast HIPER system, developed by Jim Christian, and thus is quick. We apply this new system, HIPER- extension, to attack a variety of word problems. Implementation alternatives are discussed, developed, and compared with each other as well as with the HIPER system.

Finally, we look at the problem of finding a complete set of reductions for a ternary boolean algebra. Given are alternatives to attacking this problem and the already known solution along with its run in the HIPER-extension system"--Abstract, page iii.

Advisor(s)

Wilkerson, Ralph W.

Committee Member(s)

Ho, C. Y. (Chung You), 1933-1988
Sager, Thomas
Smith, R. T. (Richard Thomas), 1925-
Zobrist, George
Hall, Leon M., 1946-

Department(s)

Computer Science

Degree Name

Ph. D. in Computer Science

Publisher

University of Missouri--Rolla

Publication Date

Spring 1992

Pagination

x, 132 pages

Note about bibliography

Includes bibliographical references (pages 126-131).

Rights

© 1992 Daniel Patrick Murphy, All rights reserved.

Document Type

Dissertation - Open Access

File Type

text

Language

English

Thesis Number

T 6409

Print OCLC #

26980935

Electronic OCLC #

1112109348

Download

Share

 
COinS