• 书名：基于矛盾体分离演绎的一阶逻辑自动定理证明器

• ISBN：978-7-5240-0326-7

• 出版社：冶金工业出版社有限公司

• 定价：85

• 作者：曹锋 林玲瑜

• 出版时间：2025-09-15

内容简介

自动推理是人工智能重要的组成部分，主要包括命题逻辑求解和一阶逻辑定理证明。一阶逻辑系统相比命题逻辑系统具有更丰富的表达能力，许多的现实问题都可用一阶逻辑表示。因此，对于一阶逻辑自动定理证明器的研究具有重要的学术价值和广泛的应用前景。矛盾体分离规则是一种多元演绎方法，该方法突破了传统二元归结方法每次限定只有2个子句参与演绎，每次只消去1组互补对文字的限制，具有很多优良的演绎特性,其能够有效地发挥子句间的协同性、动态性和导向性等特性，从而提升一阶逻辑自动定理证明器的能力和效率。

本书重点介绍了基于矛盾体分离理论的一阶逻辑自动定理证明器的各个组成部分、系统构建、演绎过程验证和实验评估，设计实现了基于矛盾体分离演绎的一阶逻辑自动定理证明器、基于矛盾体分离演绎的一阶逻辑自动定理证明融合系统、基于矛盾体分离演绎的一阶逻辑自动定理证明验证检查工具，涵盖了用于一阶逻辑自动定理证明的整个体系。

本书可供从事逻辑推理、自动定理证明、知识表示、形式化验证等人工智能相关专业研究的硕士生、博士生及科研学者参考阅读。

编辑推荐

本书可供从事逻辑推理、自动定理证明、知识表示、形式化验证等人工智能相关专业研究的硕士生、博士生及科研学者参考阅读。

目录

第1章 前言... PAGEREF _Toc170397677 \h 1

1.1 背景及意义 PAGEREF _Toc170397678 \h 1

1.2 国内外相关研究现状 PAGEREF _Toc170397679 \h 3

1.2.1 子句集预处理方法研究现状 PAGEREF _Toc170397681 \h 3

1.2.2 启发式策略研究现状 PAGEREF _Toc170397682 \h 5

1.2.3 推理方法研究现状 PAGEREF _Toc170397683 \h 7

1.3 论文的主要工作 PAGEREF _Toc170397684 \h 10

1.4 论文结构安排 PAGEREF _Toc170397685 \h 12

第2章 矛盾体分离演绎理论... PAGEREF _Toc170397686 \h 15

2.1 引言 PAGEREF _Toc170397687 \h 15

2.2 一阶逻辑基础知识 PAGEREF _Toc170397688 \h 16

2.3 矛盾体分离规则 PAGEREF _Toc170397689 \h 17

2.4 矛盾体分离约简规则 PAGEREF _Toc170397690 \h 22

2.5 矛盾体分离演绎的其它形式 PAGEREF _Toc170397691 \h 23

2.6 小结 PAGEREF _Toc170397692 \h 29

第3章 一阶逻辑子句集预处理... PAGEREF _Toc170397693 \h 30

3.1 引言 PAGEREF _Toc170397694 \h 30

3.2 冗余子句处理 PAGEREF _Toc170397695 \h 33

3.3 基于演绎距离的子句度量方法 PAGEREF _Toc170397696 \h 35

3.3.1 文字演绎距离 PAGEREF _Toc170397697 \h 35

3.3.2 子句演绎距离 PAGEREF _Toc170397698 \h 38

3.4 基于矛盾体分离演绎的一阶逻辑子句预处理方法 PAGEREF _Toc170397699 \h 39

3.5 实验与分析 PAGEREF _Toc170397700 \h 40

3.5.1 实验准备 PAGEREF _Toc170397701 \h 41

3.5.2 实验结果分析 PAGEREF _Toc170397702 \h 41

3.6 小结 PAGEREF _Toc170397703 \h 43

第4章 基于矛盾体分离演绎的启发式策略... PAGEREF _Toc170397704 \h 44

4.1 引言 PAGEREF _Toc170397705 \h 45

4.2 启发式策略 PAGEREF _Toc170397706 \h 46

4.2.1 子句选择策略 PAGEREF _Toc170397707 \h 48

4.2.2 文字选择策略 PAGEREF _Toc170397708 \h 50

4.2.3 矛盾体分离式评估策略 PAGEREF _Toc170397709 \h 51

4.2.4 矛盾体分离演绎控制策略 PAGEREF _Toc170397710 \h 54

4.3 启发式策略的使用方法 PAGEREF _Toc170397711 \h 55

4.4 小结 PAGEREF _Toc170397712 \h 58

