Z3和coq的区别

Posted 2023-02-25

【中文标题】Z3和coq的区别

【英文标题】：Difference between Z3 and coq

【发布时间】：2012-07-16 21:51:52

【问题描述】：

我想知道是否有人可以告诉我Z3和coq之间的区别？在我看来，coq 是一个证明助手，因为它要求用户填写证明步骤，而 Z3 没有这个要求。但似乎 coq 也有类似于 Z3 的自动战术？还是说coq的证明搜索能力没有Z3强大？

【问题讨论】：

交叉发布：qr.ae/TUrnvY

【参考方案1】：

Coq 是一个交互式定理证明器（又名证明助手）。它提供了一种语言来编写数学定义、算法和定理。它还提供了一个用于生成机器检查校样的环境。 Coq 已被用于形式化数学定理，并提供编程语言的语义。今天，我们可以在 POPL 找到许多使用 Coq 的论文。一些人声称，在未来，像 Coq 这样的系统将被数学家广泛使用。 article 对数学中的形式证明有一个令人信服的论据。最近，Georges Gonthier 使用 Coq 创建了四色定理的可调查证明。 Coq 的可信核心很小，并且提供了很高的保证。

Z3 是一个SMT（可满足性模理论）求解器。它的语言是许多排序的一阶逻辑+理论，例如算术、位向量、数据类型、数组等。这种语言不像 Coq 中使用的那样具有表达力。 Z3 也不支持像 Coq 这样的证明管理。 Z3主要用于软件测试和验证。它还可用于解决约束、规划问题、谜题等。 寻找可满足公式的模型（即解决方案）非常重要。 article 描述了 Microsoft 和其他地方的许多 Z3 应用程序。 Z3 本质上是一个自动定理证明器。在Z3中，战术用于指定domain specific strategies。也就是说，针对特定应用领域中的问题的定制求解器。 Z3 可以生成可以独立检查的证明/证书。然而，证明生成并不是 Z3 项目的主要关注点。此外，许多模块不支持证明生成，并且在用户请求生成证明时必须禁用。 Z3 也被集成到了证明助手中，例如Isabelle，还有一些正在努力将 Z3 集成到 Coq 中。这个想法是两全其美：非常富有表现力的语言和非常好的自动化。 Z3 也可以被视为一个可以嵌入到更大应用程序中的逻辑推理引擎。实际上，到目前为止，每个 Z3 应用程序都是如此。最终用户不直接使用 Z3。它隐藏在 Isabelle、Pex、VCC 等工具中。Z3 的 new Python front-end 试图改变这一点。