是否有高级API/环境/库来测试某一特定方法（例如启发式算法）在基于一阶逻辑/类型理论生成构造性证明方面的有效性？

我正在寻找一个用户友好的API，能够验证类似于以下公式的证明的正确性：。

如果可能的话，我更倾向于使用独立的库，而不是像Coq/HOL这样的语言的直接接口。

提前感谢！

回答：

一般来说，没有这样的工具。

一阶逻辑是半可判定的。简而言之，这意味着如果存在证明，你总能找到它。如果不存在，你可能会找到一个反驳，或者永远循环试图找到一个。没有系统能为所有一阶逻辑公式提供开箱即用的证明/反驳。

当然，即使存在证明，也无法保证你能快速找到它。因此，在实践中，在合理的时间/资源内找到证明是一个棘手的问题，即使它们确实存在。从理论上讲，如果你愿意等待足够长的时间，你总能做到这一点。

这是理论方面的情况。在实践中，现代SMT求解器可以做很多事情，特别是如果你对软件-硬件验证中实际出现的引理感兴趣，而不是纯粹的数学。例如，你使用的例子可以用SMTLib语言编码为：

(assert (not (forall ((a Int)) (=> (>= a 0) (exists ((b Int)) (> b a))))))(check-sat)

并且可以由z3轻松证明（假设你将上述文本放入名为a.smt2的文件中）：

$ z3 a.smt2unsat

在这里，我们断言了我们想要证明的否定，而z3说unsat不可满足，这意味着原始陈述实际上是一个定理。需要一些努力才能看出对应关系，但这是公认的。此外，如果你的公式不是定理，那么SMT求解器可以给你一个具体的反例；这对于调试或确定虚假性很有用。

这并不意味着z3（或任何其他SMT求解器）会解决你抛给它们的所有公式。特别是对于交替量词，它们可能会给出答案，或者通过说unknown放弃尝试，或者可能永远循环。

毫无疑问，你已经知道解决此类问题的正确工具是像Coq/Hol/Isabelle/ACL2等定理证明器；但你明确寻找的是一键式解决方案。我认为SMT求解器接近你想要的，但要注意它们有我上面提到的固有限制，并且还受到当前启发式和证明引擎集的限制。它们肯定会随着时间的推移而改进，但你永远不会有完全的自动化。

总之，这一切都取决于你的真正目标是什么。对于软件/硬件实际验证任务中出现的问题，SMT求解器会带你走得很远；还有一个额外的好处是它们理解很多“理论”（算术、数组、数据结构，仅举几例）。此外，它们可以很容易地编程，因为大多数求解器在许多高级语言中暴露了高级API，并且大多数编程语言都有使它们易于使用的绑定。

然而，如果你的兴趣在于纯粹的数学，我认为你无法避免半自动化的定理证明世界。试着看看Lean，这是一个现代的、可高度编程的定理证明器。例如，请注意，大多数定理证明器已经带有利用SMT求解器的策略，因此虽然你必须手动编写证明，但有很多自动化工具可以帮助你。