问题描述
是否有高级 API/环境/库来测试基于一阶逻辑/类型理论生成构造性证明的特定方法（例如启发式算法）的有效性？
我正在尝试找到一种用户友好的 API，可以验证公式证明的正确性，例如：
如果可能，我更喜欢独立库，而不是 Coq/HOL 等语言的直接接口。
提前致谢！
解决方法
一般不会，不会。
一阶逻辑是semi-decidable。简而言之，这意味着如果有证据，你总能找到它。如果没有，你可能会找到一个反驳，或者永远循环试图找到一个反驳。没有系统会为所有一阶逻辑公式提供开箱即用的证明/反驳。
当然，即使有证据，也不能保证你能很快找到。因此，在实践中，在合理的时间/资源中找到证明是一个棘手的问题，即使它们存在。理论上，如果您愿意等待足够长的时间，您总是可以这样做的。
这是它的理论方面。在实践中，现代 SMT 求解器可以做很多事情，特别是如果您对软硬件验证实践中出现的引理感兴趣；而不是纯数学。例如，您使用的示例可以用 SMTLib 语言编码为：
(assert (not (forall ((a Int)) (=> (>= a 0) (exists ((b Int)) (> b a))))))
(check-sat)
并且可以通过例如 z3 轻松证明（假设您将上述文本放在名为 a.smt2 的文件中）：
$ z3 a.smt2
unsat
这里我们断言了我们想要证明的否定，z3 说unsat是可证伪的，这意味着原始陈述实际上是一个定理。需要眯着眼睛才能看到对应关系，但它已经确立。另外，如果你的公式不是定理，那么SMT求解器可以给你一个具体的反例；这有利于调试，或建立虚假。
这不意味着 z3（或任何其他 SMT 求解器）将求解您开箱即用的所有公式。尤其是使用交替量词时，他们可能会想出答案，或者说 unknown 就放弃尝试，或者他们可能会永远循环。
毫无疑问，您已经知道解决此类问题的正确工具是定理证明器，例如 Coq/Hol/Isabelle/ACL2 等；但你明确地在寻找按钮。我认为 SMT 求解器接近您想要的，但需要注意的是，它们既有我上面提到的固有局限性，也受其当前启发式和证明引擎的限制。它们肯定会随着时间的推移而改进，但您永远无法实现完全自动化。
总而言之，这完全取决于您的目标是什么。对于软件/硬件实际验证任务中出现的问题，SMT求解器会带你走得更远；额外的好处是他们理解了很多“理论”。 （算术、数组、数据结构，仅举几例。）此外，它们可以轻松编程，因为大多数求解器公开了许多高级语言中的高级 API，并且大多数编程语言都具有使它们易于使用的绑定使用。
但是，如果您对纯数学感兴趣，我认为您无法避免定理证明的半自动化世界。例如，尝试研究Lean，这是一个高度可编程的现代定理证明器。请注意，大多数定理证明器已经提供了利用 SMT 求解器的策略，因此虽然您必须手动编写证明，但有很多自动化可以帮助您。