Errors Related to Substitution and Set Operations
与替换和集合运算有关的错误

In this paper, some errors related to substitution and set operations in the proof procedures of lifting lemma and the completeness theorem of deletion strategy, which are in the literatures on resolution-based automated reasoning, are pointed out, analyzed, and corrected.