摘要
本文在广义λ-归结方法中引进删除策略,讨论了λ-蕴涵的若干性质,并证明:以λ-蕴涵为基础的删除策略不破坏广义λ-归结方法的完备性.
The present paper introduces the deletion strategy into generalized λ-resolution and discusses certain properties of λ-strong entailment. It is proved that deletion strategy based on λ-entailment doesn't destory the completeness of generalized λ-resolution method.
出处
《吉林大学自然科学学报》
CAS
CSCD
1993年第2期37-41,共5页
Acta Scientiarum Naturalium Universitatis Jilinensis
基金
国家自然科学基金
国家教委博士点基金
863计划
国家攀登计划资助课题
关键词
广义归结
Λ-归结
删除策略
generalized resolution, λ-resolution, deletion strategy