Doctoral Dissertations
Abstract
“A major portion of the work and time involved in completing an incomplete set of reductions using an E-completion procedure such as the one described by Knuth and Bendix [KB70] or its extension to associative-commutative equational theories as described by Peterson and Stickel [PS81] is spent calculating critical pairs and subsequently testing them for coherence. A pruning technique which removes from consideration those critical pairs that represent redundant or superfluous information, either before, during, or after their calculation, can therefore make a marked difference in the run time and efficiency of an E-completion procedure to which it is applied.
The exploitation of term symmetry is one such pruning technique. The calculation of redundant critical pairs can be avoided by detecting the term symmetries that can occur between the subterms of the left-hand side of the major reduction being used, and later between the unifiers of these subterms with the left-hand side of the minor reduction. After calculation, and even after reduction to normal form, the observation of term symmetries can lead to significant savings.
The results in this paper were achieved through the development and use of a flexible E-unification algorithm which is currently written to process pairs of terms which may contain any combination of Null-E, C (Commutative), AC (Associative-Commutative) and ACI (Associative-Commutative with Identity) operators. One characteristic of this E-unification algorithm that we have not observed in any other to date is the ability to process a pair of terms which have different ACI top-level operators. In addition, the algorithm is a modular design which is a variation of the Yelick model [Ye85], and is easily extended to process terms containing operators of additional equational theories by simply "plugging in" a unification module for the new theory”--Abstract, page ii.
Advisor(s)
Wilkerson, Ralph W.
Dekock, Arlan R.
Committee Member(s)
Zobrist, George W. (George Winston), 1934-
Gillett, Billy E.
Stoecker, William V.
Trimble, S. Y.
Department(s)
Computer Science
Degree Name
Ph. D. in Computer Science
Publisher
University of Missouri--Rolla
Publication Date
Summer 1988
Pagination
x, 123 pages
Note about bibliography
Includes bibliographical references (pages 120-122).
Rights
© 1988 Blayne E. Mayfield, All rights reserved.
Document Type
Dissertation - Open Access
File Type
text
Language
English
Thesis Number
T 5740
Print OCLC #
20142440
Recommended Citation
Mayfield, Blayne E., "The role of term symmetry in E-unification and E-completion" (1988). Doctoral Dissertations. 692.
https://scholarsmine.mst.edu/doctoral_dissertations/692
Comments
The author would like to thank the American Academy of Dermatology and the McDonnell-Douglas corporation for their financial support.