z3 - Z3和coq的区别

Question

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

Answer 1

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

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