消除forall使用不饱和度

Question

我们知道,我们可以通过以下方式证明一个定理的有效性:

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) ) )

因此,如果它返回不饱和,那么我们可以说上面的公式是有效的.

现在我想用这个想法从以下断言中消除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))) 

Answer 1

是的,当我们通过证明其否定是不可满足的来证明公式的有效性时.例如,为了证明这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.如果满足要求,我的意思是如果第二个是第二个,那么第一个是可以满足的.删除存在量词的这一步通常称为skolemization.请注意,最后两个公式不相同.例如,考虑的解释{ X -> 2 }是分配X给2.公式Exists X. not (X = 2)仍计算为true的这种解释,因为我们可以选择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.然而,在这种情况下,所得公式通常难以解决,因为它在斯科化步骤之后包含通用量词.