Planning and Patching Proof

We describe proof planning: a technique for both describing the hierarchical structure of proofs and then using this structure to guide proof attempts. When such a proof attempt fails, these failures can be analyzed and a patch formulated and applied. We also describe rippling: a powerful proof method used in proof planning. We pose and answer a number of common questions about proof planning and rippling.

• Type: Conference
• Year: 2004
• Where: AISC
• Authors: Alan Bundy
• Keywords: AISC 2004, Artificial Intelligence, Powerful Proof Method, Proof Attempt, Proof Planning