2.5.4 线性归结策略
  线性归结策略首先从子句集中选取一个称作顶子句的子句C0开始作归结。归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci+1。而Bi属于S或是已出现的归结式Cj(j<i)。即,如下图所示归结得到的新子句立即参加归结。