声明
摘要
第1章 绪论
1．1 课题背景
1．1．1 形式化方法
1．1．2 定理证明器
1．2 国内外研究
1．3 研究目标
1．4 本文的主要创新点
1．5 章节安排
第2章 预备知识
2．1．1 字母表
2．1．2 项和公式
2．1．3 联结词
2．1．4 变量与替换
2．1．5 可满足性
2．1．6 完备性
2．1．7 范式
2．2 序
2．2．1 简化序
2．2．2 多重集合
第3章 演绎系统
3．1 引言
3．2 相继式演算
3．2．1 相继式
3．2．2 公理
3．2．3 联结词规则
3．2．4 量词规则
3．2．5 切规则
3．2．6 相继式演算的完备性
3．3 归结原理
3．3．1 合一
3．3．2 推理规则
3．3．3 归结定理
3．4 叠加法
3．4．1 等式公理
3．4．2 文字选择函数
3．4．3 推理规则
3．4．4 简化规则
3．5 小结
第4章 定理证明器的设计与实现
4．1 概述
4．1．1 系统功能
4．1．2 系统架构
4．1．3 开发环境
4．2 一阶逻辑的实现
4．2．1 项和公式的实现
4．2．2 替换的实现
4．2．3 语法分析与显示输出
4．3 输入环境
4．4 交互式定理证明
4．4．1 功能模块
4．4．2 证明过程
4．4．3 相继式
4．4．4 证明树
4．4．5 策略
4．5 自动定理证明
4．5．1 功能模块
4．5．2 公式预处理
4．5．3 合一的实现
4．5．4 序和叠加法
4．5．5 搜索证明
4．5．6 自动定理证明界面
4．6 保存／载入证明
4．7 小结
第5章 系统演示
5．1 引言
5．2 证明演示
5．2．1 命题逻辑问题
5．2．2 一阶逻辑问题
5．2．3 群论问题1
5．2．4 群论问题2
5．2．5 群论问题3
5．3 证明能力测试
5．4 系统的局限性
5．5 小结
第6章 总结和展望
6．1 工作总结
6．2 工作展望
参考文献
致谢
