项目名称: 希尔伯特空间以及矩阵理论在HOL4中的形式化

项目编号: No.61170304

项目类型: 面上项目

立项/批准年度: 2012

项目学科: 计算机科学学科

项目作者: 施智平

作者单位: 首都师范大学

项目金额: 52万元

中文摘要: 定理证明方法可以用于任何能被数学模型表示的系统,不受状态数限制,是非常理想的验证方法,而定理库的构建是定理证明应用的关键问题。矩阵是线性变换的算子,在信息系统中应用广泛。在定理证明器中系统地构建矩阵理论和线性变换理论将会极大地提高定理证明器的建模和推理能力。本项目研究有限维希尔伯特空间以及矩阵理论的形式化方法,研究线性变换性质的形式化方法,包括相关性、对称性、正交性和同构性,并在高阶逻辑定理证明环境HOL4中开发相应的定理库,构建以矩阵理论为核心的定理证明体系,在国际上公开发布HOL4矩阵定理库,推动HOL4在时间状态变换和空间变换系统的验证中的应用,提高我国在定理证明基础平台构建领域的国际影响力。基于所研发的矩阵定理库,用定理证明方法验证SpaceWire总线的发送接收、编码模块和总线控制模块,示范矩阵定理库的应用。

中文关键词: 希尔伯特空间;gauge积分理论;矩阵理论;高阶逻辑;旋量理论

英文摘要:

英文关键词: Hilbert space;gauge integral;matrix theory;higher-order logic;screw theory

成为VIP会员查看完整内容
0

相关内容

人工智能技术在口腔正畸诊疗中的应用研究进展
专知会员服务
13+阅读 · 2022年5月1日
人工智能技术在智能武器装备的研究与应用
专知会员服务
157+阅读 · 2022年4月13日
《过参数化机器学习理论》综述论文
专知会员服务
45+阅读 · 2021年9月19日
专知会员服务
113+阅读 · 2021年7月24日
人工智能的理论及实践 知识图谱,160页pdf
专知会员服务
99+阅读 · 2021年6月30日
干货书《金融数学导论: 概念与计算方法》,290页pdf
专知会员服务
59+阅读 · 2021年5月7日
专知会员服务
104+阅读 · 2021年3月23日
【干货书】金融数学概念和计算方法的导论,290页pdf
专知会员服务
57+阅读 · 2020年11月16日
智能合约的形式化验证方法研究综述
专知
13+阅读 · 2021年5月8日
【斯坦福经典书】熵与信息论,311页pdf
专知
3+阅读 · 2021年3月23日
最新《图理论》笔记书,98页pdf
专知
48+阅读 · 2020年12月27日
图表示学习Graph Embedding综述
AINLP
32+阅读 · 2020年5月17日
知识图谱嵌入(KGE):方法和应用的综述
专知
53+阅读 · 2019年8月25日
图嵌入(Graph embedding)综述
人工智能前沿讲习班
448+阅读 · 2019年4月30日
形式化方法的研究进展与趋势
中国计算机学会
34+阅读 · 2018年11月8日
贝叶斯机器学习前沿进展
架构文摘
12+阅读 · 2018年2月11日
【基础数学】- 01
遇见数学
19+阅读 · 2017年7月25日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
35+阅读 · 2022年3月14日
Transformers in Medical Image Analysis: A Review
Arxiv
39+阅读 · 2022年2月24日
Arxiv
13+阅读 · 2021年6月14日
Arxiv
99+阅读 · 2020年3月4日
Arxiv
11+阅读 · 2018年4月25日
小贴士
相关VIP内容
人工智能技术在口腔正畸诊疗中的应用研究进展
专知会员服务
13+阅读 · 2022年5月1日
人工智能技术在智能武器装备的研究与应用
专知会员服务
157+阅读 · 2022年4月13日
《过参数化机器学习理论》综述论文
专知会员服务
45+阅读 · 2021年9月19日
专知会员服务
113+阅读 · 2021年7月24日
人工智能的理论及实践 知识图谱,160页pdf
专知会员服务
99+阅读 · 2021年6月30日
干货书《金融数学导论: 概念与计算方法》,290页pdf
专知会员服务
59+阅读 · 2021年5月7日
专知会员服务
104+阅读 · 2021年3月23日
【干货书】金融数学概念和计算方法的导论,290页pdf
专知会员服务
57+阅读 · 2020年11月16日
相关资讯
智能合约的形式化验证方法研究综述
专知
13+阅读 · 2021年5月8日
【斯坦福经典书】熵与信息论,311页pdf
专知
3+阅读 · 2021年3月23日
最新《图理论》笔记书,98页pdf
专知
48+阅读 · 2020年12月27日
图表示学习Graph Embedding综述
AINLP
32+阅读 · 2020年5月17日
知识图谱嵌入(KGE):方法和应用的综述
专知
53+阅读 · 2019年8月25日
图嵌入(Graph embedding)综述
人工智能前沿讲习班
448+阅读 · 2019年4月30日
形式化方法的研究进展与趋势
中国计算机学会
34+阅读 · 2018年11月8日
贝叶斯机器学习前沿进展
架构文摘
12+阅读 · 2018年2月11日
【基础数学】- 01
遇见数学
19+阅读 · 2017年7月25日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
相关论文
Arxiv
35+阅读 · 2022年3月14日
Transformers in Medical Image Analysis: A Review
Arxiv
39+阅读 · 2022年2月24日
Arxiv
13+阅读 · 2021年6月14日
Arxiv
99+阅读 · 2020年3月4日
Arxiv
11+阅读 · 2018年4月25日
微信扫码咨询专知VIP会员