A Boolean Pruning Method for Improving Tableau Reasoning Efficiency in First-Order Many-Valued Logic
Quan Liu · Chinese Journal of Computers · 2003
Tableau method with quantifiers in first order many valued logic exist uniform expansion rules, and sound and complete have been proved by Zabel et al . But It is difficulty for computer to implement. Because the number of the branch which have been extended is very large. A Boolean pruning method is proposed in this paper. Tableau rules for such quantifiers can be simplified by providing a link between signed formulas and upset/downset in Boolean set lattices. In addition, through analyzing to Boolean pruning method, a simplified Tableau reasoning method is founded for regular formulas in first order many valued logic formulas. It is allowable for us to apply the same extension rules.