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

• 作者: 关永 叶世伟 吕兴利 张杰 施智平 李晓娟
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 形式化方法 定理证明 连续傅里叶变换 HOL4 频率响应
• 年，卷（期）: 2015,（4）
• 页码范围: 31-36
• 页数: 6页
• 分类号: TP301.2
• 字数: 7638字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2015.4.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	关永	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	95	1336	17.0	33.0
3	李晓娟	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	39	261	9.0	14.0
4	叶世伟	中国科学院研究生院信息科学与工程学院	30	250	8.0	15.0
5	施智平	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	24	145	8.0	11.0
6	吕兴利	首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心	1	2	1.0	1.0