*JAPE
JAPE（Ｊ∀Ｐ∃）はユーザーが論理体系，理論をコード化し，証明図（Fitch diagrams，Gentzen trees）やcounter model（Kripke diagrams）を簡単なマウス操作により作成できるproof calculatorです．
// - Japeカーネルにコード化の仕様（テキストファイル）を読み込んで利用する．
// - 既存の定理の参照可能．
// - 証明図のスタイル変更可能．
// - コード化ごとに書式が異なる．
*インストール例
適当な書き込み可能ディレクトリにおいて
wget http://www.cs.ox.ac.uk/people/bernard.sufrin/personal/jape.org/BUILDS/v7_d15/InstallLinuxjape.jar
java -jar ./InstallLinuxjape.jar
により installer が起動，（必要に応じてインストール先を変更，「command in ...」をチェックし）「Install」の後，「Exit (and clean up) now」で完了．
*起動例
インストール先の/examples以下に多数のコード化の例が収められており，これら理論ファイル(jt)を引数にして，以下のように起動すると便利です．
自然演繹
./Jape ./examples/natural_deduction/I2L.jt
./Jape ./examples/jnj/jnj.jt
./Jape ./examples/ItL_QMWpre2000/ItL.jt
シーケント計算
./Jape ./examples/sequent_calculus/SCS.jt
./Jape ./examples/sequent_calculus/MCS.jt
関数，等号を持つ理論
./Jape ./examples/functional_programming/functions.jt
./Jape ./examples/functional_programming/trfunctions.jt
集合論
./Jape ./examples/sets/set.jt
拡張子「j」のファイルを追加することもできます．
厳格なLK
./Jape ./examples/sequent_calculus/MCS.jt ./examples/sequent_calculus/MMCS.j
free logicに準じた体系．var m，m inscope が入用．
./Jape ./examples/sequent_calculus/MCS.jt ./examples/sequent_calculus/MCS_LF.j
右辺に複数の式を許す直観論理
./Jape ./examples/sequent_calculus/MCS.jt ./examples/sequent_calculus/IMCS.j
あるいは引数なしで ./Jape と起動し，「File」から「Open...」または「Open new theory」でも構いません．とくにファイル名が空白を含む ./examples/useful_buttons/displaystyle in Edit menu.j などは（ファイル名を変更するか）「Open...」から読み込みます．また「Erase theory」により，再起動なしで理論を初期化出来ます．
*証明図作成例
./Jape ./examples/sequent_calculus/MCS.jt
として起動すると，「conjectures」，「Jape Control」が開くので，前者から「|- ((P→Q)→P)→P」をポイントして，ダブルクリック．「Proof #1」が開くので，以下，適当な箇所のポイント，ダブルクリックなどを繰り返すと
&ref(2014061101.png);
のような証明図が得られます．Ctrl+d で「Proof #1」が閉じ，チェックがついて定理になります．
証明の保存はctrl+s．proofファイルの拡張子は「jp」．
*リンク
- http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html
- http://www.cs.ox.ac.uk/people/bernard.sufrin/MANUALS/roll_your_own.pdf
