如何设置Coq作为一阶逻辑的定理证明器

Question

据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明助手中使用机器学习或其他启发式方法来自动化证明过程的努力(它们被命名为*hammer?)，其中一些趋势发表在http://ai4reason.org/activities.html上。

我的问题是- Coq能否被配置为与一阶逻辑的E-prover或Z3 prover具有类似功能的FOL定理证明器？如果是，我该如何配置Coq来实现这种用途呢？

Answer 1

如果您想要在Coq证明中自动找到一阶语句的证明，您可以使用Coq锤子的重构策略的标准策略firstorder (见下文)。

如果你想使用Coq来解决tptp格式中出现的问题，有一个工具https://github.com/lukaszcz/tptp2coq可以将一个tptp文件转换成一个Coq文件，然后你可以使用一些自动化的策略来解决目标，但它不会与E-prover或Z3竞争。

还有一个工具，Coq锤子，它会将Coq目标转换为FOL，然后运行FOF验证器，如E，Z3，僵尸。如果那些FOF证明者可以找到证明，Coq hammer将使用证明中使用的引理列表，尝试使用自动策略在Coq中再次查找证明(这称为证明重构)。