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