第5章 矛盾体分离演绎算法... PAGEREF _Toc170397713 \h 58

5.1 引言 PAGEREF _Toc170397714 \h 59

5.2 矛盾体分离演绎算法关键技术 PAGEREF _Toc170397715 \h 59

5.3 矛盾体分离演绎框架 PAGEREF _Toc170397716 \h 61

5.4 矛盾体分离演绎算法 PAGEREF _Toc170397717 \h 63

5.4.1 基于较优子句的矛盾体分离演绎算法 PAGEREF _Toc170397718 \h 64

5.4.2 基于优化演绎路径的矛盾体分离演绎算法 PAGEREF _Toc170397719 \h 66

5.4.3 基于充分使用子句的矛盾体分离演绎算法 PAGEREF _Toc170397720 \h 69

5.5 基于矛盾体分离演绎的路径搜索算法 PAGEREF _Toc170397721 \h 73

5.6 基于矛盾体分离演绎的全局参数 PAGEREF _Toc170397722 \h 75

5.7 小结 PAGEREF _Toc170397723 \h 77

第6章 基于矛盾体分离演绎的一阶逻辑自动定理证明器系统构建... PAGEREF _Toc170397724 \h 78

6.1 引言 PAGEREF _Toc170397725 \h 78

6.2 基于矛盾体分离演绎的一阶逻辑自动定理证明器的构建 PAGEREF _Toc170397726 \h 79

6.2.1 CSE系列证明器的运行方式 PAGEREF _Toc170397727 \h 81

6.2.2 CSE证明器支持的问题格式 PAGEREF _Toc170397728 \h 82

6.2.3 CSE证明器问题解析与存储 PAGEREF _Toc170397729 \h 83

6.2.4 合一项函数最大复杂度动态控制 PAGEREF _Toc170397730 \h 84

6.2.5 因子归结的实现 PAGEREF _Toc170397731 \h 85

6.2.6 等词归结的实现 PAGEREF _Toc170397732 \h 86

6.2.7 CSE证明器演绎过程正确性检查 PAGEREF _Toc170397733 \h 87

6.3 CSE证明器的实现 PAGEREF _Toc170397734 \h 88

6.4 CSE证明器性能分析 PAGEREF _Toc170397735 \h 89

6.4.1 实验准备 PAGEREF _Toc170397736 \h 89

6.4.2 CSE性能分析 PAGEREF _Toc170397737 \h 90

6.4.3 CSE矛盾体分离演绎能力分析 PAGEREF _Toc170397738 \h 92

6.5 小结 PAGEREF _Toc170397739 \h 95

第7章 基于矛盾体分离演绎的一阶逻辑自动定理证明器融合系统构建... PAGEREF _Toc170397740 \h 96

7.1 引言 PAGEREF _Toc170397741 \h 96

7.2 关键技术 PAGEREF _Toc170397742 \h 98

7.2.1 融合系统结合方案 PAGEREF _Toc170397743 \h 99

7.2.2 矛盾体分离式筛选方法 PAGEREF _Toc170397744 \h 100

7.2.3 接口实现 PAGEREF _Toc170397745 \h 101

7.3 CSE与其它证明器的融合系统构建 PAGEREF _Toc170397746 \h 102

7.3.1 CSE融合系统方案一的实现 PAGEREF _Toc170397747 \h 103

7.3.2 CSE融合系统方案二的实现 PAGEREF _Toc170397748 \h 104

7.4 CSE融合系统演绎过程正确性检查 PAGEREF _Toc170397749 \h 105

7.5 CSE融合系统实验评估 PAGEREF _Toc170397750 \h 107

7.5.1 实验准备 PAGEREF _Toc170397751 \h 107

7.5.2 CSE_V性能分析 PAGEREF _Toc170397752 \h 107

7.5.3 CSE_E性能分析 PAGEREF _Toc170397753 \h 110

7.6 小结 PAGEREF _Toc170397754 \h 112

第8章 多元动态演绎在Prover9证明器中的应用... PAGEREF _Toc170397755 \h 112

8.1 引言 PAGEREF _Toc170397756 \h 112

8.2 多元动态演绎算法 PAGEREF _Toc170397757 \h 113

8.2.1 子句演绎权重 PAGEREF _Toc170397758 \h 114

8.2.2 文字演绎权重 PAGEREF _Toc170397759 \h 114

8.2.3 演绎分离式自定义规则 PAGEREF _Toc170397760 \h 115

8.2.4 多元动态演绎算法设计 PAGEREF _Toc170397761 \h 116

8.2.5 回溯算法 PAGEREF _Toc170397762 \h 118

