%0 Journal Article
%T 一阶子句搜索方法
%A 郭远华
%A 曾振柄
%J 计算机应用
%D 2009
%X ？子句集的可满足性判定是自动证明领域的热点之一。提出了子句搜索方法判定命题子句集φ的可满足性，该方法查找φ中子句的一个公共不可扩展子句c，当且仅当找到c时φ可满足，此时c中各文字的补构成一个模型。结合部分实例化方法将子句搜索方法提升至一阶。一阶子句搜索方法可以判定子句集的m可满足性，具备终止性、正确性和完备性，是一种判定子句集可满足性的有效方法。
%K 一阶逻辑
%K 自动证明
%K 可满足性
%K 子句搜索方法
%K 部分实例化方法
%U http://www.joca.cn/CN/abstract/abstract12387.shtml