In English

Formalisering av algoritmer och matematiska bevis En formalisering av Toom-Cook algoritmen i Coq med SSReflect

Jesper Andersson ; Åsa Lideström ; Daniel Oom ; Anders Sjöberg ; Niclas Ståhl
Göteborg : Chalmers tekniska högskola, 2014. 63 s.
[Examensarbete för kandidatexamen]

Computer-aided formalization of mathematics has progressed in the last decade with the formalization of very large and complex proofs such as the proof of the Four color theorem and the Feit-Thompson theorem. In this report we present a formal proof of the Toom-Cook algorithm using the Coq proof assistant together with the SSReflect extension. The Toom-Cook algorithm is used to multiply polynomials and can also be used for integer multiplication.



Publikationen registrerades 2014-10-02. Den ändrades senast 2014-10-15

CPL ID: 203645

Detta är en tjänst från Chalmers bibliotek