The Proof Machine (2016)

The Incredible Proof Machine ℹ 🔄 現在のタスク：ブロック数：論理ブロック：ヘルパーブロック：新しいカスタムブロック：カスタムブロックを追加：↶ ↷ + − 1:1フィット ⤓ 🔄 × 今日は何を証明したいですか？ × The Incredible Proof Machineへようこそ！これは何ですか？これは、様々な論理（例えば、命題論理、述語論理）で視覚的に証明を実行するためのツールです。証明の各ステップを表すブロックを追加し、それらを正しく接続するだけで、結論が緑色になれば、完全な証明を作成したことになります！ドットを2つ接続するには、ドラッグ＆ドロップするだけです。完成した証明の例については、この論文を参照してください。UIの簡単な紹介については、Tea Leaves Programmingチャンネルの紹介ビデオ（13分）をご覧ください。なぜこれがあるのですか？The Incredible Proof Machineは、証明を行う楽しさと喜びを伝えるために作成されました。特にコンピュータ支援の方法で、まず「実際の」定理証明器（例：Isabelle）の構文を学ぶ必要なしにです。どのようなキーボードショートカットが使用できますか？CTRL+Z：変更を元に戻すCTRL+Y：変更をやり直すCTRL+A：すべてのブロックを選択BACKSPACE、DELETE：選択したブロックを削除SHIFT+MOUSE1：選択にブロックまたは領域を追加結論が緑色にならないのはなぜですか？あなたの証明が（まだ）証明ではないからです。これにはこれらの理由が考えられます：いくつかのブロックには、どこにも接続されていない入力（仮定）があります。これらは赤色で表示されます。いくつかの接続は、明らかに異なる命題（赤色で☠マークが付いている）を接続しているか、またはそれらが不十分で、異なるかどうか不明確（赤色で？マークが付いている）です。後者の場合、注釈ブロック（✎P）を挿入すると役立つ場合があります。証明にサイクルがあります。これらは（ご想像の通り）赤色で表示されます。ローカル仮説を誤って配線しました。ローカル仮説とは、ブロックのへこみの左側に出力され、対応するへこみの右側の入力に接続される証明の部分でのみ使用できるものです。これらが赤色で表示されることを言及する必要があるでしょうか？これらの奇妙な文字をどのように入力しますか？数式を入力する必要がある場所はごくわずかです。主に✎Pブロックを使用したい場合や、独自のタスクを定義したい場合です。そこで、次の略語を使用できます：∧ ∨ → ↑ ¬ ∀ ∃ ⊥ の代わりに、& | -> ^ ~ ! ? False と書くことができます。複数の仮定または結論を持つカスタムタスクをどのように作成しますか？各仮定と結論を独自の行に配置します。つまり、それぞれにEnterキーを押します。カスタムブロックをどのように作成しますか？Shiftキーを押しながらクリックすると、ブロックを選択できます。次に、選択したブロックをラップするカスタムブロックを作成するオプションが表示されます。私の証明はどこに行きましたか？現在、証明はブラウザ内でのみ保存されます。これは、このウィンドウ/タブを閉じた後にローカルストレージを削除した場合、またはプライベートブラウジングセッションなどの場合に失われることを意味します。将来のバージョンでは、サーバーに進行状況を保存する計画があります。誰がこれを作ったのですか？主にJoachim Breitnerが、いくつかの同僚や友人からの貴重な助けを得て作成しました。ここでさらに読むことができますか？Incredible Proof Machineの詳細については、特に学術的な観点から、次の出版物を参照してください：Joachim Breitner：Visual theorem proving with the Incredible Proof Machine、ITP 2016で採択された論文、2016年8月Joachim Breitner：The Incredible Proof Machine、LFMTP 2016での招待講演、2016年6月Joachim Breitner、Denis Lohner：The meta theory of the Incredible Proof Machine、Archive of Formal ProofsのIsabelle形式化、2016年5月Incredible Proof Machine、Joachim Breitnerへのインタビュー、Sebastian Ritterbuschによる、科学ポッドキャスト「Modellansatz」のエピソード78、ドイツ語、2016年手伝ってもらえますか？もちろん！すべてFree Softwareなので、すぐにコードを取得して貢献を開始できます。より多くの人々が貢献するほど、The Incredible Proof Machineはより信じられないものになります。