An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs
Manfred Kerber, Michael Kohlhase, Volker Sorge · 1999
Mechanised reasoning systems and computer algebra systems have apparently di erent objectives. Their integration is, however, highly desirable, since in many formal proofs both of the two di erent tasks, proving and calculating, have to be performed. Even more importantly, proof and computation are often interwoven and not easily separable. In the context of producing reliable proofs, the question how to ensure correctness when integrating a computer algebra system into a mechanised reasoning system is crucial. In this contribution, we discuss the correctness problems that arise from such an integration and advocate an approach in which the calculations of the computer algebra system are checked at the calculus level of the mechanised reasoning system. This can be achieved by adding a verbose mode to the computer algebra system which produces high-level protocol information that can be processed by an interface to derive proof plans. Such a proof plan in turn can be expanded to proofs at di erent levels of abstraction, so the approach iswell-suited for producing a high-level verbalised explication as well as for a low-level machine checkable calculus-level proof. We present an implementation of our ideas and exemplify them using an automatically solved extended example. Changes in the criterion of `rigour of the proof ' engender major revolutions in mathematics 1 H. Poincare, 1905