提高一阶多值逻辑Tableau推理效率的布尔剪枝方法

摘要：

含有量词的一阶多值Tableau方法具有统一的扩展规则,并由Zabel等人给出了可靠性和完备性的证明.但由于扩展后的分枝随着真值数目的增加而呈指数的增加,因而影响了机器推理执行的效率.该文提出了布尔剪枝方法,将带符号的公式与集合的上集/下集联系起来,使含量词的一阶多值逻辑公式的扩展规则大大简化.进一步,通过对布尔剪枝方法的分析,建立了一类特殊一阶多值逻辑正则公式的更为简洁的Tableau推理方法,该方法使得含量词的一阶多值逻辑Tableau推理类同于经典逻辑Tableau方法.

关键词：多值逻辑、量词、Tableau方法、集合的上集/下集、正则公式

所属期刊栏目：26

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60073039,60273080;吉林省科技发展计划20020306;吉林大学校科研和教改项目

在线出版日期：2003-11-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1165-1170