「述語論理をAgdaで書く」

というタイトルで、某氏作成の述語論理の実装と、私作成のホーア論理のインチキ実装を紹介しました。皆様、ご静聴ありがとうございます。
質疑応答

• Q.なんか、Agdaで証明を書いていると、手で証明を書いた後、Agdaで清書しているだけのように感じるのですが。
• A.Agdaの型の推定機能とrefinement機能により、証明の1ステップ前の論理式がどんな型であり、どんなルールが使われたかを推定することが出来ます。例題のような短い証明ではあまり利点とは感じないでしょうが、証明が長くなるほど便利になってくると思います。
• Q.自動で証明はできないのですか？
• A.有限ステップで有限個のルールを使用して証明を作るわけですから、全ての可能性を検査して正しい証明を取り出すことも原理的には可能です。しかし、将棋のゲームソフトと同じで、状態爆発が起き、指数関数的に可能性の数が増えていくので、全ての可能性を検査するのは数が多すぎて現在の計算機では不可能です。ですから、現段階では人間がうなくガイドする必要があります。