%0 Journal Article
%T Errors Related to Substitution and Set Operations<br>与替换和集合运算有关的错误
%A CHENG Xiao-chun
%A Jiang Yun-fei
%A <br>程晓春
%A 姜云飞
%J 软件学报
%D 1999
%I 
%X 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.
%K Resolution
%K substitution
%K unification
%K set
%K deletion strategy<br>归结
%K 替换
%K 合一
%K 集合
%K 删除策略
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=F133C82B2F3ACD27&yid=B914830F5B1D1078&vid=F3090AE9B60B7ED1&iid=0B39A22176CE99FB&sid=BC084ACE66B62CC8&eid=02DC3A182A5530DF&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=6