ソフトキーボードまたはキーボードから式を入力し、「解析」を押す。事前にテキストエディター等で入力した式を入力欄にコピー&ペーストしてもよい。文法的に正しければ結果欄に表示される。 「この式を前提に加える」または「この式を結論とする」を選ぶ。これを繰り返して、推論を入力する。 推論を入力し終わったら、上部の「チェック開始」を押す。 タブローの展開規則を適用したい式の上にドラッグ&ドロップする。 枝が閉じたら、その枝の末端に「枝を閉じる」をドラッグ&ドロップする。 間違えた場合は、枝の末端に「式を削除する」をドラッグ&ドロップする。 すべての枝が閉じたら「チェック終了」を押す。閉じないことがわかったら「チェック中止」を押す。 デモビデオ ∀x(Tx∧Mx) ┣ ∀xTx∧∀xMxの妥当性のチェック 出演:土屋俊 放送大学「記号論理学('14)」第7回より許可を得て転載 ¬∃xCx∨∃x(Cx∧