問題タブ [theorem-proving]

定理証明者の Isabelle に習い始めたのは 2～3 週間ほど前です。私はまだまったくの初心者で、チュートリアル「Isabelle/HOL でのプログラミングと証明」に取り組みました。

これまでに見つけた行列に関する唯一の助けは、HOL ライブラリのソース コードを調べることでした。

次に、行列に関するプロパティを証明する方法を学びたいと思います。行列のラムダ構文は、私にとってまだ新しいものです。Isabelle で行列を使用するためのチュートリアルまたは基本/中間の例はありますか?

私のイザベル理論では、定数係数を持つ行列があります。

転置行列を計算できます。

私の目には、後者は同等である必要があります

の定義によりtranspose。しかし、これは真実ではありません。ここで私のエラーは何ですか?

ちなみに、転置の定義は次のとおりです。

私は Coq を初めて使用しますが、いくつかの努力により、さまざまな帰納補題を証明することができました。ただし、次の帰納的定義を使用するすべての演習で行き詰まります。

私が得た最も遠いものは、次の補題でした：

次の 2 つの補題は、最初のステップを通過できませexistsんintros。

どんな助けでも大歓迎です！

多くの場合sledgehammer、証明を見つけるという問題が発生しますが、それを挿入しても終了しません。sledgehammerIsabelle の最も重要な部分の 1 つだと思いますが、証明が失敗すると面倒になります。

Sledgehammerのチュートリアルには、「なぜ Metis は証明の再構築に失敗するのか?」という小さな章があります。

それはリストします：

1. isar_proofs各ステップが によって正当化される段階的な Isar 証明を取得するオプションを試してくださいmetis。ステップはかなり小さいので、 metis再生できる可能性が高くなります。
2. smtの代わりに証明方法を試してくださいmetis。通常はより強力ですが、証明を再生するために Z3 を使用できるようにするか、SMT ソルバーを信頼するか、証明書を使用する必要があります。
3. 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、 、、、、 、を介して、必要な事実を渡しながら、blastまたは証明メソッドを試してください。autounfoldingusingintro:elim:dest:simp:

問題は、最初のオプションでは証明がより冗長になり、手動の介入が必要になることです。2 番目のオプションはほとんど機能しません。

では、3 番目のオプションはどうでしょうか。適用できる簡単なヒューリスティックはありますか?

unfoldingとはどう違いusingますか？また、失敗した証明からintro:、elim:、およびを使用する方法に関するベスト プラクティスはありますか?dest:metis

部分的な例

証明の最初の行は取るに足らないように見えるので、削除したいと思います。最初の行を削除してsledgehammerも証明は見つかりますが、この見つかった証明は失敗します (終了しません)。

最近、イザベルの定理証明器を使い始めました。別の補題を証明したいので、HOL ライブラリにある補題「det_linear_row_setsum」で使用されているものとは異なる表記法を使用したいと思います。より具体的には、「χ i 」ではなく「χ ij 表記」を使用したいと考えています。しばらくの間、同等の式を定式化しようとしてきましたが、まだわかりませんでした。

..

これを証明できる自動定理証明システムを探しています。

クロコダイルは男の子供を連れて行きました。男はワニに自分の子供を食べないように頼んだ. しかし、クロコダイルは言いました。

彼の分析ソリューションは次のようになります。

x - ワニは子供を食べる y - 男性 答え: ワニは子供を食べる

~ は等しいことを意味します。意味しない、-> 意味する、+ OR;

ですから、答えは男性が言わなければならないということです：「あなたは子供を食べるつもりはありません」。

さて、ここにはたくさんのシステムがリストされています: http://en.wikipedia.org/wiki/Automated_theorem_proving

私はそれらのうちの5-6を試しましたが、ここで何をしているのか本当に理解できませんでした. この定理をそれらの中で形式化して、その最初の部分に入ることができるようにする方法:

((x~y)->!x) and ((x XOR y)->x)

そして答えを得る

y出力として。

少なくともどのシステムが自動的にそれを行うことができるか、さらにヒントを教えてください。

よろしく、コンスタンチン。

C++ プログラムで z3 API を使用したいと考えています。どのヘッダー ファイルを含めるか、z3 関数などを含むプログラムを実行する方法を考えています。

z3 ソース コードに付属するファイルを確認しました。example.cppこのファイルを実行するmake examplesには、内部でコマンドを実行するビルド ディレクトリで実行する必要がありました。

プログラムを作成する場合、プログラムをコンパイルする../src/api必要があるたびに、このようにコンパイルする必要がありますか (lib ファイルをインクルードしてリンクします)。

私を助けてください、私は以前に z3 を使用したことがありません。どんな助けでも大歓迎です。:)

c++ 用の z3 API と、それらを c++ プログラムで使用する方法を学びたいです。チュートリアルを見つけようとしましたが、見つかりませんでした。どこからそれを学ぶことができますか？チュートリアルか何か？ありがとう。