Can proof planning be applied to non-mathematical domains?
Yes. We have had some success applying proof planning to game playing (Bridge and Go) and to configuration problems. It is potentially applicable wherever there are common patterns of reasoning. Proof planning can be used to match the problem to the reasoning method in a process of meta-level reasoning. Proof planning gives a clean separation between the factual and search control information, which facilitates their independent modification. Here is a pointer to the research on automating bridge done in my research group. An introduction to our work on configuration is: Lowe, H., Pechoucek, M. and Bundy, A. Proof Planning and Configuration, in “Proceedings of the Ninth Exhibition and Symposium on Industrial Applications of Prolog”, 1996. • 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 ripp
