The Formalization of Discrete Fourier Transform in HOL
Joint Authors
Guan, Yong
Zhang, Yupeng
Li, Liming
Zhang, Jie
Shi, Zhiping
Source
Mathematical Problems in Engineering
Issue
Vol. 2015, Issue 2015 (31 Dec. 2015), pp.1-8, 8 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2015-10-28
Country of Publication
Egypt
No. of Pages
8
Main Subjects
Abstract EN
Traditionally, Discrete Fourier Transform (DFT) is performed with numerical or symbolic computation, which cannot guarantee 100% accurate analysis which may be necessary for safety-critical applications.
Machine theorem proving is one of the formal methods that perform accurate analysis with completeness to some extent.
This paper proposes the formalization of DFT in a higher-order logic theorem prover named HOL.
We propose the formal definition of DFT and verify the fundamental properties of DFT.
Two case studies are presented to illustrate usefulness and correctness of the formalized DFT, including formal verifications of Fast Fourier Transform (FFT) and cosine frequency shift.
American Psychological Association (APA)
Shi, Zhiping& Zhang, Yupeng& Guan, Yong& Li, Liming& Zhang, Jie. 2015. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering،Vol. 2015, no. 2015, pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
Modern Language Association (MLA)
Shi, Zhiping…[et al.]. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering No. 2015 (2015), pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
American Medical Association (AMA)
Shi, Zhiping& Zhang, Yupeng& Guan, Yong& Li, Liming& Zhang, Jie. The Formalization of Discrete Fourier Transform in HOL. Mathematical Problems in Engineering. 2015. Vol. 2015, no. 2015, pp.1-8.
https://search.emarefa.net/detail/BIM-1074468
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-1074468