Experiments with Proof Plans for Induction

Abstraction, in contrast to meta-level inference, works with a degenerate version of the object-level space in which some essential detail is thrown away. Because abstract plans are strongly tied to the object-level space, they are limited in their expressive power.