The Formalization of Discrete Fourier Transform in HOL
The Formalization of Discrete Fourier Transform in HOL
复制标题
HOL 中离散傅立叶变换的形式化
DOI：
10.1155/2015/687152
复制
发表时间：
2015-10
影响因子：
--
通讯作者：
Jie Zhang
中科院分区：
文献类型：
--
作者：
Yupeng Zhang;Yong Guan;Liming Li;Jie Zhang
传统上，离散傅立叶变换（DFT）是用数值或符号计算来执行的，这不能保证100%准确的分析，这对于安全关键应用可能是必要的。机器定理证明是一种形式化的方法，它能在一定程度上完成精确的分析。本文提出了一个高阶逻辑定理证明器HOL中DFT的形式化。给出了DFT的形式化定义，并验证了DFT的基本性质。两个案例研究，以说明有效性和正确性的形式化DFT，包括快速傅立叶变换（FFT）和余弦频移的形式验证。
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.
登录
查看更多内容
影响因子：
0.7
作者：
Liya Liu;O. Hasan;S. Tahar
通讯作者：
Liya Liu;O. Hasan;S. Tahar
DOI：
10.1007/978-1-4612-3658-0_10
发表时间：
1989-05
期刊：
--
影响因子：
--
作者：
M. Gordon
通讯作者：
M. Gordon
影响因子：
0.8
作者：
J. Harrison
通讯作者：
J. Harrison
HOL4 中矩阵理论的形式化
影响因子：
2.1
作者：
Shi, Zhiping;Zhang, Yan;Song, Xiaoyu
通讯作者：
Song, Xiaoyu
HOL4 中复数论的形式化
影响因子：
--
作者：
YONG GUAN;XIAOYU SONG;MINHUA WU;JIE ZHANG
通讯作者：
JIE ZHANG