定理证明理论与应用专题前言

<正>随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.近年来,定理证明已经逐步用于越来越多的软件、硬件系统验证，这一方面为软硬件系统的安全性保障提供了新的有力工具,另一方面也成为定理证明技术发展的有利契机.目前,定理证明的规模化问题、定理证明工具本身的底层逻辑理论问题、适应于定理证明方案的程序验证理论问题等变得越来越重要,对于数学分析、离散数学、概率等基础定理证明库或求解方案的需求也越来越迫切.