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

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

作　　者：吕兴利 施智平[1] 李晓娟[1] 关永[1] 叶世伟[2] 张杰[3] 

机构地区：[1]首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心,北京100048 [2]中国科学院研究生院信息科学与工程学院,北京100049 [3]北京化工大学信息科学与技术学院,北京100029

出　　处：《计算机科学》2015年第4期31-36,共6页Computer Science

基　　金：国际科技合作计划(2010DFB10930;2011DFG13000);国家自然科学基金项目(60873006;61070049;61170304;61104035;61373034;61303014);北京市自然科学基金暨北京市教委重点项目(4122017;KZ201210028 036);北京市优秀人才培养项目;北京市属高校青年拔尖人才培育计划资助

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]