基于广义归结的定理机器证明系统

本文使用Ｃ—ＰＲＯＬＯＧ语言在ＳＵＮ工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统ＧＲＭ，ＲＭ，证明了《数学原理》中Ｐａｒｔ１：ｍａｔｈｅｍａｔｉｃａｌｌｏｇｉｃ中ＳｅｃｔｉｏｎＡ与ＳｅｃｔｉｏｎＢ中全部定理（３５０个）．讨论ＧＲＭ和ＲＭ的时、空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带ＯＣＣＵＲ检查的模式匹配．

格值一阶逻辑系统的α广义归结原理

在基于格蕴涵代数的格值逻辑系统框架下,笔者扩展了基于格值逻辑系统的α归结原理,将广义子句集上的归结扩展到一般广义子句集上,提出了基于格值一阶逻辑系统LF(X)的α广义归结原理,建立了格值一阶逻辑系统中α广义归结原理的可靠性定理.通过给出的提升引理,证明了该原理的弱完备性定理.这将为建立基于格值逻辑系统的广义归结方法提供新的自动推理技术.

降低广义归结原理空间复杂度方法的研究

本文针对广义归结原理实现时空间复杂度非常大的问题,通过实际分析广义归结方法实现时造成多余归结的实例,提出了几种优化方法,使系统的归结能力显著提高。

广义归结中的强蕴涵和涵盖

本文讨论了涵盖和强蕴涵之间的关系,给出并证明了强蕴涵是涵盖的条件,还证明了在广义归结中同时使用涵盖和强蕴涵做为删除策略仍是完备的.

命题逻辑中非子句α-有序线性广义归结方法

为了处理在不确定性环境下的自动演绎,重点研究了基于自动推理理论的归结方法,其自动推理理论是真值定义在格蕴涵代数(lattice implication algebra,LIA)结构上格值逻辑系统中的。在已有的确定真值水平α二元归结研究的基础上,作为其继续研究和扩展,引入了基于格值命题逻辑系统LP(X)的非子句多元α-有序线性广义归结方法和演绎,这从本质上避免了一个非子句广义归结演绎到规范子句的形式。随后,得到LP(X)中的非子句多元α-有序线性广义归结演绎是可靠和完备的。该研究工作为格值命题逻辑中基于自动推理的归结提供了一个更有效的方法。

程序分析与广义归结

本文提出使程序分析的机械化效率得以提高的一种途径——广义归结,并证明了这一方法的正确性。

HORN集上基于广义归结方法的定理机器证明

设计了一个Horn集上基于广义归结方法的定理机器证明系统。在算法中使用广度优先与深度优先结合避免了传统归结的组合爆炸。分析了该系统的优缺点,在前人研究的基础上地提出了几点优化的建议。

Boole算子Fuzzy逻辑中的广义归结原理

王湘浩、刘叙华的广义归结方法在一阶逻辑中推广了Robinson的归结原理,使得可以将归结方法用于一种非子句形式的公式集-广义子句集上.从而不仅可以避免从一般的公式集到子句集的转化过程所产生的大量符号冗余,同时也保持了对问题描述的自然性.我们在文献[2]中提出了Boole算子Fuzzy逻辑（以下简称BOFL）,同时将归结方法简洁自然地引入BOFL.在BOFL中,一般地,对任意给定的公式G,可以将G转化成形如{λ1,…,λm,λm+1∨C1,…,λm+n∨Cn}的子句集S,其中λ1,…,λ（m+n）是Fuzzy算子,C1,…,Cn是不含Fuzzy算子的普通形式的子句,则对于任意的Fuzzy算子λ,公式G是λ-恒假的当且仅当子句集S是λ-恒假的.

广义RUE-NRF归结的配锁

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

直觉模糊逻辑的(α,β)-广义锁归结方法

归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程,基于直觉模糊命题逻辑归结原理的一般形式,提出了子句(α,β)-可满足和(α,β)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁,规定在做归结时各子句中被消去文字在该子句中的序号最小,由此建立了(α,β)-广义锁归结方法,并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤,并通过实例说明了该方法的有效性。

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

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

一种新的广义半锁归结

本文提出了对配锁方式不加限制的广义半锁归结方法，并证明了它在一阶逻辑中的完备性．

广义λ-归结中的删除策略

本文在广义λ-归结方法中引进删除策略,讨论了λ-蕴涵的若干性质,并证明:以λ-蕴涵为基础的删除策略不破坏广义λ-归结方法的完备性.

广义支撑集归结原理

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

关于广义调解的一点注记

本文指出了广义调解完备性证明中一个错误,并且给出了使广义调解完备的根据.

NC线性对称调解

本文提出了NC调解方法,证明了NC对称调解与NC归结的结合及广义对称调解与广义归结的结合的线性演绎都是完备的。