定理证明者中的归纳证明（Z3、Vampire、具有 TPTP 语法）

Question

我正在使用 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

Answer 1

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

--mode portfolio --schedule induction

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

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