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