论文部分内容阅读
本文介绍了项重写系统(TRSs)形式简洁且计算能力强，在计算科学里是一种受到广泛研究和应用的形式计算模型。对于项重写系统本身的性质(如合流性、终止性、等价性等)有大量的研究，学术界提出了很多有效的算法及模型来验证，其中冯速等设计开发了TRS元计算模型——动态项重写计算(DTRC)，它具有层次化结构和动态重写等特征，可应用于归纳定理的形式自动证明以及项重写系统弱终止性的形式自动证明等方面。
本文结合冯速等研究的关于项重写系统在特定域下弱终止性证明的最新成果，介绍我们设计开发的基于DTRC的形式自动证明平台及其在TRS弱终止下自动证明的应用。