文献[1]提出了Horn集上输入半锁归结原理,文献[2]则把文献[1]的结论推广到了含有等词的Horn集上。文献[3]提出了处理等词的RUE-NRF推理规则。它的特点是把等词的自反性,可传性以及替换性包括在这一推理规则之中,从而在整个定理反驳证明过程中不再出现任何等词公理。文献[3]证明了这一规则的正确性和完备性,并用布尔代数,群论和环论等十七个定理在计算 Literature [1] proposed that the Horn set input semi-lock principle, while the literature [2] extended the conclusion of [1] to the Horn set containing the equivalent words. Literature [3] proposed RUE-NRF inference rules for processing terms. It is characterized by the inclusion of reflexivity, transmissibility, and substitution of the equivalents in this rule of reasoning so that no other axioms emerge throughout the proof-refutation of the theorem. Document [3] proved the correctness and completeness of this rule and calculated it by seventeen theorems such as Boolean algebra, group theory and loop theory