Masters Theses

Abstract

"Unification algorithms are an essential component of automated reasoning and term rewriting systems. Unification finds a set of substitutions or unifiers that, when applied to variables in two or more terms, make those terms identical or equivalent. Most systems use Robinson's unification algorithm or some variant of it. However, terms containing functions exhibiting properties such as associativity and commutativity may be made equivalent without appearing identical. Systems employing Robinson's unification algorithm must use some mechanism separate from the unification algorithm to reason with such functions. Often this is done by incorporating the properties into a rule base and generating equivalent terms which can be unified by Robinson's algorithm. However, rewriting the terms in this manner can generate large numbers of useless terms in the problem space of the system.

If the properties of the functions are incorporated into the unification algorithm itself, there is no need to rewrite the terms such that they appear identical. Stickel developed an algorithm to unify two terms containing associative and commutative functions. The unifiers (there may be more than one) are found by creating a homogeneous linear Diophantine equation with integer coefficients from the terms being unified. The unifiers can be constructed from solutions to this equation.

The unifiers generated from one solution of the Diophantine equation are independent of any other solution to the equation. Therefore, once the Diophantine equation has been solved, the unifiers can be calculated from the solutions in parallel. We have implemented Stickel's AC unification algorithm to run in parallel on a local area network of Sun 4/110 workstations in an effort to improve the speed of AC unification"--Abstract, page ii.

Advisor(s)

Wilkerson, Ralph W.

Committee Member(s)

McMillin, Bruce M.
Powell, Thomas G.

Department(s)

Computer Science

Degree Name

M.S. in Computer Science

Comments

The research was partially funded by the McDonnell Douglas Corporation and the Missouri Research Assistance Act.

Publisher

University of Missouri--Rolla

Publication Date

Fall 1988

Pagination

vii, 92 pages

Note about bibliography

Includes bibliographical references (pages 44-45).

Rights

© 1988 David John Kleikamp, All rights reserved.

Document Type

Thesis - Open Access

File Type

text

Language

English

Thesis Number

T 5765

Print OCLC #

19452967

Download

Share

 
COinS