読者です 読者をやめる 読者になる 読者になる

JAPE

*JAPE

JAPE(J∀P∃)はユーザーが論理体系,理論をコード化し,証明図(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