This project continues and expands the research in the design, development, and implementation of techniques for enhancing the power and performance of equational systems. The three key areas for this research effort are rewrite operations, equational programming, and equational deduction, though the results will likely also be applicable to other areas such as (constraint) logic programming. Research on rewrite operations will focus on variants of pattern matching algorithms that are specifically tailored to lazy evaluation strategies for functional programming and to build the semantics of certain functions into the matching algorithms for equational deduction. The investigations in equational deduction will center on the PI's recently proposed basic completion method, in which no inferences are applied at those subexpressions in formulas that are built up from substitutions generated in previous inference steps. The equational programming component of the proposal will focus on the further development of Equals --- a fast parallel implementation of a lazy language and the Integral system which uses symbolic constraint solving techniques to glue together program analyses across different paradigms. ***
