z3 - Z3の反例出力

Question

Z3の数式が不飽和で、（get-proof）が指定されている場合、それが何であるかについての情報が見つからない出力があります。それに関するドキュメントはどこにありますか？

私にはまったく読めないようですが、これを入力として受け取るツールはありますか？

乾杯、マット

Answer 1

Z3によって生成された「証拠」は人間が消費するためのものではありません。フォーマットの古いバージョンは、論文で説明されています：Proofs and Refutations、およびZ3。このz3_api.hファイルには、各証明ルールの長い説明が含まれています。証明ルール識別子は。で始まりZ3_OP_PRます。Z3プルーフオブジェクトを使用する2つのアプリケーションを知っています。次のペーパーには多くの例が含まれており、プルーフオブジェクトの使用方法について説明しています。

1. Isabelle Interactive Theorem Prover：Z3証明は、信頼できるコアを使用してIsabelle内で再構築されます。Sascha Bohmeのホームページで、この作業とZ3プルーフフォーマットを説明するいくつかの論文を見つけることができます。

2. 補間関数の生成

   パッドが言ったように、使用するのunsat-coresははるかに簡単です。