Loading article…
Japeは、設定可能なグラフィカル証明支援システムであり、元々はロンドン大学クイーン・メアリー校のリチャード・ボーナットとオックスフォード大学のバーナード・サフリンによって開発されました。[ 2 ]このプログラムは、 Mac、Unix、およびWindowsオペレーティングシステムで利用可能です。Javaプログラミング言語で記述されており、 GNU GPLの下でリリースされています。
Japeは、数理論理学における証明の作成演習を含む「コンピュータ支援論理教育」のための最も人気のあるプログラムであると主張されている。[ 3 ]
Japeは、形式的推論をより深く理解することを目的として、1992年にリチャード・ボルナットとベルナール・スフリンによって作成されました。ベルナール・スフリンが「Jape」という名前を考案しました。[ 2 ]
2019年に、彼らはGitHubでコードを公開した。[ 4 ]
Jape は、ユーザーが推論規則のシステムとして定義する論理体系において、人間が主導する証明の発見をサポートします。ユーザーのジェスチャー (タイピング、マウスのクリック、マウスのドラッグなど) をアシスタントの証明アクションにマッピングします。Jape は、オブジェクト ロジックや理論に関する特別な知識を持たず、現在ロードされているオブジェクト ロジックの規則によって正当化される場合にのみ、証明内の移動を行います。[ 5 ] Jape では、証明ステップを作成および取り消すことができ、追加された証明ステップの効果を表示することで、証明を見つけるための戦略を理解するのに役立ちます。[ 2 ] : 60ユーザーが証明ステップを追加および削除すると、証明ツリーが構築され、Jape はそれをツリー形式またはボックス形式で表示できます。[ 5 ] Jape では、さまざまな抽象度レベルで証明を表示できます。証明専用の表示モードを使用することで、順方向証明を自然演繹スタイルで表示することも可能です。[ 6 ]
Japeはシーケント計算と自然演繹の変種を扱う。また、量化子を用いた形式的証明もサポートしている。[ 2 ]： 84