一种多值规则量词公式的tableau的方法

A Kind of Tableau Reasoning Method with Quantifiers in Many-valued Regular Logic

在多值逻辑中，含有量词的tableau方法具有统一的扩展规则，并已通过可靠性和完备性的证明。但是由于扩展后的分枝非常庞大，使机器实现非常困难。文章通过对规则量词公式与一阶经典量词公式的对应关系的研究，使二者使用统一的扩展规则。

Tableau method with q uantifiers in first-order many-valued logic exists uniform exitension rules, and reliability and completeness have been proved by Zabel and so on. But it is difficulty for computer to implement. Because the number of the branch having been extended is very large. 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 research relation between regular formulas and first-order classical for mulas, it is allowable for people to apply the same extension rules.