Term rewriting systems form an important computational paradigm in programming languages, abstract data type specification and verification, automated deduction and computer algebra. The theory of rewriting has developed rapidly, and new application areas are being explored. However, not much is known about the computational aspects of rewrite operations. In this proposal the basic operations in rewriting, and the means to design and analyze efficient algorithms for them, will be studied. Practical algorithms will be designed on both sequential and parallel machines. Algorithms, which learn efficiently from their history, will be designed for important and useful classes of rewrite systems. Several facets of the matching problem will be studied from a novel perspective. The practical performance of the designed algorithms will also be investigated. This investigation will be useful in improving the efficiency of rewrite-based systems as well as provide understanding of the inherent complexities and limitations of the rewrite approach.
