项重写系统等价性的形式自动证明

本项目以各种归纳法及申请者设计开发的项重写系统元计算模型“动态项重写计算”为主要工具，确立项重写系统等价性的形式自动证明方法，证明该方法的正确性。同时，实现该方法，确认其有效性，探讨其有效范围，本项目是对于程序正确性的自动证明及可证明语言的设计开发方面的创新的和指导性的基础研究，研究还将确立弱终止性的形式自动证明方法。