DevoirDire 作成者: Jason

DevoirDireは、形式論理文書の作成・検証・管理を行うツールです。法令・政策、契約、規格・仕様、論理学の授業など、ルール・義務・要件を正確に記述する必要がある場面で、曖昧さを低減します。

作成：述語論理、量化子、等号、そして義務論理演算子（義務・許可・禁止）と時相演算子（常に・いつか・まで）を用いて、ガイド付きの式ビルダーでノードごとに式を構築できます。JSONを手書きしたり構文を学んだりする必要はありません。

検証：文書を3つの方法でチェックします。

• 無矛盾性：これらの式は同時に充足可能か？
• 妥当性：選択した結論は他の式から導かれるか？
• 健全性：その論証は妥当であり、かつ組み込みの事実ベースに裏付けられているか？

義務論理・時相推論はチェックごとに任意で有効化でき、設定可能で有界な可能世界の集合上で評価されます。結果にはすべての留保事項と限界が明確に示され、曖昧にされることはありません。

管理：文書はローカルで管理されます。インポート、エクスポート、作成、編集、再構成、日付付きリビジョンの保存はすべて端末上に保存されます。任意の共有編集をオンにしない限り、データが端末の外へ出ることはありません。初期設定ではオフです。

共同編集(任意):文書をホストし、サーバーを介さないブラウザー間の直接接続で他の人を招待できます。最初に全員が安全番号を確認し、編集できる人はホストが選び、すべての変更はリビジョンとして記録されます。

練習問題にはガイド付き練習問題があり、学生が式の答えを判定または構築する自動採点の問題を、メインエディタと同じ検証エンジンで出題します。一覧の最後のあとも新しい問題が自動生成され、進捗は問題の種類ごとに記録されます。ロジックジムには時間制限つきのドリルと対戦があり、アカデミーから始まります。問題を作成で自分の問題も作れます。

キーボードとコントローラー：すべての操作をキーボードで行えます。練習問題、文書一覧、エディターの単一キーのショートカットは、割り当ての変更や無効化ができます（?キーで一覧表示）。ゲームコントローラーへの対応は任意で、設定で有効にするまでオフです。これまで動作を確認したのは疑似コントローラーのみです。

英語(カナダ)、フランス語(カナダ)、ドイツ語、イタリア語、日本語、スペイン語、簡体字中国語、ヒンディー語で利用できます。