ゲーム紹介 古典論理の推論の妥当性を証明するゲームです。ここで遊べる証明法は「タブロー法」と呼ばれます。ブラウザ/モバイルのゲームです。命題論理と一階述語論理の両方を扱えます。（９月末までの期間限定で公開中） ゲームの遊び方 ・ゲーム画面のロードに数分かかることがあります。 ・ゲーム画面がロードされたら言語は「日本語」を選んでみてください。 ・妥当な推論の簡単な一例で、ゲームの遊び方を学びましょう。これです： A∨B, A⊃C, B⊃C ⺊ C ・目の前に「練習パネル」が開かれています。「練習パネル」のex 1)がそれになります。ex 1) をクリックしてください。すると画面てっぺんの入力画面に「 A∨B, A⊃C, B⊃C ⺊ C 」が表示されたはずです。 ・次に「証明開始」ボタンを押します。 ・すると、結論「C」の否定式を書くよう指示するダイアログボックスが生じます。 ・操作のチュートリアルをつけたい場合、ダイアログボックス内の「案内 付 / 無」のチェックボックスは、チェックを入れたままにしてください。 ・左隣の「記号パネル」にある否定記号を選んで、ダイアログボックス内の入力枠に「¬C」という否定式を書いてください。書いてから、「書けた！」ボタンを押してください。ゲームが始まります。 ・「A∨B」「A⊃C」「B⊃C」「¬C」という４つのノードで構成された一本の枝が伸びています。これは論証の前提すべてと結論の否定です。 ・ゲームが始まって最初にすることは、操作する枝を選ぶことです。 ・いま選択できる枝は一本しかありません。枝下にある「1」ボタンをクリックしましょう。すると枝に属する全てのノードに色がつきます。 ・規則が適用できる式（ノード）は赤紫で表示されます。 ・「X」規則を除くどの規則も適用できない式（ノード）は青で表示されます。 ・ノードたちに色がついたことが確認できたら、その中から規則を適用したい式（青色になったノード）のどれかをクリックで選びます。 ・選ばれたノードは黄色で表示されます。 ・ノードは一度に２つまで選択できます。「x」規則を適用するときは「A」と「¬A」（Aは任意の式）の二つが必要になります。 ・もしもノードの選択を解除したい場合、そのノードをもう一度クリックしましょう。するとノードの色が、黄色から赤紫か青に変わるでしょう。 ・いまひとつのノードを黄色にしていますか。次に、適用したい規則を左の「規則パレット」から正しく選んでください。それをクリックすると、ノードが増えて枝が伸びます。 ・再び、同じ枝「枝番号1」を選んでみましょう。いま規則を適用した式は、青色から赤紫に変わっています。古典命題論理のタブローでは、枝上で一度規則を適用すると、その式には２度と規則が適用できなくなります。 ・{枝番号をクリック -> 選んだ枝上にある青色の命題をクリック -> 「規則パレット」からそれに適用したい規則をクリック -> ノードが増えて枝が拡張} この作業を続けると同じ枝の上に矛盾が現れます。枝上に矛盾が現れたら、両方を選んで「規則パレット」の「x」をクリックしましょう。その枝が閉じて、数字が「x」に変わります。 ・全ての枝が「x」になったら、妥当性の証明は成功です。どうしても「x」にならない枝が残れば、妥当性の証明は失敗です。（しかし、「A∨B, A⊃C, B⊃C ⺊ C」は必ず妥当性の証明に成功します）