6

我们知道，我们可以通过说来证明定理的有效性：

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
assert ( forall (x,y) . Demorgan(x,y) )

或者，我们可以通过以下方式消除 forall 量词： 

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
( assert (not  Demorgan(x,y) ) )

所以如果它返回 unsat，那么我们可以说上面的公式是有效的。

现在我想用这个想法从以下断言中消除 forall 量词： 

assert ( exists x1,x2,x3 st .( forall y . formula1(x1,y) iff
                                          formula2(x2,y) iff
                                          formula3(x3,y) ) )

那么在 Z3 中有什么方法（使用 C++ API 或 SMT-LIB2.0）我可以断言如下内容：

assert (exists x1,x2,x3 st. ( and ((not ( formula1(x1,y) iff formula2(x2,y) )) == unsat)
                                  ((not ( formula2(x2,y) iff formula3(x3,y) )) == unsat)))
4

1 回答 1

10

是的，当我们可以通过证明其否定不可满足来证明公式的有效性时。例如，要证明那Forall X. F(X)是有效的，我们只需要证明那not (Forall X. F(X))是不可满足的。该公式not (Forall X. F(X))等价于(Exists X. not F(X))。该公式(Exists X. not F(X))等效于not F(X)将绑定变量X替换为新常数的公式X。Equisatisfiable，我的意思是第一个是可满足的，如果第二个是可满足的。这个删除存在量词的步骤通常称为skolemization。请注意，最后两个公式不等价。例如，考虑{ X -> 2 }分配X给的解释2。公式Exists X. not (X = 2)在这种解释中仍然评估为真，因为我们可以选择X是3。另一方面，not (X = 2)在这种解释中，公式的计算结果为假。我们通常使用术语量词消除过程来表示给定公式F产生等效的无量词公式的过程F'。因此，skolemization 不被视为量词消除过程，因为结果不是等效公式。

话虽如此，我们不必手动应用 skolemization。Z3可以为我们做到。这是一个示例（也可在此处在线获得）。

(declare-sort S)
(declare-fun F (S) Bool)
(declare-fun G (S) Bool)
(define-fun Conjecture () Bool 
    (forall ((x S)) (= (and (F x) (G x)) (not (or (not (F x)) (not (G x)))))))
(assert (not Conjecture))
(check-sat)

现在，让我们考虑一个形式为 的公式Exists X. Forall Y. F(X, Y)。为了证明这个公式的有效性，我们可以证明否定not Exists X. Forall Y. F(X, Y)是不可满足的。否定等价于Forall X. Exists Y. not F(X, Y)。现在，如果对这个公式应用 skolemization，我们得到Forall X. not F(X, Y(X)). 在这种情况下，绑定变量Y被替换为Y(X)，其中Y是结果公式中的新函数符号。直觉是该函数Y是“选择函数”。对于每一个X，我们可以选择不同的值来满足公式F。Z3 会自动为我们执行所有这些步骤。我们不需要手动应用 skolemization。但是，在这种情况下，生成的公式通常更难求解，因为它在 skolemization 步骤之后包含一个全称量词。

于 2013-05-27T16:11:39.027 回答