Unification and matching are fundamental operations in many symbol- manipulation systems such as automated deduction, rewriting and logic programming. In most applications involving unification and matching, typically the same term is repeatedly unified either with several other terms or with every subterm of these terms. Moreover, very often these match and unification attempts fail. Existing methods are inadequate for repeated unification/matching because either they are inefficient or they make strong assumptions on the structure of the input. In addition, they do not handle failures properly. The basic issues involved in repeated matching and unification and the means to design efficient algorithms for them will be addressed in this project. Moreover, algorithms that can detect failures quickly will be designed. The practical importance of our algorithms will be studied through a number experiments that will be conducted. The experiments will provide the best choice of algorithms which will be used to build a rewrite system and to improve the SBProlog interpreter/compiler. This research will yield new classes of algorithms for repeated matching and unification and also speed up implementations of a large class of symbol-manipulation systems.
