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

Saved in:
Bibliographic Details
Published in:Mathematical problems in engineering 2015-01, Vol.2015 (2015), p.1-8
Main Authors: Li, Liming, Guan, Yong, Zhang, Yupeng, Shi, Zhiping, Zhang, Jie
Format: Article
Language:English
Subjects:
Algorithms
Case studies
Completeness
Computation
Engineering
Fast Fourier transformations
Formal method
Fourier transforms
Frequency shift
Logic
Mathematical models
Methods
Metis
Partial differential equations
Safety critical
Signal processing
Software
Theorem proving
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1024-123X
1563-5147
DOI:10.1155/2015/687152