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主要用于软件测试和验证.它还可以用于解决约束,计划问题,谜题等.在寻找可满足公式的模型(即解决方案)时非常重视.该文章介绍了在微软内部和其他地方的许多Z3应用.Z3本质上是一个自动定理证明器.在Z3中,策略用于指定特定于域的策略.也就是说,针对特定应用领域中的问题的自定义解算器.Z3可以生成可以独立检查的样张/证书.但是,证明生成不是Z3项目的主要关注点.此外,许多模块不支持证明生成,并且在用户请求证明生成时必须禁用.Z3也已经集成在Isabelle等证明助手中,有些正在努力将Z3整合到Coq中.我们的想法是拥有两全其美:非常富有表现力的语言和非常好的自动化.Z3也可以被视为可以嵌入更大应用程序的逻辑推理引擎.实际上,到目前为止每个Z3应用程序都是如此.最终用户不直接使用Z3.它隐藏在Isabelle,Pex,VCC等工具中.Z3的新Python前端试图改变它.