Coq内核的证明技术

如何解决Coq内核的证明技术

Isabelle的内核验证能力基于分辨率以及高阶统一。

Coq的核如何证明定理？

问题来自阅读保尔森的“泛型定理证明者的基础”：

提议类型可能会占用过多空间；并将用Huet的统一程序代替高阶逻辑吗？

解决方法

大多数证明者中有两种技术：“证明”部分（负责构建证明，因为它对于用户而言通常过于繁琐）和“检查”部分（负责验证证明是否正确）格式并匹配给定的定理语句）。在Isabelle和Coq中，内核仅负责“检查”部分。

就Coq而言，按类型命题范式确实用于检查证明。换句话说，证明是归纳构造演算（CIC）的lambda项，其类型与被视为类型的定理陈述进行比较。

,

Coq的核如何证明定理？

如上所述，Coq的核不证明了定理，只有检查了。

该检查通常使用类型检查完成：如果该术语是应用程序，则（递归）检查参数是否具有正确的类型，以及函数返回类型是否与该类型匹配。例如，要证明a + f(b)的类型为nat，您必须检查plus的类型为nat -> nat -> nat，f的类型为A -> nat， a的类型为nat，而b的类型为A。

证明必须由用户构造。 proof 本身是一个 lambda术语。定理命题是λ项的类型。

由于直接创建正确的lambda术语可能很困难，因此Coq不会强迫用户一次性编写整个术语。相反，您可以手动或用tactics来填充术语中的“漏洞”。战术是一些小程序，它们试图填写证明（可能是正确的……）。

构造完整个lambda项后，Coq会通过检查lambda项确实具有人们希望证明的命题类型来对证明进行检验。