Equational reasoning is ubiquitous in many areas of computer science such as automated theorem proving, formula manipulating systems, algebraic specifications, and functional and logic programming languages. Rewriting is a mathematical formalism which can offer both flexible computing and effective reasoning with equations. We aim at developing a unified theory of computational-logical-algebraic systems based on the theory of rewriting systems combining computations and proofs.
Computing Information Theory (Prof. Toyama)
Our research focuses on important theoretical features of the rewriting paradigm, such as the Church-Rosser property, the termination property, and the modular property. We are also interested in 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. We are investigating program verification and transformation systems based on automated theorem proving techniques.
- Rewriting Theory
- Foundations of Softwares
- Automated Deduction