Isabelleのチュートリアルを読みながらまとめていきたいと思います。http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf最新バージョンはIsabelle2009-1。バージョンが変わる前…

1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理…