University of Houston
Department of Computer Science
In partial fulfillment of the Requirements for the Degree of
Master of Science
Hang Shi
will defend his thesis
Symbolic Computation and Equational Programming
Abstract
Equational formulas of the form M = N occur frequently in mathematics, logic and
computer science. A set of given equations can always lead to other equations.
Equations are also used as definitions. This is well known in computer science
since programs written in applicative languages, abstract interpreter definitions,
and algebraic data type definitions are clearly of this nature.
LR² program is a laboratory for developing and evaluating fast, efficient and practical
rewriting techniques. Term rewriting system gives us an elegant framework for
symbolic computation, theorem proving, equational reasoning and equational logic programming.
LR² program allows non-left linear rules such as x+ -x → 0 and
equal(x,x) → true , etc. In this thesis an
efficient Non Left Linear AC matching algorithm is developed. This algorithm is
implemented with the tabling algorithm in and its performance is studied on
several benchmarks.
Date: Wednesday, November 22, 2000
Time: 11:00 AM
Place: 550-PGH
Faculty, students, and the general public are invited.
Thesis Advisor: Dr. Rakesh Verma