| 提高一阶多值逻辑Tableau推理效率的布尔剪枝方法 |
| |
| 引用本文： | 刘全,孙吉贵.提高一阶多值逻辑Tableau推理效率的布尔剪枝方法[J].计算机学报,2003,26(9):1165-1170. |
| |
| 作者姓名： | 刘全 孙吉贵 |
| |
| 作者单位： | 吉林大学符号计算与知识工程教育部重点实验室,长春,130012;吉林大学计算机科学与技术学院,长春,130012 |
| |
| 基金项目： | 国家自然科学基金 ( 60 0 73 0 3 9,60 2 73 0 80 )，吉林省科技发展计划( 2 0 0 2 0 3 0 6)，吉林大学创新基金资助 |
| |
| 摘 要： | 含有量词的一阶多值Tableau方法具有统一的扩展规则，并由Zabel等人给出了可靠性和完备性的证明，但由于扩展后的分枝随着真值数目的增加而呈指数的增加，因而影响了机器推理执行的效率，该文提出了布尔剪枝方法，将带符号的公式与集合的上集／下集联系起来，使含量词的一阶多值逻辑公式的扩展规则大大简化，进一步，通过对布尔剪枝方法的分析，建立了一类特殊一阶多值逻辑正则公式的更为简洁的Tableau推理方法，该方法使得含量词的一阶多值逻辑Tableau推理类同于经典逻辑Tableau方法。
|
| 关 键 词： | 人工智能 Tableau推理效率 一阶多值Tableau方法 布尔剪枝方法 |
| 修稿时间： | 2002年1月28日 |
A Boolean Pruning Method for Improving Tableau Reasoning Efficiency in First-Order Many-Valued Logic |
| |
| LIU Quan,SUN Ji,Gui.A Boolean Pruning Method for Improving Tableau Reasoning Efficiency in First-Order Many-Valued Logic[J].Chinese Journal of Computers,2003,26(9):1165-1170. |
| |
| Authors: | LIU Quan SUN Ji Gui |
| |
| Abstract: | 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. |
| |
| Keywords: | many valued logic quantifier Tableau method upset/downset in set regular formula |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
