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
終了行:
*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
ページ名: