問題タブ [theorem-proving]

私は、B.Russell 著の本 Introduction to Mathematical Philosophy を読んでいて、そこに記述されているすべての定理を形式化しようとしていました。

一対多の関係は、次のテキストで説明されています ( contexts on book )。

1 対多の関係は、x が y に対して問題の関係を持っている場合、y に対しても関係を持っている項 x' が他に存在しないような関係として定義できます。

または、再び、次のように定義することもできます: 2 つの項 x と x' が与えられた場合、x が与えられた関係を持つ項と x' が持つ項には、共通の要素はありません。

または、再び、それらの 1 つとその逆の相対積が同一性を意味するような関係として定義することができます。ここで、2 つの関係 R と S の「相対積」は、あるときに x と z の間に成立する関係です。 x が y に対して R の関係をもち、y が z に対して S の関係をもつような中間項 y。

3 つの定義方法があります。最初の 2 つの記述に成功し、それらが同等であることを証明しました。3番目に行き詰っている間、「相対的な製品」の概念を取り除き、その意味合いに直接到達しようとしましたが、失敗しました.

以下は私の定義です。間違いはありましたか?

以下は、3番目の定義をどのように解釈するかであり、それらの同等性を証明することもできませんでした.

どの証明が であるかid_eqvはLemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y、前もって簡単に証明できます。

誰かが私がどこで間違ったのかを理解するのを手伝ったり、ヒントをくれたりできますか? 前もって感謝します。

簡単なレビュー：

• 推論規則＝結論＋規則＋前提
• 証明木 = 結論 + ルール + サブツリー
• 後方証明検索: 入力ゴールが与えられた場合、ボトムアップ方式で推論ルールを適用して証明ツリーを構築しようとします (たとえば、ゴールは最終的な結論であり、ルールを適用した後、新しいサブゴールのリストが生成されます)敷地内）

問題:
入力目標 (例: A AND B,C) が与えられた場合、最初に に AND ルールを適用すると、A AND B2 つの新しいサブ目標が得られます。最初の目標はA,Cで、2 番目の目標は ですB,C。
問題は、AとBが役に立たないことです。つまり、 のみを使用して完全な証明木を構築できCます。ただし、サブゴールが 2 つあり、C2 回証明する必要があるため、非常に非効率的です。

質問:
たとえば、 がありA AND B,C AND D,E AND F,G,H AND Iます。この場合、完全な証明木を構築するには、D と G だけが必要です。では、適用する適切なルールを選択するにはどうすればよいでしょうか。

これは Ocaml のコード例です:

関係代数の問題REL051+1.p の読み取り

対応するコードの fof で TPTP 構文を使用すると、

TPTPでわかるように、すべての ATP はそのような問題を証明できません。

この定理は、次の SMT-LIB を使用して Z3 で反駁されました。

対応する出力は

この例をここでオンラインで実行してください

私の質問は次のとおりです。Z3 に関するこの反論は正しいですか?

私は (誤って) 並行プログラムの検証に関するコースを受講しており、これまで「Owicki-Gries 法」と呼ばれるこの方法について説明してきました。どうやら、アサーションを各ステートメントに関連付けることで、プログラムに関するさまざまな結果を証明し、これらのアサーションが帰納的であり、互いに干渉しないことを示すことができます。私たちの課題の 1 つは、Lamports の Fast Mutual Exclusion アルゴリズムに関するもので、この論文で詳しく説明しています。

この論文では、相互排除のための Owicki-Gries スタイルの証明が与えられています。それは完全に直感に反するように見えます。私が理解するのに苦労しているのは、そもそもこれらの主張をどのように考え出すかということですか? これらの主張が強すぎず (干渉の自由を壊すほど強い) も弱すぎもしない (たとえば、各ステートメントのトートロジーのような些細なこと) はいつわかりますか?

乾杯

入力は (任意の) チェックされた構文を持つ記号の文字列で、出力は TRUE または FALSE です。

AND、XOR、TRUEで書かれた論理式を後置表現しようと考えていたのですが、後置ではパターンが認識しづらくなることにようやく気が付きました。

