![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
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.
Webstart とダウンロードする方法とがありますが，設定を変更した際などにリスタートが必要なので，今回はローカルにインストールします．
適当な書き込み可能ディレクトリにおいて
wget http://www.ls.cs.cmu.edu/KeYmaera/keymaera-installer.jar
により installer をダウンロード
java -jar ./keymaera-installer.jar
により起動，「Next」を押し，「3.5.11」を選択，以下デフォルトのまま step 6 まで進めてｘマークで終了させます．
java -jar ./keymaera-installer.jar
によりを起動，「Start KeYmaera」をクリック，外部プログラムのパスを聞かれますので，MathLibre20130831 以降の場合，
と入力，「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 で自動証明がスタート，直ちに
のように表示されます．利用したタクティックは左下の「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}
20131001-km.png