初等代数证明题答案的自动检测方法研究
| 中文摘要 | 第1-5页 |
| Abstract | 第5-7页 |
| 目录 | 第7-10页 |
| 第一章 绪论 | 第10-21页 |
| ·引言 | 第10-12页 |
| ·相关的研究现状 | 第12-20页 |
| ·本文的主要结构 | 第20-21页 |
| 第二章 数学证明特性分析 | 第21-38页 |
| ·数学证明的基本方法 | 第21-29页 |
| ·数学证明的语言特性 | 第29-38页 |
| ·歧义结构 | 第30-33页 |
| ·其它特性 | 第33-38页 |
| 第三章 数学证明的语法分析 | 第38-65页 |
| ·词法分析 | 第38-41页 |
| ·数学公式的语法分析 | 第41-46页 |
| ·计算语句的语法分析 | 第46-51页 |
| ·简单事实的语法分析 | 第51-58页 |
| ·文法描述 | 第52-57页 |
| ·分析算法 | 第57-58页 |
| ·证明语句的语法分析 | 第58-64页 |
| ·证明实例 | 第64-65页 |
| 第四章 数学证明的语义分析 | 第65-80页 |
| ·话语表现理论 | 第65-69页 |
| ·DRT的基本概念 | 第66-68页 |
| ·DRS的扩充定义 | 第68-69页 |
| ·DRS的构造规则 | 第69-80页 |
| ·部分语句构造规则 | 第69-74页 |
| ·DRS构造实例实例分析 | 第74-80页 |
| 第五章 数学证明的自动化验证 | 第80-121页 |
| ·机器定理证明和定理证明器 | 第80-81页 |
| ·Isabelle接口分析 | 第81-90页 |
| ·Isabelle的命令接口 | 第81-86页 |
| ·Isabelle的程序接口 | 第86-90页 |
| ·基于策略的可计算性分析 | 第90-95页 |
| ·DRS转换算法设计 | 第95-108页 |
| ·前提语句的转换 | 第95-98页 |
| ·结论语句的转换 | 第98-99页 |
| ·定义语句的转换 | 第99-100页 |
| ·语句块的转换 | 第100-101页 |
| ·讨论语句的转换 | 第101-103页 |
| ·归纳语句的转换 | 第103-104页 |
| ·反证语句的转换 | 第104-106页 |
| ·链式语句的转换 | 第106页 |
| ·计算语句的转换 | 第106-108页 |
| ·自动化验证方法研究 | 第108-121页 |
| ·计算策略 | 第109-112页 |
| ·等式策略 | 第112-115页 |
| ·定理搜索策略 | 第115-116页 |
| ·专家系统策略 | 第116-121页 |
| 第六章 结论 | 第121-123页 |
| ·论文研究工作小结 | 第121-122页 |
| ·存在的问题和进一步研究的设想 | 第122-123页 |
| 参考文献 | 第123-129页 |
| 在学期间的研究成果 | 第129-130页 |
| 致谢 | 第130页 |
