Formalisering av algoritmer och matematiska bevis En formalisering av Toom-Cook algoritmen i Coq med SSReflect
Ladda ner
Typ
Examensarbete för kandidatexamen
Bachelor Thesis
Bachelor Thesis
Program
Datateknik 300 hp (civilingenjör)
Publicerad
2014
Författare
Andersson, Jesper
Lideström, Åsa
Oom, Daniel
Sjöberg, Anders
Ståhl, Niclas
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science