DevoirDire 作成者: Jason

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

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

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

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

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

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

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

教育モードでは、学生が式の答えを判定または構築する自動採点の演習が出題され、メインエディタと同じ検証エンジンが使用されます。一覧の最後の問題のあとも、新しい問題が自動生成され、進捗は問題の種類ごとに記録されます。

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

英語（カナダ）、フランス語（カナダ）、ドイツ語、イタリア語、日本語に対応しています。