Proof planning in Maple

Abstract. We are building a system that helps us mix proof with com-putation. On the one hand, theorem proving tools are often good at helping us construct proofs but poor at doing algebraic computations within these proofs. On the other hand, computer algebra systems are good at doing algebraic computations but usually lack the ability to construct proofs. To tackle this problem, we are adding theorem proving capabilities to the computer algebra system Maple. To make the system easy to extend and to apply to new domains, we have built a simple \proof planning " shell, called CLAM-Lite in which the proof methods are declaratively and explicitly represented. To test the system, we have developed some simple methods for reasoning inductively about summa-tion.