問題タブ [theorem-proving]

定理証明ツールz3は、数式を解くのにかなりの時間がかかります。これは、簡単に処理できるはずです。これをよりよく理解し、おそらくz3への入力を最適化するために、z3が解決プロセスの一部として生成する内部制約を確認したいと思いました。コマンドラインからz3を使用する場合、バックエンドソルバー用にz3が生成する数式を出力するにはどうすればよいですか？

forallを使用せずに全称記号とdeclare-constを使用することに混乱があります

私はこのように書くことができます：

Z3を使用すると、この2つのケースでInt型のすべての可能な値が調査されます。では、違いは何ですか？本当にdeclare-constを使用して、forall数量詞を削除できますか？

私は、算術、数量詞、平等の理論を組み合わせたZ3を実験しています。これはあまり効率的ではないようです。実際、可能な場合は、数量詞をすべてのインスタンス化された地上インスタンスに置き換える方が効率的であるようです。f次の例を考えてみましょう。この例では、sortの2つの引数を取りObj、解釈されたsortを返す関数の一意の名前の公理をエンコードしましたS。この公理は、引数の各一意のリストがf一意のオブジェクトを返すことを示しています。

これはロジックでそのような公理を定義する標準的な方法ですが、このように実装すると計算コストが非常に高くなります。これには4つの定量化された変数が含まれ、それぞれが8つの値を持つことができます。これは、これが8^4 = 4096平等になることを意味します。これを証明するには、Z30.69sと2016年の数量詞のインスタンス化が必要です。この式のインスタンスを生成する簡単なスクリプトを書くと、次のようになります。

これらの公理を生成するのに0.002秒かかり、Z3でそれを証明するのにさらに0.01秒（またはそれ以下）かかります。定義域内のオブジェクト、または関数への引数の数をf増やすと、この違いは急速に増加し、定量化されたケースはすぐに実行不可能になります。

これは私に不思議に思います：私たちが有界ドメインを持っているとき、なぜ私たちはそもそもZ3で数量詞を使うのでしょうか？SMTはヒューリスティックを使用して解決策を見つけることを知っていますが、接地されたインスタンスをSMTにフィードする単純なドメイン固有のグラウンダーと効率的に競合することはできないと感じています。これはSATの解決にすぎません。私の直感は正しいですか？

Microsoft Research が開発した SMT ソルバーである Z3 を使用して、一次理論の可能なすべてのモデルを取得しようとしています。最小限の作業例を次に示します。

この命題のケースでは、満足のいく代入が 2 つあります。f->trueとf->falseです。Z3 (および一般的な SMT ソルバー) は、満足のいくモデルを 1 つだけ見つけようとするため、すべての解を直接見つけることはできません。ここでという便利なコマンドを見つけました(next-sat)が、Z3 の最新バージョンではこれがサポートされなくなったようです。これは私にとっては少し残念なことですが、一般的にこのコマンドは非常に便利だと思います。これを行う別の方法はありますか？

スコーレム化を使用して、私の理論で存在記号を削除しようとしています。これは、存在記号を、存在記号のスコープ内の全称記号変数によってパラメーター化された関数に置き換えることを意味します。

ここで、Z3でこれを行う方法の説明を見つけましたが、まだ問題があります。次の2つの関数を想定します。

真であるような整数、すなわち。f2が存在するので、それは真であるはずだと私は信じています。存在記号の式に定数を導入することにより、スコーレム化を適用します。t(f1 t)t=3

次に、存在記号を含む式は次のように書き直されます。

これは機能しません。つまり、定数cの値は3ではありません。定数に解釈を与えていないためだと思います。これcを追加すると正常に機能するためです(assert (= c 3))が、これにより存在記号の概念全体が失われます。数量詞。これが機能するように、あまり明確に解釈しない方法はありcますか？

C APIを使用してCraig補間関数を生成しようとしていますが、間違った結果が得られます。ただし、同じ問題をZ3_write_interpolation_problemを介してファイルにダンプし、iZ3を呼び出すと、期待される補間が得られます。

同じ結果を再現できるようにコードを添付します。z34.1を使用しています

次のコマンドを使用して実行可能ファイルを生成します。

g ++-fopenmp-o補間補間.c-I/home / jorge / Systems / z3 / include -I / home / jorge / Systems / z3 / iz3 / include -L / home / jorge / Systems / z3 / lib -L ​​/ home / jorge / Systems / z3 / iz3 / lib -L ​​/ home / jorge / Systems / libfoci-1.1 -lz3 -liz3 -lfoci

制約は基本的に次のとおりであることに注意してください。

A =（x=0およびx1=x0+2およびx2=x1 + 2）、

およびB=（x2> 10）

明らかに不満です。さらに、共通の変数がx2だけであることも簡単にわかります。したがって、有効な内挿にはx2しか含めることができません。

実行可能ファイル./interpolationを実行すると、ナンセンス補間が得られます。

ただし、「iz3 tmp.smt」（tmp.smtはZ3_write_interpolation_problemを使用して生成されたファイル）を実行すると、有効な補間が得られます。

unsat補間：（<= x2 10）

これはバグですか？または、Z3_interpolateを呼び出すときに、いくつかの重要な前提条件が欠落していますか？

PSCAPIでiZ3を使用した例は見つかりませんでした。

乾杯、ホルヘ

配列の長さをモデル化する必要があります。だから私は関数を宣言します

同時に、を使用していくつかのマクロを定義したいと思いますdefine-fun。

ただし、Z3で少しテストしたところ、同じソースファイルに存在できないdefine-funようです。declare-fun

次のようなこのコードは正常に機能します。

（src： http: //rise4fun.com/Z3/jRzs）

ただし、以下は、LEN挿入された場所に関係なく、エラーが発生します。

（src： http: //rise4fun.com/Z3/HdEy）

誰かがこれを回避する方法を知っていますか？

私は非常に単純なOTTERの入力ファイルを書いています：

私は検索のためにこの出力を取得します：

なぜOTTERは推測しないのCauses($c2,$c1)ですか？

編集：角かっこをから削除しましたが、[Nipah(x) & Encephalitis(x)]機能しました。なぜこれが重要なのですか？

一次理論に関する事実を証明するために Z3 の使用を最適化する実験を行っています。現在、私は Python で 1 次理論を指定し、そこで量化子を接地し、すべての節を証明目標の否定とともに Z3 に送信します。私は、結果を最適化できることを望む次の考えを持っています:証明の目標に関連する理論の数式のみを Z3 に送りたいです。この概念について詳しくは説明しませんが、直感は単純だと思います。私の理論は数式の結合であり、証明目標の真理値に影響を与える可能性のある結合のみを送信したいのです。

私の質問は次のとおりです。これは効率の改善につながるのでしょうか、それとも Z3 はすでに同様の方法を使用していますか? Z3 は、最後のアサーションが証明の目標であると常に想定しているとは思わないため、これを最適化する方法がないため、そうではないと思います。

私は Coq を初めて使用し、Ruth と Ryan のサンプル レンマを試しています。自然演繹法を使用した証明は非常に簡単で、これが Coq を使用して証明したいことです。

私はライン 3 で立ち往生していassume pます。

自然演繹から Coq キーワードへの 1 対 1 のマッピングがあるかどうか誰か教えてもらえますか?