一阶子句搜索方法

• 作者: 曾振柄 郭远华
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 一阶逻辑 自动证明 可满足性 子句搜索方法 部分实例化方法
• 年，卷（期）: 2009,（11）
• 所属期刊栏目: 人工智能与先进计算
• 页码范围: 3064-3067
• 页数: 4页
• 分类号: TP181
• 字数: 5306字
• 语种: 中文

摘要

子句集的可满足性判定是自动证明领域的热点之一.提出了子句搜索方法判定命题子句集Φ的可满足性,该方法查找Φ中子句的一个公共不可扩展子句C,当且仅当找到C时Φ可满足,此时C中各文字的补构成一个模型.结合部分实例化方法将子句搜索方法提升至一阶.一阶子句搜索方法可以判定子句集的M可满足性,具备终止性、正确性和完备性,是一种判定子句集可满足性的有效方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾振柄	华东师范大学上海市高可信计算重点实验室	29	105	6.0	8.0
2	郭远华	华东师范大学上海市高可信计算重点实验室	6	13	2.0	3.0