Computer Science ›› 2015, Vol. 42 ›› Issue (4): 31-36.doi: 10.11896/j.issn.1002-137X.2015.04.004

Previous Articles     Next Articles

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

[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

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!