逻辑中的表列方法

前言

第一章 表列方法及其发展

第一节 逻辑证明系统与逻辑语义

一、“正确推理”的两种定义

二、语言层面的语形和语义

三、逻辑层面的语形和语义

四、逻辑证明系统

五、逻辑证明系统的基本性质

第二节 表列系统

一、逻辑表列的基本思想

二、表列的实施——树

三、表列方法的优点

第三节 表列方法的发展

第二章 命题逻辑的表列方法

第一节 命题逻辑的形式语言：句法

一、形式语言Lp

二、公式的构造树

三、Lp-公式的归纳原理和递归原理

第二节 语义：真值指派与赋值

一、真值函数

二、真值指派与布尔赋值

三、饱和集

第三节 命题逻辑的Smullyan表列

一、加标公式表列

二、不加标公式表列

三、统一记法

四、扩充系统

第四节 Smullyan命题逻辑表列的可靠性与完全性

一、可靠性

二、完全性

三、流畅性与紧致性

第五节 Smullyan命题逻辑表列的优化

一、简化Smullyan表列的若干技巧

二、Smullyan表列的冗余问题

三、Smullyan表列的优化

第六节 表列系统KE

第三章 一阶逻辑的表列方法

第一节 一阶逻辑的句法

一、L的初始符号

二、L-表达式

三、L-表达式的唯一可读性

第二节 一阶逻辑的语义：模型和赋值

一、一阶模型和变元指派

二、．Herbrand．模型

第三节 一阶公式的变形及其语义性质

一、变元的代入

二、Skolem．公式

三、子句公式

第四节 一阶句子表列

一、一阶句子表列

二、一阶句子表列的可靠性和完全性

三、一阶句子表列的Herbrand优化

第五节 自由变元表列

一、合一

二、自由变元表列

第六节 子句表列

一、析取子句表列

二、蕴涵子旬表列

第四章 一阶等词理论推理的表列

第一节 理论和理论推理

一、理论

二、理论推理的基本概念

第二节 等词理论推理的表列

一、句子型等词理论推理表列

二、理论推理的自由变元表列

三、带全称变元的理论推理表列

第三节 理论推理表列的可靠性和完全性

一、可靠性

二、完全性

第四节 基于Reeves方法的ε-表列的改进

第五章 模态逻辑的表列方法

第一节 模态逻辑的形式语言和公理系统

一、模态逻辑的形式语言

二、正规模态逻辑的公理系统

第二节 Kripke语义：模型和框架

一、模型和框架

二、模态公式与和框架性质（一阶公式）的对应

第三节 模态语义图

一、Kripke语义图

二、加标语义图

三、D、T、S4、B和S5的语义图

四、模态语义图的可靠性和完全性

第四节 隐性模态表列

一、K、D、T、s4的分析性表列

二、B和S5的准分析性表列

三、Fitting模态表列系统的可靠性和完全性

四、似矢列演算的模态表列系统CK、CD、CT、CS4、CB和CS5

第五节 前缀模态表列

第六节 Massacci的一步模态表列SST

第七节 前缀模态表列系统KEM

一、前缀

二、前缀的合一

三、KEM表列规则

第六章 非单调逻辑的表列方法

第一节 缺省逻辑及其表列方法

一、Reiter的缺省逻辑

二、其他缺省逻辑

三、缺省逻辑的表列方法

第二节 非单调模态逻辑及其表列方法

一、Moore的自认知逻辑

二、自认知逻辑的表列证明

三、多模态非单调逻辑H的表列

第三节 正常条件句逻辑KLM的表列演算

一、正常条件句逻辑KLM

二、优先逻辑P

三、P的扩充及其表列演算

第四节 限定逻辑的表列方法

一、从谓词限定到公式限定

二、命题限定逻辑表列

三、公式限定逻辑的子句表列

参考文献

符号索引