a - Semantic Resolution Method in Lattice-valued Logic
Resolution-based automated reasoning is one of most important research directions in Al, semantic method is one of the most important reform methods for resolution principle, in semantic resolution method, it utilize the technology that restraining the type of clauses and the order of literals participated in resolution procedure to reduce the redundant clauses, and can improve the efficiency of reasoning, a- resolution principle on lattice-valued logic based on lattice implication algebra provide a alternative tool to handle the automated reasoning problem with uncomparability and fuzziness information, it can refutably prove the unsatisfiability of logical formulae in lattice-valued logic system. Firstly, this paper discussed the property of one class of generalized clause set on lattice-valued propositional logic LP(X), this generalized clause set can be divided into two non-empty sets, the semantic resolution method on it is investigated and sound theorem and weak complete theorem of this semantic resolution method were proved.
Automated reasoning Resolution principle Semantic resolution Lattice-valued logic Lattice implication algebras
Jiafeng Zhang Yang Xu
Intelligent Control Development Center Southwest Jiaotong University Chengdu 610031, China Center of College of Maths Southwest Jiaotong University Chengdu 610031, China
国际会议
上海
英文
399-403
2011-07-26（万方平台首次上网日期，不代表论文的发表时间）