使用引理的锁语义归结原理——LI-归结原理

为了改进对于一阶逻辑中子句集是完备的2型IDI-归结原理的一个缺点,即在IDI归结中,只对其中一个亲本子句的归结文字有所限制,对另一个亲本子句的归结文字没有任何限制,本文提出了锁语义归结,简称LI-归结。即在这种语义归结原理中,象锁归结过程一样,每一次归结的两个亲本子句中的归结文字,都是该子句中有最小锁的文字,并证明了以一种固定的配锁方法,LI-归结原理对于一阶逻辑中的子句集是完备的。 使用引理的概念,将LI-演绎进行线性整理,从而引进了TLI-演绎的概念。     

3型IDI-归结原理

本文改进了作者提出的IDI-归结原理,使之有效性有所提高,亦即,将IDI-互撞中的电子序号化,并要求每一个互撞中电子的序号序列是不减的,从而引进了3型IDI-归结原理,并证明了它对于一阶逻辑中的子句集是完备的。 本文还顺便指出了文献[1]中关于PI-互撞的性质的一个错误,并利用本文提出的序号化方法,对这个错误进行了补救。     

广义RUE-NRF归结

本文将RUE-NRF归结使用在广义子句集上,提出了广义RUE-NRF归结方法,并证明了这一方法对于一阶逻辑的完备性;将1型、2型删除策略引入广义RUE-NRF归结.     

广义RUE-NRF归结的配锁

本文把广义RUE-NRF归结对E不可满足子句集是完备的推广到了配锁的广义子句集上.     

并行单元归结

给出了基于神经网络的单元归结算法.首先将子句集S表示为δ形,并且用算子对(⊙, )引入两种类型的神经元,然后用这两种神经元构造子句集S的神经网络结构,而后给出基于Horn子句集的神经网络的归结算法,最后证明了该算法的完备性,并用实例进行了验证.     

Horn集上的语义正单元归结

Ｌ． Ｈｅｎｓｃｈｅｎ证明了语义归结对 Ｈｏｒｎ集是完备的［１］。但是语义归结不是正单元归结。本文的主要结果是不可满足的Ｈｏｒｎ子句集合Ｓ有这样一个反驳，对于这个反驳的每一个归结来说，或者一个祖先子句是正单元，而且该正单元在 Ｉ上是假的；或者一个祖先子句是正单元，而且从另一个祖先子句和这个归结式中删去他们的正义字后剩下的子句在 Ｉ上都是假的．其中 Ｉ是 Ｓ的任何一个解释。     

DF命题的矩阵归结

对DFL归结方法作进一步的研究,阐述了DF命题的矩阵归结的理论．对任一DF命题归结反演,得到对应的子句集,采用⊙运算分离DF数和DF命题得到原DF命题的命题归结矩阵,由子句集的不可满足性条件,应用鲁宾逊归结原理,得出DF命题的矩阵归结方法,证明了矩阵归结法的成立定理,并给出了矩阵归结方法的一个推论．     

格值命题逻辑系统Ln ×2P(X)中广义文字的α-归结性

归结自动推理是人工智能领域的一个重要研究方向.以格蕴涵代数为真值域的格值逻辑中的α-归结方法提供了一种处理带有模糊性和不可比较性信息的自动推理问题的工具,能对格值逻辑系统的α-不可满足子句集给出反驳证明,用α-归结原理证明格值逻辑中广义子句集的α-不可满足性,必须首先研究两个广义文字是否可以进行α-归结.研究了格值逻辑...     

布尔算子模糊逻辑中的广义半锁归结原理

大量冗余子句的产生是导致归结方法低效率的根本原因。锁策略通过对子句集中的原子进行配锁,限制某此子旬间的归结以减少无用子句的产生,从而能够提高归结方法的效率。在布尔算子模糊逻辑中,当相同谓词符号配相同锁时,广义锁归结方法是广义完备的。如果对配锁方式不加任何限制,则广义半锁归结方法是广义完备的。     

OL归结的反例及改进的MOL归结

本文给出一个反例,从中可看出OL归结是不完备的。然后加以若干改进,提出一种改进后的序线性归结原理,即MOL归结。本文证明了MOL归结原理是完备的。     

广义支撑集归结原理

广义归结是对Ｊ．Ａ．Ｒｏｂｉｎｓｏｎ普通归结的推广．支撑集策略是提高归结效率的有效方法．本文将支撑集策略引入广义归结中,提出了广义支撑集归结方法,并证明了它的完备性．     

布尔算子模糊逻辑中的删除策略

大量冗余子句的产生是导致归结方法低效率的根本原因。在布尔算子模糊逻辑中施行归结时，使用删除策略能够在水平浸透的过程中减少无用子句的产生，并且不牺牲归结的广义完备性，从而更快地示得子句集的恒假水平。     

多重取因子的线性序归结

本文重新定义了有序子句的有序因子,证明了在这种有序因子定义下的提升引理,进而在理论上得到了多重取因子的线性序归结方法的完备性.     

PROLOG线性归结的研究与设计

本文研究了 Horn 子句的形式描述,分析了 PROLOG 语言的归结机制,探讨了有选择线性归结及其不完备性,提出的改进技术引入了宽度优先搜索机制,并在理论上作了探讨,解决了使搜索陷入无穷分枝的问题。     

狭义模糊逻辑中的锁语义归结原理

在狭义模糊逻辑中的锁语义归结原理可以有比在广义模糊逻辑中更强的限制。本文讨论了这种更强限制下的锁语义归结原理,证明了它在狭义模糊逻辑中是完备的。     

格值命题逻辑系统LP(X)的语义归结方法

为提高格值逻辑系统中α-归结原理的效率,将语义归结思想和α-归结原理相结合,讨论了格值逻辑系统的α-语义归结方法,并得到了其可靠性和完备性,为基于格值逻辑的归结自动推理算法作了必要的准备。     

λ-Horn集上的λ-单元锁归结

本文给出了λ-Horn集上的λ-单元锁归结方法,并证明了λ-单元锁归结方法对λ-恒假公式是完备的。     

直觉模糊逻辑中的归结原理

在模糊逻辑归结原理的基础上，用（０，１）中的两个实数表示一个命题“真的程度”和“假的程度”，从而提出了直觉模糊逻辑，本文提出直觉模糊逻辑的归结原理，并证明其完备性。     

格值命题逻辑LP(X)中的语义归结方法

为了提高格值命题逻辑LP(X)中的α-归结原理的推理效率,将语义归结策略应用于α-归结原理,讨论了格值命题逻辑LP(X)中的α-语义归结方法,并证明了该方法的可靠性和弱完备性,为基于格值逻辑的归结自动推理提供一定基础。     

命题逻辑中一类扩展子句消去方法

随着计算机求解问题越加复杂，问题在转化为命题逻辑子句集包含的冗余信息也越来越多，浪费计算机大量的储存空间和搜索解的时间，因此，对于冗余信息的删减有助于提高计算机求解问题的效率．针对命题逻辑子句集化简问题，在原有冗余性质P、RP基础上，提出多种扩展的、具有性质HRP、ARP的子句消去方法，并通过将不对称文字添加前置方法与命题逻辑集合封锁(SET_BC)、蕴涵模归结原则(IMR)结合，分别提出不对称集合封锁(ASET_BC)消去方法和不对称蕴涵模归结(AIMR)原则．最后，提出L-集合蕴涵模归结(L-SET_IMR)原则和L-不对称集合蕴涵模(L-ASET_IMR)原则．所提出的方法丰富了命题逻辑中冗余性子句消去理论和方法．