問題タブ [theorem-proving]

私は 2 年生で、離散数学 2 の課題は自動定理証明器を作成することです。命題論理で動作する単純な証明プログラムを 4 週間で作成する必要があります (証明が常に存在すると仮定して)。これまでググってきましたが、そこにある資料は 4 週間で理解するのが本当に難しいです。初心者向けの本/サイト/オープンソースコードや、始めるのに役立つヒントを教えてくれる人はいますか? 前もって感謝します。

なぜ？

問題が発生するユースケースのコンテキスト

三角形のランダムなアイテムを 3 つ定義します。Microsoft Z3 は次のように出力する必要があります。

• 制約が満たされているか、または無効な入力値がありますか?
• すべての変数が具体的な値に割り当てられている他のすべての三角形アイテムのモデル。

項目を制約するために、assert等式を三角形にする必要があります。ピタゴラスの定理 ( (h_c² + p² = b²) ^ (h_c² + q² = a²)) から始めたかったのです。

問題

Microsoft Z3 には、非線形の算術問題を解決するための限られた機能しかないことを知っています。しかし、一部の手計算機でさえ、次のような非常に単純化されたバージョンを解決できます。

質問

• 2 つの値が指定されている場合、Microsoft Z3 でピタゴラスの定理を解く方法はありますか?
• または: 非線形算術のこれらのケースを処理できる別の定理証明者はいますか?

ご協力ありがとうございます - 何か不明な点があれば、コメントしてください。

Isabelleで補題を述べるとき、私はしばしば とタイプnitpickします。次にsledgehammer、証明を自動的に見つけようと入力します。

私は疑問に思います: NitpickとSledgehammerを呼び出して、同時に実行することは可能ですか? Sledgehammerはすでに私の補題を多数の自動証明者に送っているので、それらの証明者の 1 つは実際にNitpickのような反例発見者ではないでしょうか?

私の例：連立方程式

欲しい情報

連立方程式で、私は次の知識を得たいと思います。

与えられた値（制約ベース内）から変数値（解）を計算するために使用できる抽象的な式。

（高校のように、教師は結果を見たいだけでなく、そのような変換された抽象的な数式も望んでいました。）

私の質問

Z3Pyを使用して、Z3制約連立方程式からこの情報を取得するにはどうすればよいですか？

ありがとう。-不明な点がある場合は、何が問題なのかコメントしてください。

事例による証明を使用して証明したい単純な定理があります。以下に例を示します。

これを解決するにはどうすればよいでしょうか。そして、等値の 2 つの可能な値 (True または False) を使用してケースごとに証明を正確に定義するにはどうすればよいでしょうか?

どんな助けでも大歓迎です。ありがとう、

次の目標があります。

P 0この目標を、P 1、P 2、 、P 3の6 つのサブ目標に分割したいと思いP 4ますP 5。これは、 によって簡単に実行できapply autoます。しかし、これを行うために使用している関連するルールは何autoですか? 私の実際の目標は次のように見えるので、私は尋ねます：

apply autoその目標を同じように分解することはありません（それは私に与えます

代わりは）。

booleanSMT2と呼ばれる独自のブール値と、boolean_andそれらに対するAND関数を定義しました。私の推測では、ANDは可換です。

sk_xただし、z3は、スコーレム化された変数とでケース分割アサーションを使用できるはずだと思っていたにもかかわらず、しばらくするとこの問題について不明であると報告しますsk_y。

不思議なことに、ブール値の公理化を削除して、に置き換えると declare-datatypes、z3は次のように報告しunsatます。

私は何が間違っているのですか？公理化を使用してz3をケース分割するにはどうすればよいですか？

私の状況

私は次のことが必要なプロジェクトに取り組んでいます。

• 行列演算を含む3D 行列変換式の正しさを証明する
• 未知の行列エントリの値を持つモデルを見つけます。

私の質問

• で解くことができるように、行列演算を使用して式を表現する最良の方法は何z3ですか? ( Z3Py の Sudoku Exampleで使用されている方法はあまり洗練されておらず、より複雑な行列演算には適していないようです。)

ありがとう。- 何か不明な点がありましたら、質問コメントを残してください。

いくつかの表記法を定義するモジュール シグネチャを Coq で定義しました。しかし、署名の外でこれらの表記法を使用しようとすると、Coq は失敗します。私のコードの簡略版を以下に示します。どんな助けでも大歓迎です。

いくつかのプログラムの正しさを証明したいのですが、どこから始めればよいかわかりません。私が次のプログラムを持っているとしましょう。その正確性または欠如をどのように証明できますか。以下のソースから、それらを定理証明器にプラグインするにはどうすればよいですか。Coq、ACL2、またはほとんど何でも。

以下のコードは、標準入力から読み取るバイト数をカウントするだけです。2 つのバージョンがあり、1 つはバイトごとにカウントし、もう 1 つは可能であれば符号なし整数サイズのチャンクで読み取ります。ポータブルでもきれいでもないことはわかっています。これは、私が始めるための単なる例です。いくつかの助けを借りて。

コードは機能し、それが正しいことはわかっています。単体テストの書き方も知っていますが、それについて何かを証明する方法もわかりません。