描述逻辑ALC中的ABOX反绎推理算法

鉴于已有的描述逻辑ALC中ABOX反绎推理算法需要转化到FOL上处理,涉及了大量变元和Skolem项的使用。ALC-Tableau可以避免大量变元和斯科伦项,给出了一种直接在ALC上处理ABOX反绎推理问题的算法。该算法将ABOX反绎推理问题转化为知识库的一致性问题,在此基础上结合反绎推理的自身特性对传统的Tableau构造过程进行扩充,最终借助一个回溯过程找出反绎问题的所有解。