![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
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 を実装した唯一のシステム．
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
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
