Z3 には、prove()2 つの式の等価性を証明できる方法があります。
prove()ただし、この方法の技術文書は見つかりません。prove()裏で使われている「同等」の定義とは？それは「部分的等価性」（「回帰検証」論文で提案されている）ですか、それとももっと強力なものですか？
「部分的等価性」は、同じ入力が与えられた場合に 2 つの式が等価であることを保証するものであり、同じ出力を生成します。
1 に答える
4
「回帰検証」では、プログラムの新しいバージョンが以前のものと同じ出力を生成するかどうかを確認しています。つまり、プログラムの等価性をチェックするためのアプローチです。このアプローチでは、Z3 などの定理証明器 (SMT ソルバー) が使用されます。そうは言っても、プログラムの等価性と一次論理の式の等価性を混同すべきではありません。Z3 は一次論理式を処理します。一階論理には明確に定義されたセマンティクスがあります。重要な概念は満足可能性です。たとえば、orを truep or qに代入して true にすることができるため、式は充足可能です。反面、物足りない。追加情報はpqp and (not p)Z3 チュートリアルのこのセクション。
Z3 API は、一次式の充足可能性をチェックするための手順を提供します。Z3 Python インターフェイスにはproveプロシージャがあります。否定が満たされないことを示すことによって、式が有効であることを示します。これは、Z3 API の上に構築された単純な関数です。ここにそのドキュメントへのリンクがあります。ドキュメントは、コード内の PyDoc 注釈から自動的に生成されました。
は式が有効prove(F)かどうかをチェックしていることに注意してください。Fしたがって、 を使用して、2 つの 1 次式とが等しいprove(F == G)ことを証明することができます。つまり、本質的に が有効な式であることを示しています。FGF iff G
于 2012-12-26T17:12:28.010 に答える