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