论文部分内容阅读
本文介绍了项重写系统研究的最新课题和动态项重写计算的基本理论，着重阐述了新的项重写系统等价性证明的归纳证明理论及最新研究进展，设计并实现了四种新的项重写系统重写策略，集成原有研究成果，实现了DTRC的形式自动证明平台，该平台能实现项重写系统在特定域上等价性的自动证明和弱终止性的自动证明。
本文的创新之处是设计并实现了四种新的重写策略，使完成后的DTRC的形式自动证明平台能够提供7种重写策略，丰富了重写证明的手段；另外，还给出了两个项重写系统等价性自动证明时从TRS向DTRC转化的方法，为项重写系统等价性的自动证明提供了具体操作方法。