%0 Journal Article
%T Horn集上的输入半锁归结原理
%A 刘叙华
%J 科学通报
%P 1201-1201
%D 1985
%X 归结原理是1965年由Robinson提出的一种重要的定理机器证明方法。1970年,Loveland和Luckham提出了线性归结,这是对归结原理的重要改进。一种特殊的线性归结——输入归结在计算机上极易实现。可惜,输入归结是不完备的。1974年Henschen和Wos研究了一种特殊子句集,即所谓Horn子句集。输入归结对于Horn集是完备的。1981年,陆汝铃对Horn集上的正单项有序归结和有序输入归结进行了研究,并得到很好的结果。
%U http://csb.scichina.com:8080/CN/abstract/abstract356514.shtml