据我了解，那么Coq内置了第一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但是Coq不是定理证明者，Coq是证明助手，这意味着用户需要提供一些提示，即Coq在每个步骤中应选择哪些规则/策略。存在更多的矿石，以免组合启发式策略，但Coq仍然不能证明。我听说过在证明助手中使用机器学习或其他启发式方法来自动执行证明过程的努力（它们被称为* hammer？），其中一些趋势发表在http://ai4reason.org/activities.html中。
我的问题是-是否可以将Coq配置为用作FOL定理证明者，其能力与E-prover或Z3证明者的一阶逻辑类似？而且-如果是的话-我该如何配置Coq以进行此类使用？
如果要在Coq证明中自动找到一阶陈述的证明，则可以使用Coq锤的重构策略的标准策略一阶（请参见下文）。
[如果您想使用Coq解决tptp格式的问题，可以使用此工具https://github.com/lukaszcz/tptp2coq将tptp文件转换为Coq文件，然后您可以使用一些自动化策略来解决目标，但是它将不能与E-prover或Z3竞争。
还有一个工具Coq锤，它将Coq目标转换为FOL，然后运行FOF证明，例如E，Vampire，Z3。如果那些FOF证明者可以找到证明，则Coq锤将使用证明中使用的引理列表来尝试使用自动策略在Coq中再次找到证明（这称为证明重构）。