z3 - 定义自定义量词

Question

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

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

p 是 i 类型的谓词。有没有办法在 Z3 中定义这样的量词？

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

谢谢!

Answer 1

在 Z3 中没有直接定义此类绑定(bind)器的方法。 Z3 基于经典的简单排序的一阶逻辑，其中唯一的绑定(bind)器是通用和外部量化。特别是，Z3 不允许您直接编写 lambda 表达式。使用包含嵌套绑定(bind)器的 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 等)的证明义务。