KeYmaera の編集

*KeYmaera [#o60ecdc0]

KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.

- KeYmaera（キメラ）は formal verification ツール KeY（ http://www.key-project.org ）を differential dynamic logic（様相論理を dynamic logic に一般化する際の action に微分など連続的な条件と差分や場合分けなど離散的な条件との双方を許した，いわゆる hybrid system を扱う論理）まで拡張したもので，その名の通りビルトインだけでなく Mathematica，QEPCAD B，REDUCE，HOL Light といった QE ツールをバックエンドに用います．
// これは formal verification としては致命的です

- KeYmaera の自動証明におけるストラテジーは，常微分方程式系（またはその解）を用いて結論（またはそれを導く式）を代数不等式系に書き換えるものです．また，対話的な利用においては，ポイントした位置に応じたマウスの右クリックメニューからタクティックを選択してゆく高機能な証明環境が実装されています．

*インストール例 [#o4f9f46b]
Webstart とダウンロードする方法とがありますが，設定を変更した際などにリスタートが必要なので，今回はローカルにインストールします．

適当な書き込み可能ディレクトリにおいて

wget http://www.ls.cs.cmu.edu/KeYmaera/keymaera-installer.jar

により installer をダウンロード

java -jar ./keymaera-installer.jar

により起動，「Next」を押し，「3.5.11」を選択，以下デフォルトのまま step 6 まで進めてｘマークで終了させます．

*使用例 [#h42f031e]

java -jar ./keymaera-installer.jar

によりを起動，「Start KeYmaera」をクリック，外部プログラムのパスを聞かれますので，MathLibre20130831 以降の場合，

--「Qepcad Path」に /usr/local/CAS/qesource

--「Reduce Binary」に /usr/bin/reduce

と入力，「Always use these settings as default」をチェックして「OK」，提示された SMT ソルバー「Z3」，SDP ソルバー「csdp」をそれぞれ「Download」して「はい」を押せば．Prover と Assistant のウインドウが現れます（外部プログラムのパスは「Options」→「Tool Paths...」でも設定できます．また，~/.keymaera/proof-settings.props を書き換えても構いません）．

Ctrl + Alt + o でサンプルが開くので，LICS'12 Tutorial から1つ目の continuous system の例を「Load」して，Ctrl + e で自動証明がスタート，直ちに

&ref(20131001-km.png);

のように表示されます．利用したタクティックは左下の「Proof」パネルで参照できます．

述語論理の例（2次の判別式）．次を tst1.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

\programVariables{R a,b,x;}
 \problem{!b=0->(\exists R x.x+a+b/x=0<->a^2>=4*b)}

dynamic logic（ http://en.wikipedia.org/wiki/Dynamic_logic_%28modal_logic%29 ）の例（様相性と否定）．次を tst2.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

\programVariables{R a,x,y;}
 \problem{(\[(x:=a)++(y:=a)\]x=a)<->(!\<(x:=a)++(y:=a)\>!x=a)}

数学的帰納法の例（数列の和）．次を tst3.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

\programVariables{R n,s;}
 \problem{n=0&s=0->\[(n:=n+1;s:=s+n^4)*\]s=n*(n+1)*(2*n+1)*(3*n^2+3*n-1)/30}

//数学的帰納法の例（ロジスティック写像）．次を tst3.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

// \programVariables{R a,x;}
// \problem{0<=a&a<=4&0<=x&x<=1->\[(x:=a*x*(1-x))*\](0<=x&x<=1)}

*リンク [#a1a4d5c1]

- http://symbolaris.com/info/KeYmaera.html
- http://www.youtube.com/watch?v=K7w2jGHqvdI （Webstart の説明）
- http://www.youtube.com/watch?v=jl0P4HYf9Y8 （反例の生成）
- http://www.youtube.com/watch?v=BawF1k4AnlE （帰納法が止まった時に強いサブゴール loop invariant を設ける方法）
- http://www.youtube.com/watch?v=suMtmNkI_CM （hybrid system の例）

タイムスタンプを変更しない

*KeYmaera [#o60ecdc0]

適当な書き込み可能ディレクトリにおいて

wget http://www.ls.cs.cmu.edu/KeYmaera/keymaera-installer.jar

により installer をダウンロード

java -jar ./keymaera-installer.jar

により起動，「Next」を押し，「3.5.11」を選択，以下デフォルトのまま step 6 まで進めてｘマークで終了させます．

*使用例 [#h42f031e]

java -jar ./keymaera-installer.jar

によりを起動，「Start KeYmaera」をクリック，外部プログラムのパスを聞かれますので，MathLibre20130831 以降の場合，

--「Qepcad Path」に /usr/local/CAS/qesource

--「Reduce Binary」に /usr/bin/reduce

Ctrl + Alt + o でサンプルが開くので，LICS'12 Tutorial から1つ目の continuous system の例を「Load」して，Ctrl + e で自動証明がスタート，直ちに

&ref(20131001-km.png);

のように表示されます．利用したタクティックは左下の「Proof」パネルで参照できます．

述語論理の例（2次の判別式）．次を tst1.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

\programVariables{R a,b,x;}
 \problem{!b=0->(\exists R x.x+a+b/x=0<->a^2>=4*b)}

\programVariables{R a,x,y;}
 \problem{(\[(x:=a)++(y:=a)\]x=a)<->(!\<(x:=a)++(y:=a)\>!x=a)}

数学的帰納法の例（数列の和）．次を tst3.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

\programVariables{R n,s;}
 \problem{n=0&s=0->\[(n:=n+1;s:=s+n^4)*\]s=n*(n+1)*(2*n+1)*(3*n^2+3*n-1)/30}

//数学的帰納法の例（ロジスティック写像）．次を tst3.key として保存，Ctrl + o でロード，Ctrl + e で自動証明スタート．

// \programVariables{R a,x;}
// \problem{0<=a&a<=4&0<=x&x<=1->\[(x:=a*x*(1-x))*\](0<=x&x<=1)}

*リンク [#a1a4d5c1]

テキスト整形のルールを表示する