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

来源 :2014湖北省计算机学会学术年会 | 被引量 : 0次 | 上传用户：shumoljw

【摘要】

：

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分

【作者】

：

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

【机构】

：

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

【出处】

：

2014湖北省计算机学会学术年会

【发表日期】

：

2014年10期

【关键词】

：

连续傅里叶变换高阶逻辑定理形式化方法电阻电感电容串联谐振电路频率响应

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

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

其他文献

射阳蚕业的现状与发展对策

射阳县地处苏北沿海，蚕桑业是全县农业经济结构中的优势产业，为地方经济、出口创汇、致富农民作出了较大贡献。笔者现针对射阳县蚕业现状，提出一些发展对策，仅供参考。

期刊

发展对策蚕业农业经济结构苏北沿海优势产业地方经济出口创汇射阳县

庄子的隐逸思想与当代人的舒压

社会主义市场经济条件下，竞争已渗入到人们生活的方方面面，随竞争而来的种种压力也正给人们的工作和学习带来困扰和负担。西方人的舒压思想适合其个人主义、功利主义的文化背景

期刊

庄子舒压竞争隐逸思想

一手抓培育扶持一手抓规范管理——江苏泰州制订社团、民非税收优惠和管理政策规定

2003年江苏省泰州市民政局和财政局联合制订了加强市直社团收费及财务管理的规定,财政局委托民政局负责发放会费收据和结算凭证,各社团统一到民政局购领.五年来,该市执行这一

期刊