摘要
本文将RUE-NRF归结使用在广义子句集上,提出了广义RUE-NRF归结方法,并证明了这一方法对于一阶逻辑的完备性;将1型、2型删除策略引入广义RUE-NRF归结.
The present paper covers the application of RUE-NRF resolution to a set of generalized clauses by proposing a generalized RUE-NRF resolution method, and a proof of the completeness of this method in first order logic. Furthermore, 1-model and 2-model deletion strategies are introduced into generalized RUE-NRF resolution.
出处
《吉林大学自然科学学报》
CAS
CSCD
1993年第1期37-40,共4页
Acta Scientiarum Naturalium Universitatis Jilinensis
基金
国家自然科学基金
国家教委博士点基金
国家863计划
国家攀登计划项目资助课题
关键词
调解
RUE-NRF
归结
消解
广义消解
generalized resolution, paramodulation , RUE-NRF resolution
