Extension Rule in First Order Logic

摘要：

The extension rule (ER) is a new method for theorem proving, which is potentially a complementary method to resolution-based methods. But the first-order ER method is incomplete. We improve the first-order ER approach by (a) revise the definition of the potential blockage, give a complete first-order ER algorithm, (b) increasing the case M-satisfiability by giving a bound M, so as to make the ER method more usejul for theorem proving and logic programming, and (c) accelerating it through invoking the more efficient proposition ER method. We also prove the soundness and completeness of the improved first-order ER algorithm and report some preliminary computational results.

作者: Xia Wu Jigui Sun Kun Hou

作者单位: College of Computer Science and Technology, Jilin University, 130012 Changchun, China;Key Laboratory College of Computer Science and Technology, Jilin University, 130012 Changchun, China;Key Laboratory

会议类型: 国际会议

会议名称: Firth IEEE International Conference on Cognitive Informatics(第五届认知信息国际会议)

会议地点: 北京

会议语种:英文

页码: 701-706

在线出版日期: 2006-07-17（万方平台首次上网日期，不代表论文的发表时间）