Z3和coq之间的区别

Question

我想知道如果有人能告诉我Z3和coq之间的区别吗？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这个要求。但似乎coq也有类似于Z3的汽车策略？或者，coq中的证明搜索能力不如Z3强大？

Answer 1

Coq是一个交互式定理证明器（aka proof assistant）。它提供了一种语言来编写数学定义，算法和定理。它还提供了生成机器检查证明的环境。 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试图改变这种情况。