声明
摘要
第一章 绪论
1.1 研究背景和意义
1.2 国内外研究现状
1.2.1 定理证明的研究现状
1.2.2 遗传算法形式化的研究现状
1.3 本文的主要研究内容及贡献
1.4 本文的组织结构
第二章 形式化方法概述
2.1 形式化方法简介
2.2 交互式定理证明器
2.3 HOL系统简介
2.4 本章小结
第三章 交叉操作的形式化
3.2 交叉操作的定义及预备工作
3.3 交叉操作的一般化结构模型
3.4 一般化模型的高阶逻辑表示
3.4.1 染色体的高阶逻辑描述
3.4.2 交叉项的高阶逻辑描述
3.4.3 基本操作的高阶逻辑描述
3.5 交叉操作的形式化建模
3.6 交叉操作的高阶逻辑描述
3.7 交叉操作中基本操作性质的形式化证明
3.7.1 基本操作性质的高阶逻辑描述
3.7.2 基本操作性质的形式化证明
3.7 难点及解决方案
3.8 本章小结
第四章 交叉算子在HOL4系统中的形式化
4.1 研究动机
4.2 单点交叉算子的形式化
4.2.1 单点交叉算子的形式化实现
4.2.2 单点交叉算子性质的证明
4.3 多点交叉算子的形式化
4.3.1 多点交叉算子的形式化实现
4.3.2 多点交叉算子性质的证明
4.4 难点及解决方案
4.5 本章小结
第五章 形式化的交叉算子的应用
5.1 形式化的交叉算子的应用
5.2 本章小结
第六章 总结与展望
6.1 总结
6.2 展望
参考文献
致谢
研究成果及发表的论文
作者与导师简介