问题标签 [coq-plugin]

据我了解，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 以供此类使用？

我目前正在开发一个 ocaml 程序，该程序将使用 coq api 来提取有关证明及其目标的信息。为此，当使用“refine ?[name]”或其他命名目标的策略时，我想提取给目标的名称。到目前为止，我正在获得当前的目标，使用我当前的证明状态来提取它们，如下所示

使用这种方法，我可以提取目标的 ID，但不能提取它们的名称。

有没有可能提取名称？