面向下一代定理证明技术的高阶重写元理论及其自动证明方法研究

Intractive Theorem Proving (ITP) is playing a more and more important role in fields like mathmatical theories formalization and trustwarthy software verification. Enhancing the expressivity and reasoning power of ITP is a world wide focus. Higher-Order Rewriting (HOR) are the models by introducing algebraic rewriting into the classic type theory model, which combine the computational diagrams of functional programming, equality reasoning and rewriting computation. Extended with HOR, current ITPs can be improved on their expressivities, reasoning power and developing efficiencies. Building its meta-theories is prerequisite for any HOR to be feally usuful. However, there still several mete-theoritical problems kept open for HOR, whose hardness originate from their intrinsic complexities...This research has two goals. The first goal is developping the meta-theories for HOR in systematical way, where meta-properties like strong normalization, confluence and decidability of type checking are focused, and taking as the long-term goals building the meta-theory foundation for next generation kernal of ITP. The second goal is developping the proof automation methods to further improve the ease of usability of ITP...Building meta-theories for HOR are well known cutting-edge and challanging problems. The research on the proof automation of meta-theories is the continuance of the pioneering research conducted by the members of our team.

交互式定理证明在数学理论形式化、可信软件研究等方面正在发挥越来越重要的作用。进一步增强其表达和推理能力是当前学术研究热点。高阶重写是在经典类型论模型中引入代数重写所得到的新模型，它融合了函数式编程、等式推理及重写等计算范式，以其为内核能显著提高定理证明器的表示能力、推理能力和应用开发效率。建立其元理论是高阶重写应用的前提，但因其固有的复杂性，迄今仍有不少问题属于学术界的开放问题。..本课题有两个目标，一是系统研究高阶重写模型的元理论性质，包括强正规化性质、汇合性、类型检查可判定性等，最终为下一代交互式定理证明器内核建立系统的元理论基础。二是探索元理论分析的自动化方法，进一步增强定理证明工具易用性。..高阶重写的元理论问题公认具有前沿性和挑战性，元理论分析自动化是课题组成员所做开创性研究的延续，研究成果将为定理证明基础理论研究和应用推广产生积极的推动作用。

现代代数方法在交互式定理证明（ITPs）领域具有很大的发展潜力，类型论和等词理论融合是ITPs发展的一个趋势。课题以定理证明理论和可信软件需求为导向，以将代数方法引入计算机科学为线索，着眼于回答两类问题：代数方法在哪些方面可以增强定理证明，如何将一个有前景的技术真正实用化。为此，针对高阶重写系统的理论空白，解决了若干重要的元理论问题。主要贡献：..高阶重写强正规化性质分析方法研究，通过引入可计算性路径序，首次得到了依赖类型重写系统强正规化性质的一种机械化证明方法（DCPO）。所提方法采用了提升技术，提供了一种解决该类问题的共性框架。通过引入基于位置的抽象，提出正规重写模型，给出一种可用于带等词扩展的重写的汇合性分析方法。一阶和高阶重写的汇合性分析方法研究，发展了递减图技术，提出了若干分别适用于非终止非左线性系统、分层重写系统等的汇合性证明方法。通过构造语义模型，证明了CoqMTU的类型检查可判定性，完成了该理论的正确性证明。在逻辑框架、基于重写和定理证明的建模验证等方面也取得了若干进展。..课题的贡献在于，进一步将代数方法引入定理证明理论，增强其建模及等词推理能力。通过解决新模型的元理论问题，提供模型工具化所需的支撑技术，为新模型发展为现实可用技术扫清了关键障碍。具体理论开发中，进一步推广了可计算性归约序、递减图等技术，深化了对这些技术潜力和应用方法的认识，丰富了处理强正规化性质和汇合性等经典元理论问题的工具集。这些工作对增强定理证明技术尤其是高阶代数理论在其中的应用具有明显意义。..课题选题和技术路线具有前瞻性和先进性，课题关注代数方法在软件理论及工程中的应用，探索双方结合的新的可能性，解决了其中的一些对技术实用化至关重要的理论问题，对建立高阶代数系统可重用的一般理论框架做了探索。在可计算性归约序和递减图技术的应用上取得了连续成果，形成了研究特色。所研究的模型融合了代数方法、程序模型和逻辑演绎，符合定理证明技术发展规律，体现了计算机科学和数学科学交叉融合、相互促进的优势，也形成了研究特色。..主要研究结果发表在TCS、CSL、TCLA和RTA等软件理论的主流期刊和会议上。