| 与替换和集合运算有关的错误* |
| |
| 引用本文： | 程晓春,姜云飞. 与替换和集合运算有关的错误*[J]. 软件学报, 1999, 10(2): 201-204 |
| |
| 作者姓名： | 程晓春 姜云飞 |
| |
| 作者单位： | 1. 吉林大学计算机科学系,长春,130023;长春科技大学,长春,130026
2. 中山大学软件所,广州,510275 |
| |
| 基金项目： | 本文研究得到国家自然科学基金和国家863高科技项目基金资助. |
| |
| 摘 要： | 指出在使用归结方法的自动推理文献中,存在于提升引理和删除策略完备性定理证明中,与替换和集合运算有关的几个错误,并予以分析和改正.
|
| 关 键 词： | 归结 替换 合一 集合 删除策略 |
| 收稿时间： | 1997-10-31 |
Errors Related to Substitution and Set Operations |
| |
| CHENG Xiao-chun and Jiang Yun-fei. Errors Related to Substitution and Set Operations[J]. Journal of Software, 1999, 10(2): 201-204 |
| |
| Authors: | CHENG Xiao-chun and 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. |
| |
| Keywords: | Resolution substitution unification set deletion strategy. |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
