连续傅里叶变换基础理论的高阶逻辑形式化

计算机科学 ›› 2015, Vol. 42 ›› Issue (4): 31-36.doi: 10.11896/j.issn.1002-137X.2015.04.004

连续傅里叶变换基础理论的高阶逻辑形式化

吕兴利,施智平,李晓娟,关永,叶世伟,张杰

首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048,首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心北京100048,中国科学院研究生院信息科学与工程学院北京100049,北京化工大学信息科学与技术学院北京100029

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受国际科技合作计划(2010DFB10930,1DFG13000),国家自然科学基金项目(60873006,9,61170304,5,61373034,4),北京市自然科学基金暨北京市教委重点项目(4122017,KZ201210028036),北京市优秀人才培养项目,北京市属高校青年拔尖人才培育计划资助

Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform

LV Xing-li, SHI Zhi-ping, LI Xiao-juan, GUAN Yong, YE Shi-wei and ZHANG Jie

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： 连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用。利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础。最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用。

关键词: 形式化方法,定理证明,连续傅里叶变换,HOL4,频率响应

Abstract: Continuous Fourier transform (CFT) is widely used in the fields of mathematics and engineering.The definition of CFT and its operational properties were formalized in the higher-order logic theorem prover HOL4,including linearity,frequency shifting,reversion,integration,first-order differention and higher-order differention,which lays the foundation for analyzing related systems by formal methods.Finally,the frequency response of resistance inductance capacitance(RLC) series resonant circuit was verified by the theorem proving method,which illustrates a preliminary application of formalized CFT.

Key words: Formal methods,Theorem proving,Continuous Fourier transform,HOL4,Frequency response

吕兴利,施智平,李晓娟,关永,叶世伟,张杰. 连续傅里叶变换基础理论的高阶逻辑形式化[J]. 计算机科学, 2015, 42(4): 31-36. https://doi.org/10.11896/j.issn.1002-137X.2015.04.004

LV Xing-li, SHI Zhi-ping, LI Xiao-juan, GUAN Yong, YE Shi-wei and ZHANG Jie. Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform[J]. Computer Science, 2015, 42(4): 31-36. https://doi.org/10.11896/j.issn.1002-137X.2015.04.004

参考文献

[1] 韩俊刚,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001
[2] Slind,Konrad,Norrish M.A brief overview of HOL4.Theorem Proving in Higher Order Logics[M].Springer Berlin Heidelberg,2008:28-32
[3] http://hol.sourceforge.net/
[4] Akbarpour B.Modeling and Verification of DSP Designsin HOL[D].Montreal,Quebec,Canada:Department of Electrical and Computer Engineering,Concordia University,Aprial 2005
[5] Harrison J,Théry L.Extending the HOL theorem prover with acomputer algebra system to reason about the reals[M]∥Higher Order Logic Theorem Proving and Its Applications.Springer Berlin Heidelberg,1994:174-184
[6] 张玉鹏,施智平,关永,等.SpaceWire 译码电路在HOL4中的形式化验证[J].小型微型计算机系统,2013,8:1959-1963
[7] Abdullah A N M,Akbarpour B,Tahar S.Formal analysis and verification of an OFDM modem design using HOL[C]∥Formal Methods in Computer Aided Design,2006(FMCAD’06).IEEE,2006:189-190
[8] 盖云英,包革军,等.复变函数与积分变换[M].北京:科学出版社,2006
[9] 曾禹村,张宝俊,等.信号与系统[M].北京:北京理工大学出版社,2008
[10] Bracewell R N.The Fourier transform and its applications[M].New York,1965
[11] Taqdees S H,Hasan O.Formalization of Laplace TransformUsing the Multivariable Calculus Theory of HOL-Light[C]∥Logic for Programming,Artificial Intelligence,and Reasoning.Springer Berlin Heidelberg.New York:McGraw-Hill,1986,2013:744-758
[12] HarrisonJ.Theorem Proving with the Real Numbers [R].Technical Report number 408,University of Cambridge Computer Laboratory,December 1996
[13] 谷伟卿,施智平,关永,等.Gauge积分在HOL4中的形式化[J].计算机科学,2013,0(2):191-194
[14] Siddique U,Hasan O.Formal analysis of fractional order sys-tems in HOL[C]∥Computer-Aided Design (FMCAD).IEEE,2011:163-170
[15] 华东师范大学数学系.数学分析[M].北京:高等教育出版社,2006

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed