定义自定义量词

Question

我试图让 Z3 验证一些在符号中使用迭代最大值的正式证明。例如，对于 f，函数 (↑i:  0 ≤ i

(↑i: p(i): f(i))  ≤  x      (∀i:  p(i):  f(i) ≤ x)

其中 p 是 i 类型的谓词。有没有办法在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 等）的证明义务。