Agda2 で出会う「矛盾の証明」との戦い方はじめに この記事は Theorem Proving Advent Calendar 2011 の10日目の記事です。 1 日目の pi8027 さんの Agda2 の紹介記事 がありましたが、私も「依存型関数型プログラミング言語 Agda2 」についてお話しします。 Agda2 は依存型関数型プログラミング言語であると同時に、プログラミングを対話的に支援する Emacs 上の major-mode が付いた開発環境でもあります。また、依存型であるが故に論理との対応がつき、定理証明系としての使い方もできます。ただし、定理証明系としての機能は Coq や Isabelle/HOL よりもずっと弱いので、 Agda2 を定理証明系として使うのは、一般的にはお勧めしません。なにかメリットがあれば使えば良いと思います。 この記事では、 Agda にある程度習熟した（命題論理や一階述語論理における命
A proof of the irrationality of the square root in Agda
