A Pragmatic Approach to Extending Provers by Computer Algebra — with Applications to Coding Theory
Clemens Ballarin, Lawrence Charles Paulson · Fundamenta Informaticae · 1999
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