Z3の反例出力例

Question

Z3の式がunsatであり、（get-proof）が指定されている場合、それが何であるかに関する情報が見つからない出力があります。それに関する文書はどこにありますか？

私にはかなり読めないようですが、これを入力として使用するツールはありますか？

乾杯、 マット

Answer 1

Z3製 "証明" は人間の消費のためではありません。 フォーマットの古いバージョンについては、Proofs and Refutations, and Z3の記事に記載されています。 z3_api.hファイルには、各証明規則の長い説明があります。証明ルール識別子はZ3_OP_PRで始まります。私はZ3証明オブジェクトを使用する2つのアプリケーションを認識しています。以下の論文には多くの例があり、プルーフオブジェクトの使用方法について説明しています。

1- Isabelle Interactive Theorem Prover：Z3プルーフは、信頼できるコアを使用してIsabelle内で再構成されます。パッドはunsat-coresを使用するより簡単です、言ったようにあなたはSascha Bohme's homepage

2 - Generation of interpolants

で、この作品とZ3証明フォーマットを記述するいくつかの論文を見つけることができます。