Reasoning about coding theory: The benefits we get from computer algebra

The use of computer algebra is usually considered beneflcial 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 com- puter algebra and increase the reasoning power of the theorem prover. The unsoundness of computer algebra systems is a major problem in in- terfacing them to theorem provers. Our approach to obtaining a sound overall system is not blanket distrust but based on the distinction be- tween 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 theorem tem- plates, which provide formal speciflcations for the algorithms. Keywords. Computer algebra, mechanised reasoning, combining sys- tems, soundness of computer algebra systems, specialisation problem, coding theory. AISC topics. Integration of logical reasoning and computer algebra, automated theorem provers.