一种基于语义tableau的数据库修正方法

tableau作为自动推理的有效方法之一在许多人工智能领域中有重要的应用。在tableau基础上，提出新的tableau开放和封闭的推理标准，应用于数据库实例不满足完整性约束的不相容关系数据库中，并对其进行修正。这样可以采用逻辑程序的方法，对数据库进行修正，解决了传统修正方法丢失信息、出现新的不相容等问题。     

一种逻辑强化学习的tableau推理方法

tableau方法是一种具有较强的通用性和适用性的推理方法，但由于函数符号、等词等的限制，使得自动推理具有不确定性，针对tableau推理中封闭集合构造过程具有盲目性的问题，提出将强化学习用于tableau自动推理的方法，该方法将tableau推理过程中的逻辑公式与强化学习相结合，产生抽象的状态和活动，这样一方面可以通过学习方法控制自动推理的推理顺序，形成合理的封闭分枝，减少推理的盲目性；另一方面复杂的推理可以利用简单的推理结果，提高推理的效率。     

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。     

一种多值规则量词公式的tableau的方法

在多值逻辑中，含有量词的tableau方法具有统一的扩展规则，并已通过可靠性和完备性的证明。但是由于扩展后的分枝非常庞大，使机器实现非常困难。文章通过对规则量词公式与一阶经典量词公式的对应关系的研究，使二者使用统一的扩展规则。     

一种求解tableau等式合一问题的算法

在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法——等式合一方法，并证明了它的可靠性和完备性。在该方法中，将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究等式合一方法的有效性，在解替换求解方面，提出了提取不等式析取，并在启发式的帮助下计算等价类的方法。通过实例分析，结果表明，等式合一方法优于其它方法。     

一种含等词的分阶段Tableau算法

在增强新的扩展规则的tableau方法的基础上提出了一种新的含等词tableau算法—分阶段tableau。在该算法中，将tableau四分成两个阶段，等词单独处理，利用提取不等式析取并在启发式的帮助下计算等价类的方法，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究分阶段tableau的有效性，进行了实例分析，并与Fitting和Jeffrey方法进行了比较，结果表明，分阶段tableau方法优于其它方法。     

非经典逻辑的语义tableau方法

1.引言自动推理作为自动定理证明的扩展,在计算机科学,特别是人工智能领域中占有重要的地位。许多系统,都是以推理系统作为其核心部分,因此自动推理的研究,对人工智能的其它分枝将产生深远的影响,它所提出的推理方法也被应用于人工智能的各个领域。目前主要的推理方法有:公理系统、自然演绎系统、归结系统、语义tableau系统,不同的方法对于不同的逻辑系统各有优劣。归结系统和语义tableau系统都比较适合于自动推理,其中归结系统与子句或合取范式CNF密切相关,对经典逻辑非常有效,但对于模态逻辑等非经典逻辑存在困难。首     

多变量规则的线性插值推理方法

插值推理是稀疏规则条件下的一类重要的推理方法，单变量的情况已有较多研究，但针对多变量情况的研究还不多，仅有的几种插值方法，存在着难以保证推理结果的凸性和正规性等问题。多变量规则的插值推理是插值推理研究的重要方面，为了在多变量稀疏规则条件下能得到好的插值推理结果，本文对多变量规则的插值推理方法进行了研究，提出了一个多变量规则的线性插值推理方法。该方法能较好地保证推理结果隶属函数的凸性和正规性，为智能系统中的模糊推理提供了一个十分有用的工具。     

基于Tableau的定理机器证明系统TableauTAP

使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TabIeauTAP。该系统可以证明不含等词的经典逻辑公式童耋譬逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，TableauTAP在时间和空间效率上都是比较高的。     

基于tableau结点封闭值的非一致性数据库开放分支修复方法

在将tableau方法扩展到非一致性数据库修复的基础上,提出一种新的利用分支封闭值修复数据库的方法。该方法结合tableau分析法的开放和封闭推理标准,以开放公式树TP(IC∪r)分支为基础,为公式树TP(IC∪r)中每个结点引入一个结点封闭值。根据TP(IC∪r)中结点封闭值的定义,通过计算TP(IC∪r)的结点封闭值来选择分支进行开放修复,从而可以直接确定数据库的修复实例,同时考虑了含有I封闭的修复,将开放修复扩展到含有I封闭的TP(IC∪r),并给予逻辑证明。最后,对于一致性应答结果的逻辑特征予以证明。