逻辑中的表列方法

　　分析表列是20世纪50年代由Beth与Hintikka等人建立、后由Smullyan加以发展的一种形式证明方法，基于分析表列方法的逻辑系统称为表列系统。表列系统与公理系统、自然推理系统一样，是目前最为流行的逻辑证明方法之一，在自动定理证明方面有重要应用。表列方法具有通用于各种逻辑的一般性，不仅经典命题逻辑和一阶谓词逻辑有其表列，在模态逻辑、非单调逻辑等非经典逻辑分支中，表列方法也以不同的形式存在着。自20世纪90年代以来，人们对于表列方法的兴趣不断增加，在许多前沿逻辑研究中广泛采用表列方法。根据JonBarwise在《什么是一个逻辑系统？》中对逻辑系统多样性的阐述，有理由将表列系统作为与公理系统、自然推演系统等并列的一种重要的逻辑系统类型、将表列法作为一种重要的逻辑方法加以研究。《逻辑中的表列方法》比较系统地介绍了现代逻辑各个重要分支的表列方法，研究了表列方法的证明效率等问题。

暂缺《逻辑中的表列方法》作者简介

前言
第一章 表列方法及其发展
第一节 逻辑证明系统与逻辑语义
一、“正确推理”的两种定义
二、语言层面的语形和语义
三、逻辑层面的语形和语义
四、逻辑证明系统
五、逻辑证明系统的基本性质
第二节 表列系统
一、逻辑表列的基本思想
二、表列的实施——树
三、表列方法的优点
第三节 表列方法的发展

第二章 命题逻辑的表列方法
第一节 命题逻辑的形式语言：句法
一、形式语言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的扩充及其表列演算
第四节 限定逻辑的表列方法
一、从谓词限定到公式限定
二、命题限定逻辑表列
三、公式限定逻辑的子句表列
参考文献
符号索引