一种基于集合符号的自动推理扩展方法

被引:4
作者
刘全 [1 ]
伏玉琛 [1 ]
孙吉贵 [2 ]
崔志明 [1 ]
龚声蓉 [1 ]
凌兴宏 [1 ]
机构
[1] 苏州大学计算机科学与技术学院
[2] 吉林大学符号计算与知识工程教育部重点实验室
关键词
集合符号; 自动推理; Tableau; 经典逻辑; 非经典逻辑;
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
在多值逻辑Tableau推理的基础上,提出了一种基于集合符号的自动推理扩展方法.将符号集合作为真值,减少了Tableau的推理分枝,并可以将适合经典逻辑的推理方法和策略应用于其中,使得非经典逻辑推理经典化.使用SWI-PROLOG语言设计实现了基于集合符号的自动推理系统,在系统中使用集合符号方法,只需要在规则库中增加推理规则,即可生成规则程序,系统本身不需要任何的修改,因此一些适合于经典逻辑的推理方法和技巧就可以很容易地应用到多值逻辑、模态逻辑、直觉逻辑等非经典逻辑,也可以进一步推广到无穷值逻辑和含模糊量词(如T-算子和S-算子)的逻辑中,对于无穷值逻辑和模糊逻辑的Tableau方法研究具有一定的借鉴作用.对TPTP中的900个逻辑问题进行了证明,实验结果表明,系统在时间和空间上效率都是较高的.
引用
收藏
页码:1317 / 1323
页数:7
相关论文
共 2 条
[1]   自由变量语义tableau中δ-规则的一种改进方法 [J].
刘全 ;
孙吉贵 ;
于万钧 .
计算机研究与发展, 2004, (07) :1068-1073
[2]   Commodious axiomatization of quantifiers in multiple-valued logic [J].
Hähnle R. .
Studia Logica, 1998, 61 (1) :101-121