自动定理证明的历史几乎与计算机科学的历史一样长，计算机科学中的尖端领域——人工智能的研究也是从自动定理证明开始的。自动推理作为自动定理证明的扩展是人工智能研究的基础工作，许多重要的人工智能系统，都是以推理系统为其核心部分，所以自动推理的研究，将对人工智能的其它分枝产生深远的影响，它所提出的推理方法已被应用于人工智能的各个领域。 语义tableau方法由Beth（1959）、Hintikka（1955）年提出，而后由人工智能研究者引入到自动定理证明中，tableau方法的实质是将语义结构中的二元关系显式地表现出来。换句话说，就是通过引入相应的谓词，将二元关系的性质用逻辑公式来表示。对于不同的逻辑系统，所使用的tableau规则是相同的，只是对公式构造集进行扩展，使之更接近相应的逻辑系统。由于tableau方法具有较强的通用性和直观性，从二十世纪六十年代开始，引起了以Smullyan、Fitting为代表的计算机科学家的兴趣，同归结一样，被认为是重要的自动推理方法之一。特别是近十年来，引起了更广泛的关注，许多人在寻求各种各样的tableau方法，以求提高效率和易于计算机实现。本论文在tableau方法基础上，研究工作可以分为以下四部分： 第一部分，关于经典逻辑tableau方法研究。 （1）对于量词规则，由于γ-规则替换的任意性，可导致在同一tableau证明中，γ-规则被多次使用，使得tableau结构中出现多个自由变量。另外，δ-规则要求被Skolem化的函数符号是新的，且函数中包含分枝中出现的所有自由变量。显然。由于γ—规则的不确定性以及δ—规则的限制，可使一个简单的证明变得很复杂，延迟了tableau的封闭时间。 在文献[49]中。对δ—规则进行了改进，称δ⁺—规则。但对tableau多次出现的自由变量的情况结果仍不太令人满意。在此基础上，对δ⁺—规则进行了进一步的改进，称为δ⁺⁺—规则，并进行了有效性和完备性证明，将δ⁺⁺—规则应用到TableauTAP系统中，结果表明，改进后的系统对δ公式在实现推理空间上有较大的改进。 （2）在tableau实现时，对γ规则应用次数的限制致关重要，限制次数直接影响tableau的推理效率。我们给出识别γ公式方法，提出了含γ公式的tableau推理的改进策略，并进行了理论证明和系统实现，该系统与leanTAP软件包进行了对比实验，通过对Pelletier问题的20个实例分析，可以看出，γ公式不再需要实例化，大大缩短了tableau的证明过吉林大学博士学位论文程，减少了搜索空间，提高了推理效率. 第二部分，关于多值逻辑tabl。au方法研究. （3）含有量词的一阶多值tableau方法具有统一的扩展规则，并由Zabel等人给出了可靠性和完备性的证明.但由于扩展后的分枝随着真值数目的增加而呈指数的增加，因而影响了机器推理执行的效率.我们提出了布尔剪枝方法，将带符号的公式与集合的上集/下集联系起来，使含量词的一阶多值逻辑公式的扩展规则大大简化.进一步，通过对布尔剪枝方法的分析，建立了一类特殊一阶多值逻辑正则公式的更为简洁的tableau推理方法，该方法使得含量词的一阶多值逻辑tableau推理类同于经典逻辑tableau方法. （4）我们将经典逻辑中的结构保留子句转换方法应用到带符号的多值公式中，产生输入规模是线性的范式.并引入极性的概念，减少冗余子句的产生.利用多值子句tableau方法进行证明，并对适合于经典子句的包含删除、分解子因子等策略修改后，应用到多值子句tableau，使其推理效率大大提高. 第三部分，关于含等词tableau方法研究. （5）本文在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法—等式合一方法，并证明了其可靠性和完备性.在该方法中，将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，这样进一步限制了tableau的搜索空间，提高了tableau的推理效率.同时，为了研究等式合一方法的有效性，在解替换求解方面，提出了提取不等式析取，并在启发式的帮助下计算等价类的方法.通过实例分析，与Fi tting和Jeffrey方法进行比较，结果表明，等式合一方法优于其它方法. 第四部分，基于tab 1 eau的定理机器证明系统TableauTAP. （6）我们使用SW工一PROLOG语言在微机上设计实现了基于tableau的定理证明系统TableauTAP，并证明了其正确性.该系统可以证明不含等词的经典逻辑公式和多值逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展.应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，Tab 1 eauTAP在时间和空间效率上都是比较高的.