| 第一章 绪论 | 第9-23页 |
| 1.1 tableau及扩展规则 | 第9-10页 |
| 1.2 相关技术和策略的研究 | 第10-13页 |
| 1.2.1 含量词tableau改造技术 | 第10-11页 |
| 1.2.2 tableau非相关部分剪枝技术 | 第11页 |
| 1.2.3 因子分解技术 | 第11-12页 |
| 1.2.4 包含删除策略 | 第12-13页 |
| 1.3 理论和方法的研究 | 第13-17页 |
| 1.3.1 子句tableau方法 | 第13-14页 |
| 1.3.2 超tableau方法 | 第14页 |
| 1.3.3 决策图tableau(TDD)方法 | 第14-16页 |
| 1.3.4 翻译成整数规划的tableau方法 | 第16-17页 |
| 1.4 非经典逻辑扩展的研究 | 第17-19页 |
| 1.4.1 直觉逻辑tableau | 第17-18页 |
| 1.4.2 模态逻辑tableau | 第18-19页 |
| 1.4.3 多值逻辑tableau | 第19页 |
| 1.5 tableau应用 | 第19-20页 |
| 1.5.1 tableau在数据库方面的应用 | 第19-20页 |
| 1.5.2 tableau在诊断方面的应用 | 第20页 |
| 1.5.3 tableau在自然语言理解方面的应用 | 第20页 |
| 1.6 存在问题和展望 | 第20-21页 |
| 1.7 本文的工作 | 第21-23页 |
| 第二章 改进δ-规则的自由变量语义tableau | 第23-37页 |
| 2.1 语法和语义 | 第23-25页 |
| 2.1.1 基本定义和符号 | 第23页 |
| 2.1.2 tableau扩展规则 | 第23-25页 |
| 2.2 自由变量语义tableau | 第25页 |
| 2.3 δ~+-规则 | 第25-26页 |
| 2.4 进一步改进的δ-规则——δ~(++)-规则 | 第26-28页 |
| 2.5 δ~(++)-规则的有效性 | 第28-29页 |
| 2.6 δ~(++)-规则的完备性 | 第29-31页 |
| 2.7 规则序列 | 第31-35页 |
| 2.8 系统的实现及实验对比 | 第35-36页 |
| 2.9 小结 | 第36-37页 |
| 第三章 基于理论推理方法的自由变量语义tableau中γ-规则的改进 | 第37-52页 |
| 3.1 问题提出 | 第37-38页 |
| 3.2 理论推理 | 第38-40页 |
| 3.2.1 理论 | 第38-39页 |
| 3.2.2 理论的性质 | 第39页 |
| 3.2.3 理论推理的基本定义 | 第39-40页 |
| 3.3 基于理论推理方法的tableau | 第40-43页 |
| 3.3.1 基tableau | 第40-42页 |
| 3.3.2 自由变量tableau | 第42-43页 |
| 3.4 含γ-公式的tableau | 第43-47页 |
| 3.5 正确性证明 | 第47-48页 |
| 3.6 举例 | 第48-49页 |
| 3.7 算法实现 | 第49-51页 |
| 3.8 小结 | 第51-52页 |
| 第四章 利用等式合一处理含等词tableau | 第52-66页 |
| 4.1 含等词的tableau方法分析 | 第52-55页 |
| 4.1.1 含等词的基tableau方法 | 第52-53页 |
| 4.1.2 含等词的自由变量tableau方法 | 第53-55页 |
| 4.2 等式合一问题 | 第55-56页 |
| 4.3 利用等式合一解替换封闭tableau | 第56-58页 |
| 4.3.1 分阶段tableau | 第56页 |
| 4.3.2 利用等式合一解替换封闭tableau | 第56-58页 |
| 4.4 等式合一问题的实现算法 | 第58-63页 |
| 4.4.1 计算等价类 | 第58-59页 |
| 4.4.2 计算等价类近似算法 | 第59-63页 |
| 4.5 算法举例 | 第63-65页 |
| 4.6 小结 | 第65-66页 |
| 第五章 提高一阶多值逻辑tableau推理效率的布尔剪枝方法 | 第66-81页 |
| 5.1 多值逻辑语法和语义 | 第66-68页 |
| 5.2 含量词的一阶多值逻辑Tableau | 第68-69页 |
| 5.3 使用布尔剪枝对tableau方法的改进 | 第69-71页 |
| 5.4 含广义量词的四值逻辑tableau实例 | 第71-72页 |
| 5.5 利用布尔剪枝方法简化tableau分枝 | 第72-75页 |
| 5.6 实例分析 | 第75-76页 |
| 5.7 多值逻辑正则公式的tableau方法 | 第76-79页 |
| 5.8 小结 | 第79-81页 |
| 第六章 转换成带符号子句的多值逻辑推理方法 | 第81-87页 |
| 6.1 多值逻辑中的结构保留子句转换 | 第81-83页 |
| 6.2 多值逻辑中带量词的子句转换 | 第83-84页 |
| 6.3 多值子句tableau | 第84-85页 |
| 6.4 方法改进 | 第85-86页 |
| 6.4.1 子句转换方法改进 | 第85-86页 |
| 6.4.2 子句tableau的改进 | 第86页 |
| 6.5 小结 | 第86-87页 |
| 第七章 翻译成整数规划的tableau方法 | 第87-97页 |
| 7.1 基本概念 | 第87页 |
| 7.2 命题IP-tableau | 第87-89页 |
| 7.3 一阶IP-tableau | 第89-91页 |
| 7.4 多值IP-tableau | 第91-94页 |
| 7.5 无穷值逻辑IP-tableau | 第94-96页 |
| 7.6 小结 | 第96-97页 |
| 第八章 直觉逻辑中的tableau方法 | 第97-103页 |
| 8.1 基本概念 | 第97页 |
| 8.2 形式系统LJ | 第97-99页 |
| 8.2.1 LJ系统规则 | 第97-98页 |
| 8.2.2 LJ的逻辑规则 | 第98-99页 |
| 8.3 Kripke模型 | 第99-100页 |
| 8.4 直觉逻辑的tableau方法 | 第100页 |
| 8.5 直觉逻辑中的模型存在定理 | 第100-102页 |
| 8.6 小结 | 第102-103页 |
| 第九章 基于tableau的定理机器证明系统TableauTAP | 第103-114页 |
| 9.1 程序语法 | 第103-104页 |
| 9.2 系统的预处理 | 第104-107页 |
| 9.2.1 规则表的建立 | 第104-105页 |
| 9.2.2 否定范式的自动生成 | 第105-107页 |
| 9.3 TableauTAP系统的实现 | 第107-108页 |
| 9.4 TableauTAP系统的正确性 | 第108-112页 |
| 9.5 实验结果及对比分析 | 第112-113页 |
| 9.6 小结 | 第113-114页 |
| 参考文献 | 第114-120页 |
| 作者读博士期间完成的论文和参加的项目 | 第120-122页 |
| 致谢 | 第122-123页 |
| 摘要 | 第123-125页 |
| Abstract | 第125页 |
| 原创性声明 | 第128页 |
