| 本文已被：浏览 4147次 下载 4919次 |
码上扫一扫！ |
|
|
| 与替换和集合运算有关的错误* |
|
程晓春1,2, 姜云飞3
|
|
1.吉林大学计算机科学系,长春,130023;2.长春科技大学,长春,130026;3.中山大学软件所,广州,510275
|
|
| 摘要: |
| 指出在使用归结方法的自动推理文献中,存在于提升引理和删除策略完备性定理证明中,与替换和集合运算有关的几个错误,并予以分析和改正. |
| 关键词: 归结,替换,合一,集合,删除策略. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助. |
|
| Errors Related to Substitution and Set Operations |
|
CHENG Xiao-chun,Jiang Yun-fei
|
| Abstract: |
| 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. |
| Key words: Resolution, substitution, unification, set, deletion strategy. |