例:

p IMPLIES qと書くことができるTRUE XOR p (XOR (p AND q))省略形 1+p+pq

p EQUIVALENT WITH qは 1+p+q と省略して書くことができます

NOT p省略形 1+p

p または q p+q+pq の省略形

このブール環の規則は通常の代数と同じで、次の 2 つの規則があります。

• p+p=0
• pp=p

これらのルールは、交換とともに、すべての削減を担当し、文字列がトートロジーに対応する場合は '1' になります。トートロジー Modus ponens、

((p IMPLIES q) AND p) IMPLIES q ,

は、最初に上記のように代入し、次に分配的に乗算して拡張し、最後に繰り返し単純化する必要があります。IMPLIES を単純に置き換えると、次のようになります。

トートロジー式がブール環の要素として記述されると、機械的に 1 に還元されます。他の式は、代数的に単純な式に還元されます。

これは良い戦略ですか？コンピュータサイエンスではどのような戦略が使用されていますか?

Z3 を使用して未知の射影関数を含む方程式を解き、方程式を満たす関数の有効な解釈を見つけようとしています。たとえば、方程式の場合:snd . f = g . fst有効な解釈はf = \(x,y) -> (y,x)とg = idです。Z3 が高次でないことはわかっているので、問題を一次形式でエンコードしようとしています。たとえば、次のf = g.fstように使用します。

どのような種類の作品が戻ってきますか:

ただし、snd . f = g . fst（ツリーをペアに単純化して試してみました）：

私は得るunknown。

また、ブール値または整数をパラメーターとして使用するだけでADTを使用せずに同様の問題をエンコードしようとしましたが、モデルは関数に定数値を割り当てるだけです。また、関数定数、恒等関数、ペアワイズおよびシーケンシャル コンポジション用の単純な ADT を定義してから、 のような式を単純化できる「equals」関数を定義しようとしましたf.id = fが、これには次のような再帰関数が含まれます。

これは明らかに無効です。または、解釈されていない関数を使用すると、「eq」が定数関数になります。

Int -> Int 型の関数を含む方程式と同様に、これは f と g の定数関数を返します。

これらのタイムアウトを追加します。

この種のことを機能させる方法はありますか？

どうもありがとう！

YouTube で解像度に関するビデオを見ていましたが、このビデオに出くわし、かなり役に立ちました。

http://www.youtube.com/watch?v=hhTxW5c3BXo

終わり近くで、彼は、それぞれの節の反対側にある X の両方が相殺され、残りが一緒に結合される例を示していますが、これは問題ありませんが、たとえば、複数の変数が相殺される場合に機能するかどうかを知りたいと思っていました。

(AB -> CDXY) (PQXY -> RS)

XY をキャンセルすると、ABPQ -> RSCD が発生します。

この「二重解決」のケースは当てはまらず、2 つ以上の変数のキャンセルに関する情報を見つけることができなかったという直感が得られます。

足りないものはありますか？

Z3 を使用すると、次のことを証明できます。

1 パラメータ グループを形成します。

証明は、次の Z3 コードを使用して実行されます。

対応する出力は次のとおりです。

ここでコードをオンラインで実行してください。

その他の例: 証明する

1 パラメータ グループを形成します。

証明は、次の Z3 コードを使用して実行されます。

対応する出力は次のとおりです。

ここでこのコードをオンラインで実行してください

その他の例：それを証明するために

1 パラメータ グループを形成します。

証明はここでオンラインで与えられ、4 次元拡張はここでオンラインで与えられます。

最後のいくつかの例:

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

証明してください

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

より一般的に、

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

1 つの 3 次元拡張: 証明する

1 パラメータ グループを形成します。

証拠はここでオンラインで提供されます。

双曲線関数を使用した例:

1 パラメータ グループを形成します。

証拠は ここでオンラインで提供されます

私の質問は次のとおりです。

1. 配列を使用して高次元の証明を作成することは可能ですか?

2. Z3 は、これらの証明を実行できる唯一のシステムであると主張します。同意しますか？