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))、バインドされた変数が新しい定数に置き換えられた式と同等です。同等に満足できるとは、最初のものは満足できるが、2 番目のものは満足できるということです。存在量指定子を削除するこのステップは、通常、スコーレム化と呼ばれます。これらの最後の 2 つの式は同等ではないことに注意してください。たとえば、に割り当てる解釈を考えてみましょう。式not F(X)XX{ X -> 2 }X2Exists X. not (X = 2)を選択できるため、この解釈では依然として true と評価されXます3。一方、not (X = 2)この解釈では、数式は false と評価されます。私たちは通常、与えられた式が同等の量指定子のない式を生成する手順に対して、量指定子除去手順という用語を使用します。そのため、スコーレム化は、結果が同等の式ではないため、量指定子の削除手順とは見なされません。FF'

そうは言っても、手動で 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)です。さて、この式にスコーレム化を適用すると、 が得られForall X. not F(X, Y(X))ます。この場合、バインドされた変数Yは に置き換えられましたY(X)。ここで、Yは結果の式の新しい関数記号です。直感的には、その機能Yは「選択機能」です。それぞれについてX、式を満たすために異なる値を選択できますF。Z3 はこれらすべてのステップを自動的に実行します。スコレム化を手動で適用する必要はありません。ただし、この場合、結果の式は通常、スコーレム化ステップの後に全称量指定子が含まれているため、解くのが難しくなります。

于 2013-05-27T16:11:39.027 に答える