基于半扩展规则的定理证明方法

自动定理证明一直是人工智能领域中最重要的问题之一,基于归结的方法是通过推出空子句的方法来判定子句集的可满足性.基于扩展规则的定理证明方法在一定意义上是和归结原理对偶的方法,是通过子句集能否推导出所有极大项组成的子句集来判定可满足性.通过对扩展规则的研究给出了半扩展规则的概念,并提出了基于半扩展规则的定理证明算法SER.然后分析及证明了该算法的正确性、完备性和复杂性.实验结果表明,算法SER的执行效率较基于归结的有向归结算法DR和基于扩展规则算法IER,NER有明显的提高.

一种新的基于局部搜索的扩展规则推理方法

作为与归结推理方法互补的推理方法,扩展规则推理方法得到了国内外广泛认可.目前扩展规则推理方法的研究主要集中于完备推理方法,由于极大项变换方式过于机械,导致该方法处理公式的规模比较局限.该文在深入分析扩展规则推理和局部搜索关联性的基础上,利用子句集中的"极大项"概念设计了一种反向求解策略,进而设计并实现一种新的基于局部搜索的扩展规则推理框架.在此基础上,为了使得极大项搜索过程更加适配该框架,提出了一种基于精确格局检测实现和双向半扩展规则策略的两阶段局部搜索算法.实验结果表明,该文提出的基于精确格局检测的新型扩展规则推理算法ERACC突破了传统扩展规则推理对公式规模的局限,求解效率有了极大提高,使得扩展规则推理方法不再受公式规模制约,可以用于知识编译和可能性推理等多方面的应用.