8.3 多元动态演绎在Prover9中的应用 PAGEREF _Toc170397763 \h 119

8.4 实验分析 PAGEREF _Toc170397764 \h 120

8.4.1 实验准备 PAGEREF _Toc170397765 \h 120

8.4.2 实验分析 PAGEREF _Toc170397766 \h 120

8.5 小结 PAGEREF _Toc170397767 \h 122

第9章 多元协同演绎在一阶逻辑ATP中的应用... PAGEREF _Toc170397768 \h 122

9.1 引言 PAGEREF _Toc170397769 \h 122

9.2 多元协同演绎算法 PAGEREF _Toc170397770 \h 123

9.2.1 子句选择算法 PAGEREF _Toc170397771 \h 124

9.2.2 文字选择算法 PAGEREF _Toc170397772 \h 126

9.2.3 多元协同演绎算法 PAGEREF _Toc170397773 \h 127

9.2.4 多元协同演绎回溯算法 PAGEREF _Toc170397774 \h 127

9.3 多元协同演绎算法的应用 PAGEREF _Toc170397775 \h 128

9.4 实验及结果分析 PAGEREF _Toc170397776 \h 129

9.4.1 实验准备 PAGEREF _Toc170397777 \h 129

9.4.2 CSE_E证明器判定情况 PAGEREF _Toc170397778 \h 129

9.5 小结 PAGEREF _Toc170397779 \h 132

第10章 基于多元矛盾体分离的冲突演绎方法及应用... PAGEREF _Toc170397780 \h 133

10.1 引言 PAGEREF _Toc170397781 \h 133

10.2 矛盾体分离冲突演绎 PAGEREF _Toc170397782 \h 134

10.2.1 矛盾体分离冲突演绎理论 PAGEREF _Toc170397783 \h 134

10.2.2 学习子句的生成过程 PAGEREF _Toc170397784 \h 135

10.3 矛盾体分离冲突演绎优势 PAGEREF _Toc170397785 \h 136

10.3.1 演绎理论的优势 PAGEREF _Toc170397786 \h 136

10.3.2 演绎方法的优势 PAGEREF _Toc170397787 \h 139

10.4 虚子句的选取原则 PAGEREF _Toc170397788 \h 140

10.5 实验结果与分析 PAGEREF _Toc170397789 \h 141

10.5.1 实验准备 PAGEREF _Toc170397790 \h 141

10.5.2 CSCD与Scavenger的对比分析 PAGEREF _Toc170397791 \h 141

10.5.3 CSCD_E的实验分析 PAGEREF _Toc170397792 \h 142

10.5.4 CSCD对Rating值为1问题的证明情况 PAGEREF _Toc170397793 \h 143

10.6 小结 PAGEREF _Toc170397794 \h 143

第11章 矛盾体分离超演绎方法及应用... PAGEREF _Toc170397795 \h 144

11.1 引言 PAGEREF _Toc170397796 \h 144

11.2 基于矛盾体分离超演绎的理论方法 PAGEREF _Toc170397797 \h 145

11.2.1 矛盾体分离超演绎规则 PAGEREF _Toc170397798 \h 145

11.2.2 矛盾体分离超演绎的优势 PAGEREF _Toc170397799 \h 146

11.3 基于矛盾体分离超演绎算法 PAGEREF _Toc170397800 \h 147

11.4 实验结果及分析 PAGEREF _Toc170397801 \h 149

11.4.1 实验准备 PAGEREF _Toc170397802 \h 149

11.4.2 CSSD_E对CASC-27竞赛例（共500个）的实验分析 PAGEREF _Toc170397803 \h 150

11.4.3 CSSD_E对rating为1问题的实验分析 PAGEREF _Toc170397804 \h 151

11.5 小结 PAGEREF _Toc170397805 \h 152

第12章 矛盾体分离单元结果演绎方法及应用... PAGEREF _Toc170397806 \h 152

12.1 引言 PAGEREF _Toc170397807 \h 152

12.2 矛盾体分离单元结果演绎理论 PAGEREF _Toc170397808 \h 153

12.2.1 矛盾体分离单元结果演绎定义 PAGEREF _Toc170397809 \h 153

12.2.2 矛盾体分离单元结果演绎定理 PAGEREF _Toc170397810 \h 154

12.2.3 矛盾体分离单元结果演绎的可靠性 PAGEREF _Toc170397811 \h 154

12.2.4 矛盾体分离单元结果演绎优势 PAGEREF _Toc170397812 \h 155

12.3 矛盾体分离单元结果演绎算法 PAGEREF _Toc170397813 \h 157

12.4 实验及结果分析 PAGEREF _Toc170397814 \h 159

