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

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

项目编号： No.61272002

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 荔建琦

作者单位： 清华大学

项目金额： 60万元

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

中文关键词： 高阶重写系统元理论；强正规化性质；可计算性路径序；汇合性；递减图技术

英文摘要： 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 p

英文关键词： meta-theories of higher-order rewriting systems；strong normalization；computability path ordering；confluence；decreasing diagrams