Research Institute of Electrical Communication Tohoku University


Keisuke Nakano,Professor

Kentaro Kikuchi Yoshihito Toyama


Research Activities

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.

Research topics

  • Rewriting Theory
  • Foundations of Softwares
  • Automated Deduction

Fig. Proof by Equational Reasoning→Computation by Rewriting Systems