我想知道有没有人能告诉我Z3和coq之间的区别？ 在我看来，coq是一种证明助手，因为它要求用户填写证明步骤，而Z3则没有这个要求。 但似乎coq也具有类似于Z3的自动策略吗？ 或者说coq中的证明搜索能力不如Z3强大？
1个回答
84
Coq是一款交互式定理证明器（也称为证明助手）。它提供了一种语言来编写数学定义、算法和定理。它还提供了一个环境来生成机器验证的证明。Coq已被用于形式化数学定理，并提供编程语言的语义。今天，我们可以在POPL上找到许多使用Coq的论文。有些人声称，在未来，像Coq这样的系统将被数学家广泛使用。该article对数学中形式化证明有令人信服的论据。最近，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等工具中。新的Python前端为Z3试图改变这一点。
- Leonardo de Moura
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接