论文部分内容阅读
自动推理一直是人工智能领域研究的重要内容 近几年来 ,由于tableau方法的通用性和直观性 ,引起人工智能界的广泛关注 对于自由变量语义tableau中的量词规则 ,由于γ 规则替换的任意性 ,可导致在同一tableau证明中γ 规则被多次使用 ,使得tableau推理结构树中出现多个自由变量 针对tableau中多次出现自由变量 ,使tableau封闭延迟的问题 ,在δ+ 规则的基础上 ,提出对δ+ 规则改进的δ+ + 规则 ,并进行了正确性证明 将δ+ + 规则应用到TableauTAP系统中 ,结果表明 ,δ+ + 规则使tableau封闭提前 ,在推理的时间效率和空间效率上都有较大的提高
Automatic reasoning has always been an important part of the field of artificial intelligence. In recent years, due to the versatility and intuition of the tableau method, widespread attention has been drawn to the artificial intelligence community. For the quantifier rules in the free variable semantic tableau, due to the arbitrary substitution of the γ rule, Which leads to the fact that the γ rule is used multiple times in the same tableau proof so that there are multiple free variables in the tableau inference tree. Based on the δ + rule, aiming at the problem that there are multiple free variables in tableau and the tableau closure is delayed, The δ + + rule improved for δ + rule is proved, and the correctness is proved. The δ + + rule is applied to TableauTAP system. The results show that δ + + rule makes tableau closed ahead of time, both in reasoning time efficiency and space efficiency There is a big improvement