分析表列是20世紀50年代由Beth與Hintikka等人建立、後由Smullyan加以發展的一種形式證明方法，基於分析表列方法的邏輯繫統稱為表列繫統。表列繫統與公理繫統、自然推理繫統一樣，是目前*為流行的邏輯證明方法之一，在自動定理證明方面有重要應用。表列方法具有通用於各種邏輯的一般性，不僅經典命題邏輯和一階謂詞邏輯有其表列，在模態邏輯、非單調邏輯等非經典邏輯分支中，表列方法也以不同的形式存在著。自20世紀90年代以來，人們對於表列方法的興趣不斷增加，在許多前沿邏輯研究中廣泛采用表列方法。根據Jon Barwise在《什麼是一個邏輯繫統？》中對邏輯繫統多樣性的闡述，有理由將表列繫統作為與公理繫統、自然推演繫統等並列的一種重要的邏輯繫統類型、將表列法作為一種重要的邏輯方法加以研究。《邏輯中的表列方法》比較繫統地介紹了現代邏輯各個重要分支的表列方法，研究了表列方法的證明效率等問題。本書由孔紅編著。

前言
第一章 表列方法及其發展
第一節 邏輯證明繫統與邏輯語義
一、“正確推理”的兩種定義
二、語言層面的語形和語義
三、邏輯層面的語形和語義
四、邏輯證明繫統
五、邏輯證明繫統的基本性質
第二節 表列繫統
一、邏輯表列的基本思想
二、表列的實施——樹
三、表列方法的優點
第三節 表列方法的發展
第二章 命題邏輯的表列方法
第一節 命題邏輯的形式語言：句法
一、形式語言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的擴充及其表列演算
第四節 限定邏輯的表列方法
一、從謂詞限定到公式限定
二、命題限定邏輯表列
三、公式限定邏輯的子句表列
參考文獻
符號索引