The Formalization of Discrete Fourier Transform in HOL

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...

Full description

Bibliographic Details
Main Authors: Zhiping Shi, Yupeng Zhang, Yong Guan, Liming Li, Jie Zhang
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

Similar Items