基于移动互联网的几何证明系统的研究与实现
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 第一章 绪论 | 第10-14页 |
| ·研究背景 | 第10-12页 |
| ·国内外研究现状 | 第12页 |
| ·研究内容 | 第12-13页 |
| ·论文组织结构 | 第13-14页 |
| 第二章 相关理论与技术概述 | 第14-28页 |
| ·移动互联网概述 | 第14-18页 |
| ·移动互联网的定义 | 第14-15页 |
| ·移动互联网的特点 | 第15页 |
| ·移动互联网的目标 | 第15-16页 |
| ·移动互联网的支撑协议 | 第16-18页 |
| ·移动互联网的发展历史和趋势 | 第18-19页 |
| ·发展历史 | 第18页 |
| ·发展趋势 | 第18-19页 |
| ·移动互联网开发技术 | 第19-22页 |
| ·iOS 开发技术 | 第20-21页 |
| ·Android 开发技术 | 第21-22页 |
| ·定理自动证明概述 | 第22-23页 |
| ·定理自动证明的发展历史 | 第23-25页 |
| ·起步阶段 | 第23-24页 |
| ·活跃阶段 | 第24-25页 |
| ·近期阶段 | 第25页 |
| ·定理自动证明的方法 | 第25-27页 |
| ·代数法 | 第25-26页 |
| ·综合法 | 第26页 |
| ·消点法 | 第26页 |
| ·三种方法的比较 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第三章 几何命题的描述与输入 | 第28-38页 |
| ·几何命题的描述 | 第28-32页 |
| ·一阶逻辑 | 第28-29页 |
| ·几何对象的谓词表示 | 第29-30页 |
| ·几何关系谓词 | 第30-32页 |
| ·举例 | 第32页 |
| ·几何命题的输入形式 | 第32-35页 |
| ·构造形式 | 第33-34页 |
| ·谓词形式 | 第34-35页 |
| ·面向对象的形式化命题的构造输入 | 第35-37页 |
| ·本章小结 | 第37-38页 |
| 第四章 定理自动证明的研究 | 第38-47页 |
| ·基于规则的推理 | 第38-40页 |
| ·前推搜索算法 | 第40-41页 |
| ·证明系统的研究 | 第41-46页 |
| ·系统简介 | 第42-43页 |
| ·证明系统的源码剖析 | 第43-45页 |
| ·系统的编译 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 第五章 系统的设计与实现 | 第47-79页 |
| ·需求分析 | 第47-49页 |
| ·功能需求分析 | 第47-49页 |
| ·性能需求分析 | 第49页 |
| ·总体设计 | 第49-50页 |
| ·画板模块的设计 | 第50-53页 |
| ·概述 | 第50页 |
| ·功能模块设计 | 第50-52页 |
| ·类图设计 | 第52-53页 |
| ·证明服务器的设计 | 第53-56页 |
| ·服务器模型 | 第53-54页 |
| ·详细功能设计 | 第54-55页 |
| ·工作流程 | 第55-56页 |
| ·画板模块的实现 | 第56-66页 |
| ·图元类的实现 | 第56-60页 |
| ·功能类的实现 | 第60-63页 |
| ·几何对象的组织 | 第63-64页 |
| ·面向对象的形式化命题构造 | 第64-66页 |
| ·证明服务器的实现 | 第66-75页 |
| ·证明系统模块的实现 | 第66-72页 |
| ·服务器主线程的实现 | 第72-73页 |
| ·服务器子线程的实现 | 第73-74页 |
| ·日志模块的实现 | 第74-75页 |
| ·系统展示 | 第75-78页 |
| ·本章小结 | 第78-79页 |
| 第六章 总结与展望 | 第79-81页 |
| ·总结 | 第79页 |
| ·展望 | 第79-81页 |
| 致谢 | 第81-82页 |
| 参考文献 | 第82-84页 |
| 在学期间的研究成果 | 第84-85页 |
