定理证明器中的归纳证明（Z3，Vampire，使用 TPTP 语法）答案

【问题标题】：Inductive proofs in theorem provers (Z3, Vampire, with TPTP syntax)定理证明器中的归纳证明（Z3，Vampire，使用 TPTP 语法）
【发布时间】：2022-08-08 10:52:54
【问题描述】：

我正在使用 TPTP 语法测试一些定理证明器（例如 Z3、Alt-Ergo、Vampire 等）的归纳能力。令我惊讶的是，他们都没有设法证明以下简单的猜想：

tff(t1, type, (fun: $int > $int )).

tff(ax1, axiom, ( 
    ! [A: $int] : (
        $less(A, 1) => (fun(A) = 123)
    )
)).

tff(ax2, axiom, ( 
    ! [A: $int] : (
        $greatereq(A, 1) => (fun(A) = fun($difference(A, 1))) 
    )
)).

tff(conj1, conjecture, ! [A: $int] : ($greatereq(A, 1) => (fun(A) = 123))).

% END OF SYSTEM OUTPUT
% RESULT: SOT_EWCr1V - Z3---4.8.9.0 says Timeout - CPU = 60.09 WC = 35.47 
% OUTPUT: SOT_EWCr1V - Z3---4.8.9.0 says None - CPU = 0 WC = 0

这个猜想可以很容易地通过归纳来证明，但是对于我测试过的绝大多数定理证明者来说似乎并非如此。显然，如果我将域限制为仅一个元素而不是整组整数，则 ATP 会成功，因为它只需要检查一组有限的数字：

tff(t1, type, (fun: $int > $int )).

tff(ax1, axiom, ( 
    ! [A: $int] : (
        $less(A, 1) => (fun(A) = 123)
    )
)).

tff(ax2, axiom, ( 
    ! [A: $int] : (
        $greatereq(A, 1) => (fun(A) = fun($difference(A, 1))) 
    )
)).

tff(conj1, conjecture, ! [A: $int] : ((A = 5) => (fun(A) = 123))).

% END OF SYSTEM OUTPUT
% RESULT: SOT_j9liHr - Z3---4.8.9.0 says Theorem - CPU = 0.00 WC = 0.08 
% OUTPUT: SOT_j9liHr - Z3---4.8.9.0 says Proof - CPU = 0.00 WC = 0.09

这是自动定理证明器的一般限制吗？是否有任何工具在归纳方面表现良好？

PS：您可以使用以下在线工具进行试用：https://tptp.org/cgi-bin/SystemOnTPTP

PS2：TPTP 语法手册可以在这里找到：https://www.tptp.org/TPTP/TR/TPTPTR.shtml

标签： logic z3 smt theorem-proving logic-programming

【解决方案1】：

正如上面评论中指出的，吸血鬼做支持归纳。然而，与其他定理证明者一样，让 Vampire 做你想做的事有时有点棘手。在这种情况下，要让它使用归纳，您必须使用选项运行

--mode portfolio --schedule induction

设置了这些选项后，Vampire 很快就找到了上述证明（在我的机器上为 0.04 秒）

TPTP 网站不允许您在运行证明者时设置特定选项，因此如果您想尝试上述内容，您必须从 here 获取 Vampire 版本或从源代码构建。

【讨论】：

感谢您的澄清！我也在本地进行了测试，它可以工作（状态：定理）！顺便说一句，您知道其他支持归纳的全自动定理证明器或 SMT 求解器，例如 Vampire？
有几个，CVC4、Zipperposition、Zeno 等。据我所知，吸血鬼是该领域最强大的证明者之一。这里显然需要进一步研究。

【解决方案2】：

这是意料之中的。 SMT 求解器不会进行开箱即用的归纳。您可以通过证明基本情况来“哄”他们进行归纳，然后提出归纳假设并让他们使用量词来证明它；但这通常是徒劳的。 SMT 求解器根本不是进行归纳证明的正确选择。以下是有关此问题的有关 stackoverflow 的一些相关先前讨论：

还有许多其他人。

话虽如此，SMTLib 中的新 define-fun-rec 构造允许递归定义，其证明自然是通过归纳完成的。所以，我预计社区将朝着这个方向发展；随着时间的推移增加归纳能力。例如，参见：

http://lara.epfl.ch/~reynolds/VMCAI2015-ind/smt-ind-RK.pdf

有关如何在 SMT 求解器中正确执行此操作的论文。据我所知，CVC5 已经包含了其中一些想法，但在这一点上期待开箱即用的归纳证明是天真的。（见https://github.com/cvc5/cvc5/issues/1796）

所以，长话短说：不，SMT 求解器不进行归纳。你可以哄他们去做，最近有一些工作增加了更多的功能，但按钮体验不太可能。如果您的目标是推理递归定义，因此您依赖于归纳，那么最好的选择是使用半自动定理证明器，例如 Isabelle、Coq、HOL、HOL-Light、ACLL2、Lean 等。所有这些有强大的设施做感应。此外，它们将 SMT 求解器合并为“策略”，因此您在这个意义上可以两全其美。（即，使用手动策略将您的证明分解为足够简单的子目标，处理归纳等，然后将其余部分发送给 SMT 求解器。）

【讨论】：

SMT 求解器是一种特殊的定理证明器，可提供一键式体验，但它可以处理的理论和问题是有限的。（但在实践中仍然非常有用！）一般意义上的定理证明器（如 Isabelle、ACL2 等）可以处理更复杂的理论和证明，但需要（通常是大量的）用户指导。
此外，区别在于滑动时间尺度。对于 2000 年初的人来说，今天的 SMT 求解器看起来相当神奇。随着时间的推移，他们变得更有能力自己证明更多的定理；但是他们可以处理的内容存在理论上的限制。另一方面，只要您愿意投入工作，手动定理证明器就可以建立任何数学定理。（这可能相当可观。）
我相信 Isabelle 可以阅读 TPTP，尽管我不是专家。（使用标签 Isabelle 提出一个单独的问题。）另请参见此处：isabelle.in.tum.de/website-Isabelle2012/dist/library/HOL/TPTP/…。最终答案实际上取决于您的确切目标是什么，但如果您使用特定的定理证明器，最好使用它的母语；因为使用任何其他语言（TPTP 或其他语言）提出问题将导致“迷失翻译”问题。即，您的经验将仅限于该翻译的能力。
我之前包含的链接似乎有一个 TPTP -> HOL 解析器。我从来没有使用过它。不知何故，这对你不起作用？
对于任何归纳证明，您都必须做一些工作来设置它。大多数证明者不会自动尝试。（我认为 ACL2 可能是一个例外，但即便如此，您也必须引导它完成它。）所以，不，我认为您没有遗漏任何东西。只是在最先进的定理证明中，您的期望与现实不符。