定理证明器Coq的理论扩展与在组合逻辑验证中的应用
发布时间：2022-12-18 17:23
交互式定理证明技术是可以应用于大规模系统验证的重要的形式化方法，近年有一些影响很广的成功案例。但是交互式定理证明的使用难度以及对使用人员的严重依赖阻碍了其在工业界的发展。本文围绕主流的交互式定理证明工具之一的Coq，总结了其应用过程中的问题，分析了问题的原因，并在此基础上从其基础理论和应用实践两方面入手尝试提高Coq在实际应用过程中的易用性。在理论方面，针对Coq在使用中对依赖类型等价关系判定能力不足的问题，对Coq基础理论进行了扩展，并通过验证扩展后理论的主要性质，保证扩展的理论同样可以应用于实现定理证明工具。在应用实践方面，针对组合逻辑提出了基于Coq的验证框架。该框架提供了对组合逻辑建模验证的统一方法，也提供了面向组合逻辑验证的扩展库。对算术计算逻辑单元的实际验证工作说明了该框架的可用性和易用性。本文的主要工作包含以下几个方面： 1.扩展了Coq的基础理论：归纳构造演算。在内涵式的归纳构造演算等价判定的基础上增加了外延式等价关系的判定能力，并且给出了扩展理论应用于实现定理证明工具的机制。外延式理论是抽象表示的，并被一些约束所限制，所有满足限制的外延式理论都可以被扩充进归纳构...
【文章页数】：129 页
【学位级别】：博士
【文章目录】：
摘要
Abstract
主要符号对照表
第1章 绪论
1.1 研究背景
1.2 研究现状
1.3 研究思路
1.3.1 定理证明技术应用问题
1.3.2 针对性改进方案的思路
1.4 预备知识
1.4.1 Coq 的理论基础归纳构造演算
1.4.2 Coq 的语法及功能
1.4.3 Coq 理论与工具之间的联系
1.5 主要贡献
1.6 论文结构
第2章 Coq 基础类型论 CIC 的扩展理论 CIC~ωT
2.1 引言
2.1.1 问题描述
2.1.2 问题分析与解决思路
2.1.3 工作难点及相关工作
2.1.4 本章结构
2.2 CIC~ωT的定义
2.2.1 理论的定义
2.2.2 类型系统部分的定义
2.3 CIC~ωT的主要性质及证明
2.3.1 汇合性
2.3.2 相关性
2.3.3 类型保持性
2.3.4 语义方面的性质
2.3.5 类型检查的可判定性
2.4 本章小结
第3章 CIC~ωT语义性质的形式化证明
3.1 引言
3.1.1 类型系统逻辑自洽性和计算中止性的证明思路
3.1.2 深层嵌入和浅层嵌入
3.1.3 本章结构
3.2 CC 模型及扩展构造的 CIC 模型
3.2.1 抽象模块
3.2.2 元模型及性质
3.2.3 CC 模型及性质
3.2.4 CIC 模型及性质
3.3 CIC~ωT抽象模型及性质证明
3.3.1 CIC~ωT模型构造
3.3.2 CIC~ωT模型可靠性证明
3.4 可嵌入外延式理论实例：Presburger 算术
3.4.1 Presburger 代数的签名
3.4.2 Presburger 代数的公理
3.5 本章小结
第4章 基于 Coq 的组合逻辑验证框架
4.1 引言
4.1.1 工具和领域选择
4.1.2 框架的特点
4.1.3 本章结构
4.2 组合逻辑验证框架介绍
4.2.1 领域库
4.2.2 功能描述
4.2.3 性质描述
4.2.4 证明管理
4.3 组合逻辑验证框架特点
4.3.1 真实性
4.3.2 灵活性
4.3.3 模块化
4.3.4 扩展库的丰富性和可扩展性
4.4 本章小结
第5章 基于组合逻辑验证框架的应用实例
5.1 引言
5.1.1 基本加法器验证的相关工作
5.1.2 并行前缀循环进位加法器验证的相关工作
5.1.3 本章结构
5.2 Ling 加法器验证
5.2.1 Ling 加法器介绍
5.2.2 框架下 Ling 加法器的验证
5.2.3 框架下 Ling 加法器扩展的验证
5.3 并行前缀加法器验证
5.3.1 并行前缀加法器介绍
5.3.2 并行前缀树的抽象模块
5.3.3 半具体的通用并行前缀加法器验证
5.3.4 具体到某种特定实现的并行前缀加法器验证
5.4 并行前缀循环进位加法器验证
5.4.1 并行前缀循环进位加法器结构及基本组件介绍
5.4.2 并行前缀循环进位加法器内核结构及证明
5.4.3 并行前缀循环进位加法器正确性证明
5.5 本章小结
第6章 结语
6.1 工作总结
6.2 研究展望
参考文献
致谢
个人简历、在学期间发表的学术论文与研究成果
本文编号：3722456
【文章页数】：129 页
【学位级别】：博士
【文章目录】：
摘要
Abstract
主要符号对照表
第1章 绪论
1.1 研究背景
1.2 研究现状
1.3 研究思路
1.3.1 定理证明技术应用问题
1.3.2 针对性改进方案的思路
1.4 预备知识
1.4.1 Coq 的理论基础归纳构造演算
1.4.2 Coq 的语法及功能
1.4.3 Coq 理论与工具之间的联系
1.5 主要贡献
1.6 论文结构
第2章 Coq 基础类型论 CIC 的扩展理论 CIC~ωT
2.1 引言
2.1.1 问题描述
2.1.2 问题分析与解决思路
2.1.3 工作难点及相关工作
2.1.4 本章结构
2.2 CIC~ωT的定义
2.2.1 理论的定义
2.2.2 类型系统部分的定义
2.3 CIC~ωT的主要性质及证明
2.3.1 汇合性
2.3.2 相关性
2.3.3 类型保持性
2.3.4 语义方面的性质
2.3.5 类型检查的可判定性
2.4 本章小结
第3章 CIC~ωT语义性质的形式化证明
3.1 引言
3.1.1 类型系统逻辑自洽性和计算中止性的证明思路
3.1.2 深层嵌入和浅层嵌入
3.1.3 本章结构
3.2 CC 模型及扩展构造的 CIC 模型
3.2.1 抽象模块
3.2.2 元模型及性质
3.2.3 CC 模型及性质
3.2.4 CIC 模型及性质
3.3 CIC~ωT抽象模型及性质证明
3.3.1 CIC~ωT模型构造
3.3.2 CIC~ωT模型可靠性证明
3.4 可嵌入外延式理论实例：Presburger 算术
3.4.1 Presburger 代数的签名
3.4.2 Presburger 代数的公理
3.5 本章小结
第4章 基于 Coq 的组合逻辑验证框架
4.1 引言
4.1.1 工具和领域选择
4.1.2 框架的特点
4.1.3 本章结构
4.2 组合逻辑验证框架介绍
4.2.1 领域库
4.2.2 功能描述
4.2.3 性质描述
4.2.4 证明管理
4.3 组合逻辑验证框架特点
4.3.1 真实性
4.3.2 灵活性
4.3.3 模块化
4.3.4 扩展库的丰富性和可扩展性
4.4 本章小结
第5章 基于组合逻辑验证框架的应用实例
5.1 引言
5.1.1 基本加法器验证的相关工作
5.1.2 并行前缀循环进位加法器验证的相关工作
5.1.3 本章结构
5.2 Ling 加法器验证
5.2.1 Ling 加法器介绍
5.2.2 框架下 Ling 加法器的验证
5.2.3 框架下 Ling 加法器扩展的验证
5.3 并行前缀加法器验证
5.3.1 并行前缀加法器介绍
5.3.2 并行前缀树的抽象模块
5.3.3 半具体的通用并行前缀加法器验证
5.3.4 具体到某种特定实现的并行前缀加法器验证
5.4 并行前缀循环进位加法器验证
5.4.1 并行前缀循环进位加法器结构及基本组件介绍
5.4.2 并行前缀循环进位加法器内核结构及证明
5.4.3 并行前缀循环进位加法器正确性证明
5.5 本章小结
第6章 结语
6.1 工作总结
6.2 研究展望
参考文献
致谢
个人简历、在学期间发表的学术论文与研究成果
本文编号：3722456
本文链接：https://www.wllwen.com/shekelunwen/ljx/3722456.html