《自动推理引论及其应用》求取 ⇩

第一章引论1

目 录1

§1.1什么是自动推理2

§1.2 各章简介4

第二章从例子学逻辑7

§2.1逻辑运算7

§2.2 自动推理程序使用的语言12

2.2.1谓词和常量14

2.2.2变量15

2.2.3 函数17

§2.3转换规则21

2.4.1假设和公理23

§2.4假设和公理、推理类型以及证明23

2.4.2推理的的类型——推理规则25

2.4.3证明28

§2.5小结35

第三章智力问题37

§3.1小型的工作智力问题38

3.1.1小型工作智力问题的表示方法39

3.1.2选择推理的类型41

3.1.3小型工作智力问题的解41

3.1.4关于子句描述和证明的讨论45

§3.2完整的工作智力问题46

3.2.1人的求解过程47

3.2.2用自动推理程序的求解过程50

3.2.3小结75

第四章 灵活的表示方法和等式的应用77

§4.1信息表示的一般化78

§4.2技巧与直接方法86

§4.3相等93

4.3.1小型方块排列问题97

4.3.2完整的方块排列问题100

§4.4推理程序中的操作顺序104

§4.5格外小心111

第五章疑难智力问题113

§5.1棋盘和骨牌智力问题113

5.1.1人的推理114

5.1.2问题的表示115

5.1.3推理规则的选择123

5.1.4求解策略123

5.1.5求解方法的性质和结果124

§5.2传教士与野人智力问题126

5.2.1问题的简单表示127

5.2.2问题的复杂表示129

§5.3弹子和天平智力问题137

5.3.1问题的表示138

第六章小结149

§6.1逻辑149

6.1.1and（与）149

6.1.3 not（非）150

6.1.2 or（或）150

6.1.4if-then（如果—则）151

6.1.5 is-equiualent-to（等价）151

6.1.6关系与法则151

§6.2描述语言153

6.2.1变量154

§6.3问题描述155

6.3.1假设和公理156

6.3.2特殊事实和特殊假设156

6.3.3 目标或定理的否定156

§6.4推理规则158

6.4.1合158

6.4.2二元归结159

6.4.3 UR-归结160

6.4.4超归结160

6.4.5等式归结161

6.4.6其它推理推则163

§6.5空子句163

§6.6 归约（Demodulation）164

§6.7类含检查（Subsumption）166

§6.8控制策略167

6.8.1支撑集策略167

6.8.2加权策略168

6.8.3单位子句优先策略168

§6.9推理实例169

§6.10 AURA172

第七章逻辑电路设计177

§7.1逻辑电路设计基本方法177

7.1.1基本逻辑电路177

7.1.2设计说明181

§7.2逻辑电路设计中的归约方法183

7.2.1函数型设计说明183

7.2.2描述性设计说明187

7.2.3表格型设计说明189

7.2.4 电路设计中归约方法的利弊191

§7.3逻辑电路设计中的超归结方法192

7.3.1 谓词OUTPUT192

7.3.2构造规则193

7.3.3例子194

7.3.4 可达信号与谓词OUTPUT197

§7.4迷宫电路的求解198

7.4.1复杂性分析198

7.4.2方法1200

7.4.3方法2204

7.4.4方法3208

§7.5多值逻辑设计中的负超归结方法214

7.5.1 T门215

7.5.2多值函数的表示215

7.5.3构造规则217

7.5.4负超归结217

§8.2一个简单的例子221

第八章 逻辑电路的正确性证明221

§8.1 什么是逻辑电路的正确性证明221

§8.3例子的重要特征224

8.3.1语言翻译224

8.3.2规范化225

8.3.3简化226

8.3.4交换型归约式和字典排序226

§8.4更复杂的例子228

§8.5加法器电路的证明234

8.5.1 1位全加器234

8.5.2黑箱技术239

第九章数学研究242

§9.1 简例243

9.1.1支撑集策略的应用249

9.1.2加权策略的应用252

9.1.3归约和规范254

9.1.4类含和冗余255

§9.2疑难问题的求解261

§9.3模型和反例的生成264

§9.4概念的可表示性：难和易271

§9.5 小结272

第十章形式逻辑的研究275

§10.1等价演算276

§10.2一个简单例子277

§10.3给以知识和直觉280

§10.4解答疑难问题282

10.4.1寻找有用的记法284

10.4.2提出猜想285

第十一章专家系统289

§11.1 什么是专家系统289

§11.2博奕专家系统290

§11.3其它类型的专家系统292

§11.4推理元293

§11.5简单的专家系统297

§11.6专家系统中推理的深度306

§11.7 小结311

第十二章程序排错与验证312

12.1.1程序段的推理314

§12.1符号执行314

12.1.2符号执行程序的表示316

12.1.3模拟程序执行的归约式326

12.1.4正确程序的执行333

12.1.5错误程序段的符号执行334

§12.2程序正确性证明338

12.2.1一简单程序及其说明340

12.2.2证明无循环程序的正确性341

12.2.3条件语句的正确性证明345

12.2.4循环程序的正确性证明348

12.2.5证明循环出口处的正确性352

12.2.6程序的正确性354

12.2.7含数组的程序的正确性的证明356

§12.3抽象程序设计和高级程序证明360

1 2.3.1什么叫抽象程序设计361

12.3.2一个抽象程序设计的例子363

§12.4结论370

第十三章Prolog：逻辑程序设计语言372

§13.1 Prolog简介374

§13.2核反应堆设计中的一例386

13.2.1问题的描述386

13.2.2用Prolog表示事实393

13.2.3一个验证连接点属性的简单程序398

13.2.4寻找路径399

13.2.5检查单个部件引起的失灵400

§13.3小结402

第十四章 自动推理的形式处理404

§14.1语言404

§14.2推理规则408

14.2.1二元归结411

14.2.2完备性415

§14.3策略422

§14.4其他推理规则429

§14.5类含检查436

§14.6归约法438

第十五章 自动推理艺术440

§15.1信息的表示442

15.1.1单位子句443

15.1.2相等谓词446

15.1.3短子句优于长子句447

15.1.4相关信息448

§15.2推理规则449

§15.3控制策略451

§15.4文献说明454

第十六章默认推理455

§16.1默认推理实例455

16.1.1默认推理的非单调特征459

16.1.2默认和伤残知识460

§16.2默认理论及其延伸462

16.2.1预备知识462

16.2.2封闭默认理论的延伸463

§16.3规范默认理论470

16.3.1封闭规范默认理论471

§16.4证明理论477

16.4.1默认证明478

16.4.2延伸元的判定问题485

§16.5 目标驱动的默认证明：和归结证明器的关系487

§16.6封闭规范默认理论和信念修正495

16.6.1公共延伸496

16.6.2信念的产生和新信息的同化499

16.6.3信念的产生和新默认的同化499

§16.7小结500

参考文献503