规则应用及结束条件
1、规则应用
逆向演绎系统中的规则称为b规则，形式为
W®L
其中W为任意的与或形式，L为一单文字。这个限制简化了b规则对与或图的应用。某些不符合这一要求的规则可以变换称这种形式，例如W®L1ÙL2形式的规则可以表示成两个规则W®L1和W®L2。
规则中应Skolem化存在量词量化的变量，并略去全称量词，认为规则中尚存的变量都是全称量词量化的变量。
在目标公式的与或图中，如果有一个文字L'能够与L合一，则可应用b规则W®L 。应用的结果是将L'结点通过一个标有L与L'的最简合一者u的匹配弧与结点L相连，结点L作为W的与或图的根结点。这样，新的与或图的解图所对应的子句就增加了一个归结式的集合，既规则 W®L的否定式 WÙØL 得到的子句与目标公式的子句对文字L进行归结得到的那些归结式。一条规则可以应用多次，每次都使用不同的变量。
2、结束条件
逆向演绎系统的事实表达式限制为文字的合取，可表示为文字的集合。对任意事实表达式，应当用Skolem函数代替事实表达式中存在量词量化的变量，并略去全称量词，认为事实表达式中尚存的变量为全称量词量化的变量，将表达式转化成标准的文字的合取形式。当一个事实文字和与或图中的一个文字可以合一时，可将该事实文字通过匹配弧连接到与或图中相应的文字上，匹配弧应标明两个文字的最简合一者。同一事实文字可以匹配多次，每次使用不同的变量。
逆向系统的结束条件就是与或图中包括一个结束在事实结点上的一致解图，该解图的合一复合作用于目标表达式就是解答与句。