5.12 Proving Theorems Using the blast Method Isabelleのclassical reasonerは自動証明のためのツールの一つであり、その中でも最も重要なメソッドがblastです。述語論理の例から見ていきます。次の例はAndrew's challengeと呼ばれ、自動証明が難しいとさ…