z3 - 定义自定义量词

Question

我试图让 Z3 验证一些在符号中使用迭代最大值的正式证明。例如，对于 fa 函数 (↑i: 0 ≤ i < N: f(i)) 指定 f 在应用于 0 和 N 之间的值时的最大值。它可以很好地公理化为：

(↑i: p(i): f(i)) ≤  x <=> (∀i: p(i): f(i) ≤ x)

在 i 的类型上使用 pa 谓词。有没有办法在 Z3 中定义这样的量词？

制定我的证明非常方便，所以我想尽可能地接近这个定义。

谢谢！

Answer 1

在 Z3 中没有直接定义此类绑定器的方法。Z3 基于经典的简单排序一阶逻辑，其中唯一的绑定器是通用和外部量化。特别是，Z3 不允许您直接编写 lambda 表达式。使用包含嵌套绑定器的 Z3 证明定理的一种方法是首先应用 lambda-lifting，然后尝试证明得到的一阶公式。

在您的示例中，您想定义一个常量 max_p_f。具有以下属性：

forall i: p(i) => max_p_f >= f(i)
(exists i: p(i) & max_p_f = f(i)) or (forall i . not p(i))

说（假设在域上定义了上界等）您必须为要应用 max 函数的每个 p,f 组合创建常量。

定义这样的函数是高阶逻辑证明助手的标准。Isabelle 定理证明器在将证明义务映射到一阶后端（E、Vampire、Z3 等）时应用类似于上述的转换。