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

Examensarbete för kandidatexamen

Använd denna länk för att citera eller länka till detta dokument: https://hdl.handle.net/20.500.12380/203645
Ladda ner:
Fil Beskrivning StorlekFormat 
203645.pdfFulltext886.37 kBAdobe PDFVisa
Typ: Examensarbete för kandidatexamen
Bachelor Thesis
Titel: Formalisering av algoritmer och matematiska bevis En formalisering av Toom-Cook algoritmen i Coq med SSReflect
Författare: Andersson, Jesper
Lideström, Åsa
Oom, Daniel
Sjöberg, Anders
Ståhl, Niclas
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.
Nyckelord: Data- och informationsvetenskap;Computer and Information Science
Utgivningsdatum: 2014
Utgivare: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/203645
Samling:Examensarbeten för kandidatexamen // Bachelor Theses



Materialet i Chalmers öppna arkiv är upphovsrättsligt skyddat och får ej användas i kommersiellt syfte!