12.4.1 实验准备 PAGEREF _Toc170397815 \h 159

12.4.2 CSURD_Eprover证明2022年国际竞赛例情况（共500个） PAGEREF _Toc170397816 \h 159

12.4.3 CSURD_Eprover证明2023年国际竞赛例情况（共500个） PAGEREF _Toc170397817 \h 160

12.4.4 CSURD_Eprover证明rating为1问题的实验情况 PAGEREF _Toc170397818 \h 161

12.5 小结 PAGEREF _Toc170397819 \h 162

第13章 基于子句活跃度和复杂度的多元动态演绎算法及应用... PAGEREF _Toc170397820 \h 163

13.1 引言 PAGEREF _Toc170397821 \h 163

13.2 一阶逻辑演绎方法 PAGEREF _Toc170397822 \h 164

13.2.1 多元动态演绎过程分析 PAGEREF _Toc170397823 \h 164

13.3 基于复杂度评估的子句选择方法 PAGEREF _Toc170397824 \h 164

13.3.1 不同的子句选择方法对多元演绎的影响分析 PAGEREF _Toc170397825 \h 164

13.3.2 基于变元项的子句活跃度评估方法 PAGEREF _Toc170397826 \h 165

13.3.3 基于函数项结构的子句复杂度评估方法 PAGEREF _Toc170397827 \h 167

13.4 基于子句活跃度和复杂度的多元动态演绎算法 PAGEREF _Toc170397828 \h 170

13.5 实验及结果分析 PAGEREF _Toc170397829 \h 171

13.5.1 实验准备 PAGEREF _Toc170397830 \h 171

13.5.2 mcs_Eprover证明国际竞赛例（共500个）判定情况 PAGEREF _Toc170397831 \h 172

13.5.3 mcs_Eprover证明Eprover2.6未证明定理（106个）的判定情况 PAGEREF _Toc170397832 \h 172

13.6 小结 PAGEREF _Toc170397833 \h 173

第14章 一种基于文字匹配度的多元协同演绎算法及应用... PAGEREF _Toc170397834 \h 174

14.1 引言 PAGEREF _Toc170397835 \h 174

14.2 多元动态演绎 PAGEREF _Toc170397836 \h 175

14.3 基于项匹配度的文字选择策略 PAGEREF _Toc170397837 \h 176

14.3.1 不同文字选择方法对矛盾体分离演绎的影响分析 PAGEREF _Toc170397838 \h 176

14.3.2 项的匹配度 PAGEREF _Toc170397839 \h 177

14.3.3 基于符号特征的项匹配度评估方法 PAGEREF _Toc170397840 \h 179

14.3.4 文字选择策略 PAGEREF _Toc170397841 \h 184

14.4 基于文字匹配度的多元协同演绎算法 PAGEREF _Toc170397842 \h 185

14.5 实验结果及分析 PAGEREF _Toc170397843 \h 186

14.5.1 实验准备 PAGEREF _Toc170397844 \h 186

14.5.2 LMD_Eprover证明2022年国际竞赛例(共500个)判定情况 PAGEREF _Toc170397845 \h 186

14.5.3 LMD_Eprover证明2021年国际竞赛例(共500个)判定情况 PAGEREF _Toc170397846 \h 188

14.6 小结 PAGEREF _Toc170397847 \h 189

第15章 基于单元子句的多元矛盾体分离演绎算法及应用... PAGEREF _Toc170397848 \h 190

15.1 引言 PAGEREF _Toc170397849 \h 190

15.2 单元子句在矛盾体分离规则中的特性 PAGEREF _Toc170397850 \h 191

15.2.1 单元子句在矛盾体分离规则中的演绎性质 PAGEREF _Toc170397851 \h 191

15.2.2 基于单元子句的多元矛盾体分离演绎框架 PAGEREF _Toc170397852 \h 192

15.3 单元子句选择策略 PAGEREF _Toc170397853 \h 193

15.4 基于单元子句的多元矛盾体分离演绎算法 PAGEREF _Toc170397854 \h 195

15.5 基于单元子句的多元矛盾体分离演绎算法应用 PAGEREF _Toc170397855 \h 196

15.6 实验及结果分析 PAGEREF _Toc170397856 \h 197

15.6.1 实验准备 PAGEREF _Toc170397857 \h 197

15.6.2 实验分析 PAGEREF _Toc170397858 \h 197

15.7 小结 PAGEREF _Toc170397859 \h 200

第16章 总结... PAGEREF _Toc170397860 \h 201

16.1 论文总结 PAGEREF _Toc170397861 \h 201

16.2 今后工作展望 PAGEREF _Toc170397862 \h 202