z3 - 我们需要添加哪些额外的公理，以便 Z3 可以验证递归程序的可满足性？

Question

正如我们 know Z3 对重复有限制。有什么办法可以得到以下程序的结果吗？什么将附加方程帮助 z3 得到结果？

    from z3 import *
    ackermann=Function('ackermann',IntSort(),IntSort(),IntSort())
    m=Int('m')
    n=Int('n')
    s=Solver()
    s.add(ForAll([n,m],Implies(And(n>=0,m>=0),ackermann(m,n) == If(m!=0,If(n!=0,ackermann(m - 1,ackermann(m,n - 1)),If(n==0,ackermann(m - 1,1),If(m==0,n + 1,0))),If(m==0,n + 1,0)))))
    s.add(n>=0)
    s.add(m>=0)
    s.add(Not(Implies(ackermann(m,n)>=0,ackermann(m+1,0)>=0)))
    s.check()

Answer 1

对于像阿克曼函数这样的嵌套递归定义，我认为您无法说服 Z3(或任何其他 SMT 求解器)实际进行任何有趣的证明。此类属性需要巧妙的归纳论证，而 SMT 求解器并不是此类验证的合适工具。 Isabelle、HOL、Coq 等定理证明器是更好的选择。

话虽如此，在 SMT 中建立递归函数属性的基本方法是将归纳假设逐字编码为量化公理，并在电子匹配时安排您想要证明的属性与该公理精确对齐引擎启动，因此它可以“正确地”实例化量词。我在这里将单词 correctly 放在引号中，因为匹配引擎将继续并继续以非生产性方式实例化公理，尤其是对于像 Ackermann 的函数。另一方面，定理证明者可以精确地控制证明结构，因此您可以明确地引导证明者通过证明搜索空间。

这是一个您可以查看的示例:list concat in z3它正在使用 SMT-Lib 接口(interface)对比您的目标简单得多的归纳属性进行归纳证明。虽然扩展它来处理您的特定示例并不容易，但它可能会提供一些关于如何处理它的见解。

在 Z3 的特殊情况下，您还可以利用其使用 PDR 算法的定点推理引擎来回答有关某些递归函数的查询。参见 http://rise4fun.com/z3/tutorialcontent/fixedpoints#h22示例展示了如何将 McCarthy 著名的 91 函数建模为一个有趣的案例研究。