Tableau基础理论及应用研究

摘要

自动定理证明的扩展之一：自动推理，是人工智能研究的基础工作。许多重要的人工智能系统，都是以推理系统为其核心部分，所以自动推理的研究，将对人工智能的其它分枝产生深远的影响，它所提出的推理方法已被应用于人工智能的各个领域。其中的语义tableau方法是由Beth(1959)、Hintikka(1955)提出，而后引入到自动定理证明中。它对于不同的逻辑系统，所使用的tableau规则是相同的，只是对公式构造集进行扩展，使之更接近相应的逻辑系统。由于tableau方法具有较强的通用性和直观性，从二十世纪六十年代开始，引起了以Smullyan、Fitting为代表的计算机科学家的兴趣，同归结一样，被认为是重要的自动推理方法之一。特别是近十年来，引起了更广泛的关注，许多人在寻求各种各样的tableau方法。 本文在研究tableau理论的基础上，主要在命题和一阶逻辑中做了以下五个方面的研究： 1.在基本逻辑表示方式的基础上，重点研究了命题和一阶逻辑的范式表示，通过采用析取式重写等方法，得到了在一阶逻辑下，将任意一阶公式转化为析取范式的方法，并利用Prolog语言进行了实现。 2.在逻辑语义的基础上，研究了tableau推理方法(包括命题及一阶)，分析原有命题逻辑下实现算法在效率上的不足，对其进行了改进，并进行了有效性和完备性的证明。同样也针对一阶逻辑下的自动推演算法，通过应用与范式转换中相类似的预处理方式进行修改，以简化后期推演程序，提高效率。 3.在对基本tableau方法扩展的基础上，研究了含等词的tableau方法。 4.在tableau基本理论和方法的基础上，将tableau应用于数据库修正中，解决了此领域中传统修正方法存在的资源消耗大、信息易丢失等问题。 5.采用Prolog语言对上述部分理论和方法进行了实现，并根据Prolog语言的特点进行了优化。

目录

文摘

英文文摘

声明

第一章 绪论

1.1逻辑系统及自动推理简介

1.2研究意义

1.3研究现状及问题

1.4本文工作

1.5本文结构安排

第二章逻辑基础

2.1 简介

2.2命题逻辑基本概念

2.3否定标准式

2.4统一符号

2.5范式概念及实现

2.6一阶逻辑基本概念

2.7一阶语义

2.8一阶统一符号

2.9一阶范式转换

2.10小结

第三章Tableau方法、理论及实现

3.1 简介

3.2命题逻辑下的语义tableau方法

3.3命题tableau有效性

3.4命题tableau完备性

3.5限制的命题tableau完备性

3.6命题逻辑下tableau的实现及改进

3.7一阶模型存在定理

3.8一阶常参语义tableau

3.9一阶常参tableau有效性

3.10一阶常参tableau完备性

3.11 合一

3.12 自由变量语义tableau

3.13一阶自由变量tableau有效性

3.14一阶自由变量tableau完备性

3.15一阶自由变量tableau实现

3.16改进一阶tableau自动推演方法

3.17小结

第四章 含等词的tableau

4.1 简介

4.2句法和语义

4.3等词公理

4.4 Hintikka引理

4.5模型存在定理

4.6含等词的tableau系统

4.7含等词的自由变量tableau系统

4.8含等词的tableau实现

4.9小结

第五章Tableau方法在数据库中的应用

5.1 简介

5.2语义tableau表示数据库

5.3 小结

第六章总结与展望

6.1 总结

6.2展望

参考文献

攻读工程硕士学位期间发表(录用)论文

致谢