Non-Trivial Symbolic Computations in Proof Planning

Abstract. We discuss a pragmatic approach tointegrate computer algebra into proof planning. It is based on the idea to separate computation and veri cation and can thereby exploit the fact that many elaborate symbolic computations are trivially checked. In proof planning the separation is realized by using a powerful computer algebra system during the planning process to do non-trivial symbolic computations. Results of these computations are checked during the re nement of a proof plan to a calculus level proof using a small, self-implemented, system that gives us protocol information on its calculation. This protocol can be easily expanded into a checkable low-level calculus proof ensuring the correctness of the computation. We demonstrate our approach with the concrete implementation in the mega system.