What is the relation between proof planning and rippling?
Rippling is a key method in our proof plans for induction. It is also useful in non-inductive domains. However, you can certainly envisage a proof planning system which did not contain a rippling method (the Saarbrücken Omega system, for instance) and you can envisage using rippling, eg as a tactic, in a non-proof planning system. So there is no necessary connection. For more on rippling see the rippling FAQ.
