3

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

我的问题是——能否将 Coq 配置为用作 FOL 定理证明器，其容量与一阶逻辑的 E-prover 或 Z3 证明器类似？并且 - 如果是的话 - 我如何配置 Coq 以供此类使用？

4

1 回答 1

2

如果您想在 Coq 证明中自动找到一阶语句的证明，您可以使用标准策略一阶，即 Coq 锤子的重建策略（见下文）。

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

还有一个工具，Coq 锤子，它将 Coq 目标转换为 FOL，然后运行 ​​FOF 证明器，例如 E、Vampire、Z3。如果那些 FOF 证明者能够找到一个证明，Coq 锤子将使用证明中使用的引理列表，使用自动策略尝试在 Coq 中再次找到该证明（这称为证明重构）。

于 2020-05-28T08:46:21.213 回答