私は2つの式F1とF2を持っています。これらの 2 つの式は、いくつかの「一時的」(または私は「フリー」と呼んでいます) 変数を除いて、ほとんどの変数を共有しています。
ここで F1 == F2 を証明したいのですが、Z3 の probe() メソッドは常にすべての変数を考慮します。これらの「自由な」変数を無視し、本当に気にかけている変数のリストだけに焦点を当てるように、prove() に指示するにはどうすればよいでしょうか?
つまり、変数のリストへの入力がすべて同じで、出力時に F1 と F2 がこれらすべての変数の値が同じである場合 (「自由な」変数の値に関係なく)、それらを「等価」と見なします。
この問題は以前に他の研究で解決されたと思いますが、どこで情報を探すべきかわかりません.
本当にありがとう。
存在量指定子を使用して、「一時的」/「自由」変数をキャプチャできます。たとえば、次の例では、式FとGは同等ではありません。
x, y, z, w = Ints('x y z w')
F = And(x >= y, y >= z)
G = And(x > z - 1, w < z)
prove(F == G)
スクリプトは反例を生成し[z = 0, y = -1, x = 0, w = -1]ます。とを「一時的な」変数と見なすyと、次の証明を試みることができます。w
prove(Exists([y], F) == Exists([w], G))
さて、Z3が戻ってきprovedます。Z3 は本質的に、すべてのxとzに対して、真になる ayがFある場合にのみ真になる a があるwことを示していGます。
これが完全な例です。
注意: 量指定子を追加すると、Z3 の問題がさらに難しくなります。unknown数量詞を含む問題で返されることがあります。
どうやらコメントできないので、別の答えを追加する必要があります。特定の変数を「無視」するプロセスは、通常、「射影」または「忘却」と呼ばれます。私は命題論理を超えた文脈ではそれをよく知らないが、直接存在記号が可能である場合（レオが説明した）、それは概念的にそれを行う最も簡単な方法である。