問題タブ [proof-system]

数式を入力して操作を実行できるが、数学的に有効な操作のみに制限するツール (GUI が推奨されますが、CLI が機能します) を探しています。また、ツールはセッションを保存し、保存された特定の一連の操作が有効であることを後で証明できる必要があります。

注:証明を生成するシステムを探しているのではなく、手動で指定した手順が有効であることを確認するだけです。

同様の操作にACL2を使用したことがありますが、一部のケースではうまく機能しますが、それ以外の場合は非常に使いにくいです。

この小さなプロジェクトが私のモチベーションです。方程式を解くことができる D テンプレート タイプです。この方程式を考えると：

シンボルのいずれかを不明として設定でき、その式を評価すると、その変数に割り当てられます。これは、式ツリーを型に組み込み、書き換え規則を使用してそれを未知の型に対応できるものに変換することによって機能します。

必要なのは、書き換えルールを検証する方法です。それらは、ある関係が真であり、別の関係も真であるというアサーションをテストすることによって検証できます。

...そして、彼らは私がそれらを読む余裕があるところに結果を公開しましたか?

私は定義された誘導型を持っています：

今、私はその誘導型の一連の特性を証明する必要がありますが、私は立ち往生し続けています。

誰かが私が前進するのを手伝ってもらえますか？

2 つの 1 次式 F と G が等しいことを自動的に証明する最良の方法は何ですか?

式には、「完全な」一次式と比較していくつかの制限があります。

1. 量指定子なし
2. 機能フリー
3. 暗黙的に普遍的に量化された

これらの式を句の標準形に変換でき、リテラルの統一のためのルーチンがあります。ただし、続行する方法と、この問題が決定可能かどうかはわかりません。

COQ では、タイプ prod (1 つのコンストラクターのペアを持つ) はデカルト積に対応し、タイプ sig (1 つのコンストラクターが存在する) は従属和に対応しますが、デカルト積が従属和の特定のケースであるという事実はどのように説明されますか? prod と sig の間にリンクがあるのではないかと思います。たとえば、定義上の同等性がありますが、リファレンス マニュアルには明示的に記載されていません。

私は以下を解決しようとしましたが、それを確認する手段がありません....または、ウルフラムはこれを行いますか? オペレーター（スコープ）の扱いが正確かどうかわかりません...知っていますか？すべての x に対して: 逆さまの A 演算子 (普遍性)

証拠：

簡単なレビュー：

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

問題:
入力目標 (例: 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 のコード例です: