※使用にはJava1.6以上のインストールが必要です
説明
シーケント計算などのゲンツェンスタイルの証明図を書くときは、普通TeXで「proof.sty」を使って書きます。しかし、証明が複雑になるとこれが非常に書きにくい。そこでそのTeX証明図の作成をアシストをしてくれるツールを作りました。昔は「XPE」というツールがあったのですが、X11上でしか動かないため、環境がそろえにくく、すでに動かしにくくなっています。このツールはJavaで作っており、大抵の環境で動くかと思います。ただし、XPEにあった自動証明機能はありません。整形ツールと言った方がいいかもしれません。
なお、現状不足してる機能が多量にありますが、まあ使う分には必要最低限の機能はあるかと。
簡単な使用例
Windowsの場合、JavaSEが入ってるならjarファイルをダブルクリックすると、起動します。
「Sequent」をクリックすると、編集できるようになります。
今回は、簡単な「左→」を使った、古典主義論理のシーケント計算での証明を書くことにしましょう。
なお、TeXでは、
- → :\to
- ∧ :\land
- ∨ :\lor
- ¬ :\neg
- ├ :\vdash
と書きます。
次に「infer」を押すと、上式が追加されます。
「左→」の場合は、上式が二つ必要なので、「Hypo」を押し、もう一つ式を追加します。
上式の左側を、左→を使ったAの証明に変えます。
右側をBの証明に。
使用した推論規則名を書こうと思うので、下式をクリックしてフォーカスを移動させます。
「Add Rule」を押すと、規則名を書く場所が追加されます。
規則名を「左→」に変えます。
これで完成したので、「Make」ボタンを押します。
「Make」ボタンを押すと、このようなウィンドウが出て、そこに「proof.sty」を使用したLaTeXのコードが表示されます。
表示されたソースをファイルに保存して、同梱されているproof.styを使ってLaTeXでコンパイルすると、このように表示されます。
なお、Save、Loadを使うと、状態を保存できます。
単に整形ツールなのでNKの証明図も書けます
ボタンの説明
- Infer
- 上式を追加し、上式と下式を線で区切る
- Infer*
- 上式を追加し、上式と下式の間を縦ドットにする
- Deduce
- 上式を追加し、上式と下式の間に何も書かない（推論規則名がある場合はそれが入る）
- Hypo
- 上式の要素を追加
- Insert Upper
- 選択中のフィールドの上に1行追加
- Insert Lower
- 選択中のフィールドの下に一行追加
- Single
- Inferのラインを単線にする
- Double
- Inferのラインを二重線にする
- Add Rule
- 推論規則名を書くフィールドを追加する
- Delete Rule
- 推論規則名を書くフィールドを消す
- Delete This
- 選択中のフィールドを削除する。選択したフィールドに上式があれば、全て削除された式の位置に追加される。
- Delele Uppers
- 選択したフィールドより上を消す。
- Make TeX
メニュー説明
- Save
- 証明図のデータを保存
- Load
- 保存した証明図を読み込み
- Quit
- 終了
ヒストリ
- β1：初公開
- β2：ファイルの保存と読み込み機能追加
- β3：クリア機能追加
- β4：
- NK用にInsert機能追加（今のところ上方向に追加なので、下方向も作るか）
- 誤爆回避のためにClearボタンを廃止しClear機能をFileメニューに追加
- proof.styがRedistribute可だったので、同梱した
- β5：
- β6：
- 一番下が下にInsertされなかったのを修正
- β7：
- Delete Uppersがおかしかったのを修正
- β8：
- Insert Lowerがおかしかったのを修正
- いじってたら途中でSaveがおかしくなっていたのを修正
※自分でも気になってること
