输入调解法和单元调解法在Horn集上的完备性  

COMPLETENESS OF INPUT PARAMODULATION AND UNIT PARAMODULATION ON HORN SET

作　　者：欧阳丹彤[1] 孙吉贵[1] 刘叙华[1] 

机构地区：[1]吉林大学计算机科学系,长春130023

出　　处：《软件学报》1993年第1期6-11,共6页Journal of Software

基　　金：国家自然科学基金;国家教委博士点基金

摘　　要：本文证明了调解法的提升引理,以及输入调解法对Horn集的完备性,进而证出了单元调解法对Horn集的完备性。Here we have proved the lifting lemma of paramodulation and the completeness of input paramodulation on Horn set, and then we have also proved the completeness of unit paramodulation on Horn set.

关 键 词：调解法 单元调解法 完备性 HORN集 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]