Affiliations: Fakultät für Informatik, Universität Karlsruhe, Karlsruhe, Germany. ballarin@ira.uka.de | Computer Laboratory, University of Cambridge, Cambridge, UK. lcp@cl.cam.ac.uk
Note: [] Address for correspondence: Fakultät für Informatik, Universität Karlsruhe, Karlsruhe, Germany Research was carried out while at the Computer Laboratory, University of Cambridge.
Note: [] Address for correspondence: Computer Laboratory, University of Cambridge, Cambridge, UK
Abstract: The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports this claim: the mechanised proofs depend on non-trivial algorithms from computer algebra and increase the reasoning power of the theorem prover. The unsoundness of computer algebra systems is a major problem in interfacing them to theorem provers. Our approach to obtaining a sound overall system is not blanket distrust but based on the distinction between algorithms we call sound and ad hoc respectively. This distinction is blurred in most computer algebra systems. Our experimental interface therefore uses a computer algebra library. It is based on formal specifications for the algorithms, and links the computer algebra library Sumit to the prover Isabelle. We give details of the interface, the use of the computer algebra system on the tactic-level of Isabelle and its integration into proof procedures.
Keywords: Computer algebra, mechanised reasoning, combining systems, soundness of computer algebra systems, specialisation problem, coding theory
