《计算机科学中的逻辑学》

目录1

第一章　形式系统概论1

1.1　从公理系统到形式系统2

1.2　形式系统的定义5

1.3　命题演算及命题演算形式系统9

1.3.1 命题演算9

1.3.2　命题演算形式系统16

1.4　形式系统的元语言和元理论19

1.4.1　形式系统的元语言和元理论20

1.4.2　元理论关于系统语构的研究22

1.4.3　元理论关于系统语义的研究27

1.4.4　元理论关于系统语构及语义关系的研究31

习题36

第二章　一阶谓词演算38

2.1　一阶谓词演算基本概念38

2.1.1　谓词和函词39

2.1.2　变元和常元41

2.1.3　量词43

2.2.1　一阶语言47

2.2　一阶谓词演算形式系统47

2.2.2　一阶逻辑51

2.3　一阶谓词演算形式系统的语义58

2.4　关于FSFC的重要元定理62

2.4.1　FSFC的合理性及其它62

2.4.2　FSFC的完备性及其它63

2.4.3　FSFC的半可判定性69

习题70

3.1　使用五个真值联结词和两个量词的一阶谓词演算系统73

第三章　其它形式的一阶谓词演算系统73

3.2　带等词的一阶谓词演算系统78

3.3　自然演绎系统80

3.4 多型变元一阶谓词演算系统91

3.5　直觉主义的一阶谓词演算系统95

3.5.1　一阶谓词演算的直觉主义系统96

3.5.2　直觉主义一阶谓词演算系统的语义103

3.6　一阶谓词演算系统的形式表述能力108

习题113

4.1.1　斯柯伦标准形和子句集115

第四章　消解原理及其应用115

4.1　消解原理115

4.1.2　赫布兰德结构119

4.1.3　赫布兰德定理124

4.1.4　消解原理128

4.2　消解的策略139

4.2.1　删除策略139

4.2.2　支集策略140

4.2.3　锁消解141

4.2.4　线性消解142

4.2.5　输入消解143

4.2.6　单位消解143

4.3　消解原理的应用144

4.3.1　问题求解145

4.3.2　规划生成146

4.3.3　程序综合147

4.3.4　程序分析和程序验证150

4.4　带等词一阶谓词演算的消解及其它154

习题156

第五章　霍恩子句逻辑和逻辑程序设计159

5.1　子句的蕴涵表示形式159

5.2　霍恩子句逻辑164

5.2.1　霍恩子句及其过程解释164

5.2.2　关于霍恩子句逻辑程序的讨论167

5.2.3　霍恩子句逻辑程序设计举例174

5.3　Prolog语言简介180

5.3.1　Prolog程序的基本构成与执行方式180

5.3.2　Prolog语言的基本文法183

5.3.3　Prolog的控制成分及Prolog程序实例185

5.3.4　Prolog的基本特点189

习题190

第六章　二阶谓词演算192

6.1　二阶语言192

6.2　二阶谓词演算形式系统194

6.3　二阶语义及其与二阶谓词演算系统的关系200

6.3.1　满结构语义201

6.3.2　一般结构语义204

6.4　知识表示的格林方法和科瓦尔斯基方法209

习题213

第七章　模态逻辑215

7.1　模态逻辑的非形式讨论216

7.2　模态逻辑正规系统及其语义219

7.2.1　模态语言及模态逻辑正规系统NSK219

7.2.2　正规结构223

7.2.3 关于正规系统的重要元定理225

7.3.1　正规系统NSKD,NSKT,NSKB229

7.3　模态逻辑系统NSKD,NSKT,NSKB,NSK4,NSK5及其它229

7.3.2　正规系统NSK4,NSK5,S4,S5及其它232

7.3.3　模态词的归约238

7.4　模态谓词演算245

7.5　模态逻辑的几种解释247

7.5.1　真理论模态逻辑247

7.5.2　认识论模态逻辑247

7.5.3　道义论模态逻辑252

7.5.4　时序逻辑254

7.5.5　经验论模态逻辑255

习题258

第八章　时序逻辑260

8.1　MPTL的语言260

8.2　MPTL的语义262

8.3　时序逻辑系统MPTL266

8.3.1　时序命题演算266

8.3.2　带等词的一阶时序逻辑279

8.4 MPTL作为并发程序验证系统287

8.4.1　归纳原理的描述287

8.4.2　程序结构的描述289

8.4.3　关于程序结构的公理及规则297

习题302

第九章　动态逻辑304

9.1　命题动态逻辑304

9.2　一阶动态逻辑310

9.2.1　一种简单的程序语言310

9.2.2　一阶动态逻辑的语言及语义311

9.2.3　FDL的公理系统316

9.3　确定型一阶动态逻辑320

9.4　一阶动态逻辑的描述能力325

习题330

第十章　多值逻辑及模糊逻辑332

10.1　三值逻辑332

10.1.1　克利恩三值逻辑333

10.1.2　卢卡西维茨三值逻辑337

10.1.3　波兹瓦三值逻辑338

10.2　无穷值逻辑341

10.2.1　卢卡西维茨无穷值逻辑341

10.2.2　雷斯彻概率逻辑345

10.3　模糊逻辑347

10.3.1　模糊子集及其运算348

10.3.2　模糊关系353

10.3.3　模糊逻辑356

10.4　模糊推理的一个应用362

习题365

第十一章　非单调逻辑366

11.1　单调性与非单调性367

11.2　非单调逻辑的产生368

11.3　缺席推理逻辑370

11.4　非单调逻辑379

11.5　限定理论387

第十二章　λ-演算与组合逻辑396

12.1　逻辑系统的归约396

12.2　λ-记号及λ-表达式398

12.3　λ-演算402

12.3.1　λK-演算系统403

12.3.2　λη-演算系统及λI-演算系统409

12.3.3　化归412

12.4.1　λ-项上的运算416

12.4　λ-演算的表示能力416

12.4.2　λ-可定义的自然数函数420

12.4.3　一阶逻辑归约为λ-演算424

12.5　λ-表达式的机器表示426

12.6　组合逻辑429

12.6.1　组合逻辑形式系统430

12.6.2 λK与CL之间的关系433

习题437

参考文献439