一种矩阵归结方法

A Method of Matrix Resolution

提出了一种新的归结方法—矩阵归结。结合归结原理的单文字、纯文字、分裂规则以及Petri网的T-不变量归结的思想,给出了几种矩阵归结策略,证明了它们的完备性。方法简单易行,大大降低了归结的复杂性,提高了归结效率。

<Abstrcat> This paper provides a new method of matrix resolution. We have given some schemes of (matrix) resolution combined with single literal, pure literal, rule of split and T-invariant of Petri net, (then) proved its perfectibility. The all methods are simple, useful and effectible.