自由变量语义tableau中δ-规则的一种改进方法

自动推理一直是人工智能领域研究的重要内容 近几年来 ,由于tableau方法的通用性和直观性 ,引起人工智能界的广泛关注 对于自由变量语义tableau中的量词规则 ,由于γ 规则替换的任意性 ,可导致在同一tableau证明中γ 规则被多次使用 ,使得tableau推理结构树中出现多个自由变量 针对tableau中多次出现自由变量 ,使tableau封闭延迟的问题 ,在δ+ 规则的基础上 ,提出对δ+ 规则改进的δ+ + 规则 ,并进行了正确性证明 将δ+ + 规则应用到TableauTAP系统中 ,结果表明 ,δ+ + 规则使tableau封闭提前 。