## An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs

• Mechanised reasoning systems and computer algebra systems have apparentlydifferent objectives. Their integration is, however, highly desirable, since in manyformal proofs both of the two different tasks, proving and calculating, have to beperformed. Even more importantly, proof and computation are often interwoven andnot easily separable. In the context of producing reliable proofs, the question howto ensure correctness when integrating a computer algebra system into a mechanisedreasoning system is crucial. In this contribution, we discuss the correctness prob-lems that arise from such an integration and advocate an approach in which thecalculations of the computer algebra system are checked at the calculus level of themechanised reasoning system. This can be achieved by adding a verbose mode to thecomputer algebra system which produces high-level protocol information that can beprocessed by an interface to derive proof plans. Such a proof plan in turn can beexpanded to proofs at different levels of abstraction, so the approach is well-suited forproducing a high-level verbalised explication as well as for a low-level machine check-able calculus-level proof. We present an implementation of our ideas and exemplifythem using an automatically solved extended example.

### Additional Services

Author: Manfred Kerber, Michael Kohlhase, Volker Sorge urn:nbn:de:hbz:386-kluedo-3632 SEKI Report (96,6) Preprint English 1999 1999 Technische Universität Kaiserslautern 2000/04/03 Fachbereich Informatik 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$