基于 DTRC的形式自动证明平台及其应用 (2004年)

动态项重写计算(DTRC)是项重写系统( TRS)的元计算模型 ,具有层次化结构和动态重写等特征 , 可应用于归纳定理的形式自动证明以及项重写系统弱终止性的形式自动证明等方面 。文中介绍了一个基于DTRC的形式自动证明平台及其在 TRS弱终止性自动证明上的应用 。