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

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

作　　者：刘全[1] 孙吉贵[1] 窦全胜[1] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130023

出　　处：《计算机工程》2003年第8期128-130,136,共4页Computer Engineering

基　　金：国家自然科学基金资助项目(60073039);吉林省自然科学基金资助项目(2000540)

摘　　要：在多值逻辑中，含有量词的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.

关 键 词：多值规则公式 量词 TABLEAU 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]