基于高级逻辑的交叉算子的形式化研究
| 摘要 | 第4-6页 |
| ABSTRACT | 第6-7页 |
| 第一章 绪论 | 第12-20页 |
| 1.1 研究背景和意义 | 第12-13页 |
| 1.2 国内外研究现状 | 第13-16页 |
| 1.2.1 定理证明的研究现状 | 第13-14页 |
| 1.2.2 遗传算法形式化的研究现状 | 第14-16页 |
| 1.3 本文的主要研究内容及贡献 | 第16-17页 |
| 1.4 本文的组织结构 | 第17-20页 |
| 第二章 形式化方法概述 | 第20-28页 |
| 2.1 形式化方法简介 | 第20-23页 |
| 2.2 交互式定理证明器 | 第23-24页 |
| 2.3 HOL系统简介 | 第24-26页 |
| 2.4 本章小结 | 第26-28页 |
| 第三章 交叉操作的形式化 | 第28-48页 |
| 3.1 研究动机 | 第28页 |
| 3.2 交叉操作的定义及预备工作 | 第28-29页 |
| 3.3 交叉操作的一般化结构模型 | 第29-30页 |
| 3.4 一般化模型的高阶逻辑表示 | 第30-32页 |
| 3.4.1 染色体的高阶逻辑描述 | 第30-31页 |
| 3.4.2 交叉项的高阶逻辑描述 | 第31页 |
| 3.4.3 基本操作的高阶逻辑描述 | 第31-32页 |
| 3.5 交叉操作的形式化建模 | 第32-35页 |
| 3.6 交叉操作的高阶逻辑描述 | 第35页 |
| 3.7 交叉操作中基本操作性质的形式化证明 | 第35-44页 |
| 3.7.1 基本操作性质的高阶逻辑描述 | 第35-37页 |
| 3.7.2 基本操作性质的形式化证明 | 第37-44页 |
| 3.8 难点及解决方案 | 第44-45页 |
| 3.9 本章小结 | 第45-48页 |
| 第四章 交叉算子在HOL4系统中的形式化 | 第48-62页 |
| 4.1 研究动机 | 第48页 |
| 4.2 单点交叉算子的形式化 | 第48-51页 |
| 4.2.1 单点交叉算子的形式化实现 | 第48-49页 |
| 4.2.2 单点交叉算子性质的证明 | 第49-51页 |
| 4.3 多点交叉算子的形式化 | 第51-59页 |
| 4.3.1 多点交叉算子的形式化实现 | 第52页 |
| 4.3.2 多点交叉算子性质的证明 | 第52-59页 |
| 4.4 难点及解决方案 | 第59-60页 |
| 4.5 本章小结 | 第60-62页 |
| 第五章 形式化的交叉算子的应用 | 第62-66页 |
| 5.1 形式化的交叉算子的应用 | 第62-65页 |
| 5.2 本章小结 | 第65-66页 |
| 第六章 总结与展望 | 第66-68页 |
| 6.1 总结 | 第66-67页 |
| 6.2 展望 | 第67-68页 |
| 参考文献 | 第68-72页 |
| 致谢 | 第72-74页 |
| 研究成果及发表的论文 | 第74-76页 |
| 作者与导师简介 | 第76-78页 |
| 附件 | 第78-79页 |
