問題タブ [theorem-proving]

誰かがZ3自体でZ3を証明しようとしましたか？

Z3を使用して、Z3が正しいことを証明することさえ可能ですか？

より理論的には、X自体を使用して、ツールXが正しいことを証明することは可能ですか？

GNU Prolog で書かれたトートロジー チェッカーのオープンソース実装を探しています (SWI-Prolog の実装も受け入れられますが、GNU Prolog が推奨されます)。

次のようなクエリでプログラム入力をフィードしたいと思います。

また

もちろん、表記は次のように異なる場合があります。

結果として私が期待するのは、「はい/いいえ」、「等しい/異なる」、「見つかった証明/証明を見つけることができなかった」などのブール値の答えです。

ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/で GNU-Prolog のトートロジー チェッカーを見つけましたが、ライセンスが添付されておらず、Gnu Prolog 算術制約と算術機能を適用する方法の手掛かりがありません論理モデルだけを算術で拡張するため。

• 他の同様のソルバーはありますか?
• モデルを拡張するために算術機能を使用する方法の例。

ありがとう、グレッグ。

PS 算術によると、部分的なサポートを探しています - 提案されたソリューションが古典的なロジックを適切に処理して開く場合、単純なヒューリスティック (gnu-prolog 整数関数の例も歓迎) を使用して手動でコーディングできるいくつかの基本的なケースのみを処理したい-ソースコードは拡張するのに適しています:)。

PPS @larsmansが指摘したように、ゲーデルの不完全性定理によれば、 「すべての」式を証明する方法はありません。そのため、Gnu Prolog プログラムを探しているので、与えられた公理と規則のセットから証明できるものを探しています。そのような公理と規則のセットの例を探しています ;) もちろん、チェッカーは失敗する可能性があります-「いくつかの」ケースで動作することを期待しています:)。- 一方、ゲーデルの完全性定理があります ;)。

Z3 の QBVF ソルバーをいじっていて、存在するアサーションから値を抽出できるかどうか疑問に思っています。つまり、私が次のものを持っているとしましょう：

これは基本的に、「最小」の 16 ビット符号なし値があることを示しています。次に、私は言うことができます：

Z3-3.0 は喜んでこう答えます。

これは本当にクールです。しかし、私がやりたいのは、get-value を介してそのモデルの一部を抽出できるようにすることです。当然のことながら、次のいずれも機能していないようです

いずれの場合も、Z3 は当然、そのような定数はないと不平を言います。(check-sat)呼び出しへの応答によって証明されるように、Z3 がその情報を持っていることは明らかです。get-valueまたは他のメカニズムを介して、存在する値に自動的にアクセスする方法はありますか?

ありがとう..

ListSetCoq標準ライブラリのモジュールを使用しています。証明の条件について推論する方法がわかりません。たとえば、次の証明に問題があります。コンテキストの定義が提供されています。

現在の証明状態にはinr、Aeq_dec仮説としてのが含まれています。inl帰納の基本ケースとのAeq_decが真である帰納ケースを破棄しました。

真であるための唯一の方法はH、真であるa <> x場合set_mem xsです。を取得するためにH、に条件を適用できるはずです。しかし、私はこれを行う方法を理解していません。条件を処理、分解、または適用するにはどうすればよいですか？a <> xset_mem xs

幅優先探索を命題定理証明の戦略としてどのように使用できますか (明確な問題の定式化がわかりません。各状態で使用可能なアクションは何か、状態とは何か)。

ネットのいたるところで説明を探していました。すべてのドキュメントで BFS について言及されていますが、アルゴリズムを提供しているものはありません。

ご協力ありがとうございました

パターンマッチング（たとえば、Prolog、MLファミリー言語、およびさまざまなエキスパートシステムシェルに見られる）は、通常、厳密な順序で要素ごとにクエリをデータと照合することによって機能します。

ただし、自動定理証明のようなドメインでは、一部の演算子が結合法則と可換性であることを考慮する必要があります。データがあるとします

とクエリ

表面構文で見ると、これは一致しませんが、論理的には結合法則であるため、$Xバインドされたものと一致する必要があります。A or Bor

この種のことを行う既存のシステムは、どの言語でもありますか？

Prolog の実装について述べている SATCHMO 定理証明者に関するかなりの数の論文を見てきました。しかし、私がこれまでに見つけた唯一のソース コードの実装は本にあり、それは非常に限られており、ルールがどのように評価され、起動されるかの例を示すことのみを目的としていました。Prolog で SATCHMO の優れたオープン ソース実装を見た人はいますか?

Satchmo と呼ばれる Django 用の Python 言語ツールについて言及しているのではないことに注意してください。タグに Satchmo を含めなかったのは、そのタグの主要な定義として Stack Overflow が示しているものだからです。

私はagdaを学ぼうとしています。しかし、問題が発生しました。Agda wiki で見つけたすべてのチュートリアルは、私には複雑すぎて、プログラミングのさまざまな側面をカバーしています。agda の 3 つのチュートリアルを並行して読んだ後、簡単な証明を書くことができましたが、実際のアルゴリズムの正確さのためにそれを使用するにはまだ十分な知識がありません。

このテーマに関するチュートリアルをお勧めできますか? Learn Yourself a Haskell に似ていますが、Agda 用です。

アルゴリズムを書くとき、私は通常コメントに不変条件を書き留めます。

たとえば、1つの関数が順序付きリストを返し、もう1つの関数がリストが順序付けられることを期待する場合があります。
定理証明が存在することは知っていますが、使用した経験はありません。

また、スマートコンパイラ[sic！]は、それらを利用してプログラムを最適化できると思います。
それで、不変条件を書き留めて、コンパイラーにそれらをチェックさせることは可能ですか？