摘要
子句集的可满足性判定是自动证明领域的热点之一。提出了子句搜索方法判定命题子句集Φ的可满足性,该方法查找Φ中子句的一个公共不可扩展子句C,当且仅当找到C时Φ可满足,此时C中各文字的补构成一个模型。结合部分实例化方法将子句搜索方法提升至一阶。一阶子句搜索方法可以判定子句集的M可满足性,具备终止性、正确性和完备性,是一种判定子句集可满足性的有效方法。
Deciding satisfiability of clause set is one of the active research topics in the automated reasoning field. A clause searching method of deciding satisfiability of propositional clause set Φ was proposed. This method first searched one clause C which cannot be extended from all clauses in Φ, if and only if C exists Φ was satisfied and the negative of C was one model. The authors updated clause searching method to first-order by partial instantiation method. Clause searching method in first-order logic can decide M satisfiablility of clause set and is of terminating, sound and complete property. It is a valid method for deciding satisfiability of clause set.
出处
《计算机应用》
CSCD
北大核心
2009年第11期3064-3067,共4页
journal of Computer Applications
基金
国家自然科学基金资助项目(90718041)
关键词
一阶逻辑
自动证明
可满足性
子句搜索方法
部分实例化方法
first-order logic
automated reasoning
satisfiability
clause searching method
partial instantiation method
