突然ですが、皆さんは定理証明支援器ってご存知ですか。 定理証明支援器というのは、命題論理の定理を半自動で証明することを可能にしてくれるツールです。去年の末、「テスト？ちがうちがう。これからの時代は証明だよ！」という話になったので、どうせOCam…