Isabelle2013 の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• Isabelle2013 へ行く。

*Isabelle2013 [#tb60deb7]
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

多彩な定理証明環境です．インターフェイスはemacsではなくjeditが標準です．

自動証明提案ツール sledgehammer http://www.cl.cam.ac.uk/~lp15/papers/Automation/index.html を実装した唯一のシステム．

*インストール例 [#he922c7d]
 sudo apt-get install coinor-csdp
 export CAS=/usr/local/CAS
 sudo mkdir $CAS
 sudo chmod 777 $CAS
 cd $CAS
 wget http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013_linux.tar.gz
 tar zxvf ./Isabelle2013_linux.tar.gz
 echo "export Z3_NON_COMMERCIAL=yes
 export ISABELLE_CSDP=/usr/bin/csdp" >> ~/.bashrc
 sudo ln -s $CAS/Isabelle2013/bin/isabelle /usr/local/bin/isabelle
 isabelle jedit
*使用例 [#aaa58f1b]
 echo -e "theory test imports Complex_Main
 begin
 lemma \"setsum id {..(n::nat)} = n * (n + 1) / 2\"
   by (induct n, simp_all add:real_of_nat_Suc algebra_simps)
 end" | isabelle tty
*デモ映像 [#m8e354c5]
- http://www.youtube.com/watch?v=AhybiY0JHvg&list=PLV4jidMU0jOKCs32SwUR4hBgURHtlBCOs
*リンク [#ibfe853b]
- http://www.cl.cam.ac.uk/research/hvg/Isabelle/
- http://d.hatena.ne.jp/ehito/20130503/1367582411
- http://suseum.jp/gq/question/2067
- http://www.jssac.org/Editor/Suushiki/V16/No2/V16N2_106.pdf