Rewriting systems are mathematical formalisms which can offer both flexible computing and effective reasoning with equations. Thus, rewriting systems play an important role in various areas, such as automated theorem proving, formula manipulation systems, algebraic specifications, and functional and logic programming languages.
Our research focuses on important theoretical features of the rewriting paradigm, such as the Church-Rosser property, the termination property, and the modular property. The goal of this research is to obtain a unified theory of functional-logic-algebraic systems.
Rewriting systems can provide a useful tool for program transformations. We investigate this by developing a program transformation system for functional programs which base their semantics on rewriting systems. As a theoretical framework, we pay much attention to higher order rewriting and inductive theorem proving. We are also interested in the design and analysis of automated deduction systems which can offer both effective computation of functional (or logic) programming languages and flexible reasoning of automated theorem provers.
