The Formalization of Discrete Fourier Transform in HOL
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 complet...
Main Authors: | , , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Hindawi Limited
2015-01-01
|
Series: | Mathematical Problems in Engineering |
Online Access: | http://dx.doi.org/10.1155/2015/687152 |
id |
doaj-2f31237310d946d38a5e514973fb28ce |
---|---|
record_format |
Article |
spelling |
doaj-2f31237310d946d38a5e514973fb28ce2020-11-24T23:46:52ZengHindawi LimitedMathematical Problems in Engineering1024-123X1563-51472015-01-01201510.1155/2015/687152687152The Formalization of Discrete Fourier Transform in HOLZhiping Shi0Yupeng Zhang1Yong Guan2Liming Li3Jie Zhang4Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, ChinaBeijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, ChinaBeijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, ChinaBeijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, ChinaCollege of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, ChinaTraditionally, 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.http://dx.doi.org/10.1155/2015/687152 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Zhiping Shi Yupeng Zhang Yong Guan Liming Li Jie Zhang |
spellingShingle |
Zhiping Shi Yupeng Zhang Yong Guan Liming Li Jie Zhang The Formalization of Discrete Fourier Transform in HOL Mathematical Problems in Engineering |
author_facet |
Zhiping Shi Yupeng Zhang Yong Guan Liming Li Jie Zhang |
author_sort |
Zhiping Shi |
title |
The Formalization of Discrete Fourier Transform in HOL |
title_short |
The Formalization of Discrete Fourier Transform in HOL |
title_full |
The Formalization of Discrete Fourier Transform in HOL |
title_fullStr |
The Formalization of Discrete Fourier Transform in HOL |
title_full_unstemmed |
The Formalization of Discrete Fourier Transform in HOL |
title_sort |
formalization of discrete fourier transform in hol |
publisher |
Hindawi Limited |
series |
Mathematical Problems in Engineering |
issn |
1024-123X 1563-5147 |
publishDate |
2015-01-01 |
description |
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. |
url |
http://dx.doi.org/10.1155/2015/687152 |
work_keys_str_mv |
AT zhipingshi theformalizationofdiscretefouriertransforminhol AT yupengzhang theformalizationofdiscretefouriertransforminhol AT yongguan theformalizationofdiscretefouriertransforminhol AT limingli theformalizationofdiscretefouriertransforminhol AT jiezhang theformalizationofdiscretefouriertransforminhol AT zhipingshi formalizationofdiscretefouriertransforminhol AT yupengzhang formalizationofdiscretefouriertransforminhol AT yongguan formalizationofdiscretefouriertransforminhol AT limingli formalizationofdiscretefouriertransforminhol AT jiezhang formalizationofdiscretefouriertransforminhol |
_version_ |
1725492016235675648 |