1 矛盾体分离演绎理论
1.1 一阶逻辑基础知识
1.2 二元归结方法
1.3 矛盾体分离规则
1.4 矛盾体分离约简规则
1.5 矛盾体分离演绎的其他形式
2 一阶逻辑子句集预处理
2.1 一阶逻辑子句预处理常用方法
2.2 冗余子句处理
2.3 基于演绎距离的子句度量方法
2.3.1 文字演绎距离
2.3.2 子句演绎距离
2.4 基于矛盾体分离演绎的一阶逻辑子句预处理方法
2.5 子句集预处理方法实验
2.5.1 子句集预处理方法实验准备
2.5.2 子句集预处理方法实验结果分析
3 基于矛盾体分离演绎的启发式策略
3.1 常用的启发式策略方法
3.2 启发式策略
3.2.1 子句选择策略
3.2.2 文字选择策略
3.2.3 矛盾体分离式评估策略
3.2.4 矛盾体分离演绎控制策略
3.3 启发式策略的使用方法
3.3.1 子句选择策略的使用
3.3.2 文字选择策略的使用
3.3.3 矛盾体分离式评估策略的使用
4 矛盾体分离演绎算法
4.1 二元归结与多元演绎
4.2 矛盾体分离演绎算法关键技术
4.3 矛盾体分离演绎框架
4.3.1 整体式演绎框架
4.3.2 Given-clause演绎框架
4.4 矛盾体分离演绎算法
4.4.1 基于较优子句的矛盾体分离演绎算法
4.4.2 基于优化演绎路径的矛盾体分离演绎算法
4.4.3 基于充分使用子句的矛盾体分离演绎算法
4.5 基于矛盾体分离演绎的路径搜索算法
4.6 基于矛盾体分离演绎的全局参数
5 基于矛盾体分离演绎的一阶逻辑自动定理证明器系统构建
5.1 一阶逻辑自动定理证明器现状
5.2 基于矛盾体分离演绎的一阶逻辑自动定理证明器的构建
5.2.1 CSE系列证明器的运行方式
5.2.2 CSE证明器支持的问题格式
5.2.3 CSE证明器问题解析与存储
5.2.4 合一项函数最大复杂度动态控制
5.2.5 因子归结的实现
5.2.6 等词归结的实现
5.2.7 CSE证明器演绎过程正确性检查
5.3 CSE证明器的实现
5.4 CSE证明器性能分析
5.4.1 实验准备
5.4.2 CSE性能分析
5.4.3 CSE矛盾体分离演绎能力分析
6 基于矛盾体分离演绎的一阶逻辑自动定理证明器融合系统构建
6.1 证明器融合方法
6.2 关键技术
6.2.1 融合系统结合方案
6.2.2 矛盾体分离式筛选方法
6.2.3 融合接口实现
6.3 CSE与其他证明器的融合系统构建
6.3.1 CSE融合系统方案（一）的实现
6.3.2 CSE融合系统方案（二）的实现
6.4 CSE融合系统演绎过程正确性检查
6.5 CSE融合系统实验评估
6.5.1 CSE融合系统实验准备
6.5.2 CSE_V性能分析
6.5.3 CSE_E性能分析
7 多元动态演绎在Prover9证明器中的应用
7.1 多元演绎方法
7.2 多元动态演绎算法
7.2.1 子句演绎权重
7.2.2 文字演绎权重
7.2.3 演绎分离式自定义规则
7.2.4 多元动态演绎算法设计
7.2.5 回溯算法
7.3 多元动态演绎在Prover9中的应用
7.4 多元动态演绎算法评估
7.4.1 多元动态演绎算法实验准备
7.4.2 性能比较及判定情况
8 多元协同演绎在自动定理证明中的应用
8.1 自动定理证明器背景
8.2 多元协同演绎算法
8.2.1 子句选择算法
8.2.2 文字选择算法
8.2.3 一种多元协同演绎算法
8.2.4 多元协同演绎回溯算法
8.3 多元协同演绎算法的应用
8.4 多元协同演绎算法实验
8.4.1 多元协同演绎算法实验环境
8.4.2 CSE_E证明器判定情况
9 矛盾体分离超演绎方法及应用
9.1 推理规则背景
9.2 基于矛盾体分离超演绎的理论方法
9.2.1 矛盾体分离超演绎规则
9.2.2 矛盾体分离超演绎的优势
9.3 基于矛盾体分离超演绎的算法
9.4 矛盾体分离超演绎算法实验分析
9.4.1 实验测试准备
9.4.2 CSSD_E对CASC-27竞赛例（共500个）的实验分析
9.4.3 CSSD_E对TPTP-v7.3.0问题解决库中rating为1问题的实验分析
10 基于子句活跃度和复杂度的多元动态演绎算法及应用
10.1 子句选择方法背景
10.2 一阶逻辑多元演绎方法
10.3 基于复杂度评估的子句选择方法
10.3.1 不同的子句选择方法对多元演绎的影响分析
10.3.2 基于变元项的子句活跃度评估方法
10.3.3 基于函数项结构的子句复杂度评估方法
10.4 基于子句活跃度和复杂度的多元动态演绎算法
10.5 基于子句活跃度和复杂度的多元动态演绎算法实验
10.5.1 实验环境准备
10.5.2 mcs_Eprover证明国际竞赛例（共500个）判定情况
10.5.3 mcs_Eprover证明Eprover2.6未证明定理（106个）的判定情况
11 一种基于文字匹配度的多元协同演绎算法及应用
11.1 文字选择方法背景
11.2 多元动态演绎
11.3 基于项匹配度的文字选择策略
11.3.1 不同文字选择方法对矛盾体分离演绎
展开
