最近Isabelle始めたばかりなので, 初心者的な視点からIsabelle入門以前の話をします. この記事を読んでIsabelleに興味を持たれたら, 是非公式turtorialからIsabelleへ入門してみてください. Isabelleについて Isabelleは証明支援言語です. 以下にその特徴をあげてみます. 標準のjEdit環境がリッチ 強力な自動証明機構 (とにかく自動証明コマンドが豊富で, さらに証明をIsabelleに探索させることもできます) 公理系が選べる (公理系はライブラリレベルでサポートされています. importするライブラリを自分で選ぶことで, HOL, ZF, Sequents, Cube などなどたくさんの公理系を扱うことができます) Isabelle/Isarによる人間に優しい証明 (Coqのように証明図をコマンドによって変形していくだけでなく, Is
![Isabelle入門の入門 - Qiita](https://cdn-ak-scissors.b.st-hatena.com/image/square/e57dc46d7ce5b1906f61bba88f14281728c66f6b/height=288;version=1;width=512/https%3A%2F%2Fqiita-user-contents.imgix.net%2Fhttps%253A%252F%252Fcdn.qiita.com%252Fassets%252Fpublic%252Fadvent-calendar-ogp-background-f625e957b80c4bd8dd47b724be996090.jpg%3Fixlib%3Drb-4.0.0%26w%3D1200%26mark64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTkxNiZoPTMzNiZ0eHQ9SXNhYmVsbGUlRTUlODUlQTUlRTklOTYlODAlRTMlODElQUUlRTUlODUlQTUlRTklOTYlODAmdHh0LWNvbG9yPSUyMzNBM0MzQyZ0eHQtZm9udD1IaXJhZ2lubyUyMFNhbnMlMjBXNiZ0eHQtc2l6ZT01NiZ0eHQtY2xpcD1lbGxpcHNpcyZ0eHQtYWxpZ249bGVmdCUyQ21pZGRsZSZzPWE4Nzk3NzUyYTQ2M2ZiZTUzY2YzODgzNDUwNTg2MTAz%26mark-x%3D142%26mark-y%3D151%26blend64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTYxNiZ0eHQ9JTQwbXl1b25fbXlvbiZ0eHQtY29sb3I9JTIzM0EzQzNDJnR4dC1mb250PUhpcmFnaW5vJTIwU2FucyUyMFc2JnR4dC1zaXplPTM2JnR4dC1hbGlnbj1sZWZ0JTJDdG9wJnM9YTUxOTdkNDcxZTczY2EwMGI2MjUxZWI4NjMxZDllMmQ%26blend-x%3D142%26blend-y%3D491%26blend-mode%3Dnormal%26s%3D407cdb78551e00a13a5c00a070714f98)