A BOOLEAN PRUNING METHOD FOR IMPROVING TABLEAU REASONING EFFICIENCY IN FIRST-ORDER MULTIPLE-VALUED LOGICS

摘要：

Tableau method with quantifiers in first-order multiple-valued logic has uniform rules of extension, and sound and completeness have been proved by Zabel and so on.The number of branches increases in exponent with the increasing of truth-value, which will affect the performance efficiency of machine. A Boolean pruning method is proposed in this paper, which simplified the extended rules of logic formula with quantifiers in first-order multiple-valued greatly by linking the signed formula and upper/lower bound of set.In addition, through the analyzing of Boolean pruning method,simplified tableau reasoning method for a kind of special regular logic formulae in first-order multiple-valued was founded, which made logic tableau reasoning method with quantifiers in first-order multiple-valued is similar to classical logic tableau method.

关键词： Multiple-valued logics Quantifier Tableau method Upper/lower set Regular formula

作者: QUAN LIU ZHI-MING CUI JI-GUI SUN WAN-JUN YU

作者单位: College of Computer Science and Technology, Soochow University, Soochow 215006,China;Ministry of Edu College of Computer Science and Technology, Soochow University, Soochow 215006,China Ministry of Education Laboratory of Symbol Calculation and Knowledge Engineering, Jilin University,

会议类型: 国际会议

会议名称: 2006 International Conference on Machine Learning and Cybernetics(IEEE第五届机器学习与控制论坛)

会议地点: 大连

会议语种:英文

页码: 2548-2553

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