《数理逻辑与机器证明》求取 ⇩

第一章　命题逻辑7

1.1　命题连接词7

1.2　公式10

1.3　形式推理系统（上）20

1.4　形式推理系统（下）38

1.5　赋值52

1.6　逻辑推论58

1.7　合取范式和析取范式69

1.8　连接符的完备集74

第二章　一阶逻辑80

2.1　命题函数和量词80

2.2　公式83

2.3　形式推理系统91

2.4　赋值99

2.5　逻辑推论105

2.6　前束范式111

第三章　可靠性和完备性117

3.1　有效性和可满足性117

3.2　可靠性120

3.3　命题逻辑的完备性121

3.4　一阶逻辑的完备性124

3.5　一阶逻辑（带等符）的完备性130

3.6　形式数学系统134

第四章　机器证明138

4.1　试探法138

4.2　判定法143

4.3　计算机辅助证明144

4.4　证明算法145

第五章　Herbrand定理147

5.1　无？前束范式147

5.2　Herbrand定理148

第六章　Davis-Putnam方法和分解法则154

6.1　Davis-Putnam方法155

6.2　统一代入158

6.3　分解法则164

附录　可证式系统178

参考书目186