ATPとCASのこと

2013-05-03

Isabelle/Isar(その1)

 Isabelle/HOLはHOLのラッパーですが,HOLにはない「推論規則による(危うげな部分も含む)マッチング」が特徴です.ただしかつてのapply-doneによるタクティック列挙の証明は,現在は構造化された言語Isar上でのエミュレーションとなっており,証明のスタイルは,システムが生成するサブゴールを人間が復唱したのち逐次証明する,悪く言えば迂遠,良く言えば修正が容易で読み易い?もの(Isar=Isabelle/HOL上のMisarではなく,Intelligible semi-automated reasoning.http://isabelle.in.tum.de/Isar/)に移行,結果として多様な証明が書けるシステムとなっています.

 apply-doneスタイルの証明についてはチュートリアルの翻訳(http://d.hatena.ne.jp/caeruiro/20100314/1268569131)がありますので,ここではIsarの特徴的な部分を中心に述べて行きます

 まずは,インストールスクリプト(for Linux).次を端末にコピー&ペーストしてください.

cd ~
echo "export Z3_NON_COMMERCIAL=yes
export ISABELLE_CSDP=/usr/bin/csdp
export PATH=$PATH:~/Isabelle2013/bin/" > ~/.bashrc
source ~/.bashrc
sudo apt-get update
sudo apt-get install coinor-csdp
wget http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz
tar -xzf ~/Isabelle2013_linux.tar.gz

ユーザーホームディレクトリにIsabelle2013というイザベルホームディレクトリが出来,準備完了です.あとは

isabelle jedit

とすれば

f:id:ehito:20130503211121j:image

のように初回起動時にPUREとHOLロジックのイメージが生成された後に,jeditが立ち上がります.メニューを日本語にするにはC+F12でオプションを表示,Generalにある言語で日本語を選択(反映には再起動),フォントはText-Areaで調整できます.

f:id:ehito:20130503211119j:image

f:id:ehito:20130503211118j:image

インターフェイスとしては他に,レスポンス抜群のtty

f:id:ehito:20130503211117j:image

お約束のemacs/Proof-General

f:id:ehito:20130503211114j:image

があり,後者は

f:id:ehito:20130503211154j:image

のように入力直後のコマンドが通るか自動的に判定させることもできますが...jeditはその上を行く「自動評価環境」です.

f:id:ehito:20130503211153j:image

f:id:ehito:20130503211151j:image

すなわち,カーソル行に対するシステムの出力が自動的に表示されるため,評価を指示するキー操作は全く不要,人間は証明を書き続けるのみです(jeditの頑張り具合はプラグインメニューのIsabelleにあるMonitor panelで確認できます).

 なお,Windowsへのインストールは,http://isabelle.in.tum.de/dist/Isabelle2013.exeダウンロード,実行するとデスクトップにIsabelle2013というイザベラホームディレクトリと,jdeitへのリンクが出来るのでクリックすれば,初回のみ

f:id:ehito:20130510112315p:image

のようにイメージが生成された後に,jeditが立ち上がります.

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/ehito/20130503/1367582411