Overview.tex

\section{简介}

定理证明是一种非常重要的形式化技术，广泛用于数学定理证明、协议验证和软硬件安全等领域。无论是SAT、QBF、SMT等特定问题的求解器，还是通用的定理证明工具如Coq、Isabelle，都取得了巨大的理论进展和实践成就。定理证明器和计算代数系统、符号计算系统等也密切相关。

$\lambda$演算是由Church、Kleene等人在20世纪30年代提出的形式系统。$\lambda$演算及其扩展是函数式程序语言的基础，并且广泛用于并发理论、类型论等领域的研究中。

本文包括$\lambda$演算、逻辑与定理证明的基础知识，重点论述类型论与逻辑逻辑证明的联系，并简单介绍定理证明辅助工具Coq的原理和使用。



数理逻辑中对形式系统的研究有两类方法：语义方法和语法方法。语义方法又称模型论方法，研究命题的语义（即命题的意义和真值）、重言式（永真）、语义后承等。语法方法亦称证明论方法，研究形式推演系统、形式定理等。本文主要从语法的角度阐述$\lambda$表达式类型和逻辑证明的关系，并将介绍它们在语义层面的本质联系。