Research on program transformation systems based on automated theorem proving

项重写系统理论广泛应用于自动定理证明和计算模型等领域。本研究旨在建立基于项重写理论的自动化程序转换系统的基本理论和原型。具体成果包括一种程序转换模板的自动构造方法，一种新的高阶程序终止证明，一种改写归纳的引理自动生成方法，一种项改写系统的自动合流证明。

The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. This research aims to develop basic theories and prototypes for automated program transformation systems based on term rewriting theory. Concrete results include an automated construction method of program transformation templates, a new termination proof of higher-order programs, an automated lemma generation method for rewriting induction, an automated confluence prover of term rewriting systems.