Is it possible to automate the learning of proof plans?
Yes, from example proofs. We have two PhD projects on this. One automated learning equation solving methods from examples. One automated learning inductive proof methods from examples. Both used forms of explanation based generalisation. The hardest aspect of this is coming up with the key meta-level concepts to describe the method preconditions. An example of such a meta-level concept is wave-front from rippling. We have not made much progress on automating the learning of these. Good references to this work are: Silver, B. Meta-level inference: Representing and Learning Control Information in Artificial Intelligence, North Holland, 1985; and Desimone R. Explanation-Based Learning of Proof Plans in “Machine and Human Learning”, Kogan Page, eds. Kodratoff, Y. and Hutchinson, A, 1989. • Have proof plans been used to teach students mathematics? Not to my knowledge. This sounds like a promising project. Some of our methods do correspond to the kinds of proof techniques used by experts in
