我应该如何定义一个封闭的谓词？

Question

我有兴趣证明关于某些假设的陈述的有效性。然而，Z3 似乎默认采用“开放”模型。例如，假设我们假设

富(4)

关于这个陈述，我想表明“在” foo 中的东西是偶数。所以我首先声明 foo

(declare-fun foo (Int) Bool)

接下来，因为我对假设感兴趣。我构造一个含义：

(implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))

最后，因为我对有效性感兴趣，而不是可满足性，所以我想检查这个陈述的否定的不可满足性。

(assert (not (implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))
(check-sat)

然而，Z3 报告说这个说法确实可以满足：

sat
(model 
  (define-fun x!0 () Int
    (- 1))
  (define-fun foo ((x!1 Int)) Bool
    (ite (= x!1 4) true
    (ite (= x!1 (- 1)) true
      true)))
)

我大致了解这里发生了什么，但我不确定如何最好地表达 foo 在我的假设陈述下应该“关闭”。对于这个非常简单的例子，我可以通过告诉 Z3 foo 没有其他成员来做到这一点：

(assert (not (implies (and (foo 4) (not (exists ((x Int)) (and (not (= x 4)) (foo x))))) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))

但是，当我转向更复杂的假设时，似乎很难自动生成公式来定义那些不在 foo.h 中的东西。

我错过了什么愚蠢的东西吗？

Answer 1

当且仅当 x = 4 时，为什么不声明 (foo x)？ 您的第一句话说（在反编译否定之后）：

(assert (foo 4))
(assert (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))

这可以通过函数 foo 来满足，该函数将所有内容都映射到“真”， 并且存在性断言可以使用 x = -1 来满足。 这是标准的一阶语义。

foo 在 4 时最多满足的一种说法是：

(assert (forall ((x Int)) (=> (foo x) (= x 4))))

你也可以说 foo 只在 4 处成立：

(assert (forall ((x Int)) (= (foo x) (= x 4))))