Non-Trivial Symbolic Computations in Proof Planning

11 years 3 months ago
Non-Trivial Symbolic Computations in Proof Planning
Abstract. We discuss a pragmatic approach to integrate 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.
Volker Sorge
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Authors Volker Sorge
Comments (0)