论文部分内容阅读
基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法，通过子句集能否推导出所有极大项来判定可满足性．IER（improved extension rule）算法是不完备的算法，在判定子句集子空间不可满足时，并不能判定子句集的满足性，算法还需重新调用ER（extension rule）算法，降低了算法的求解效率．通过对子句集的极大项空间的研究，给出了子句集的极大项空间分解后子空间的求解方法．通过对扩展规则的研究，给出了极大项部分空间可满足性判定方法PSER（partial semi—extensio