【摘要】 对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-based算法在有限步之内判定.更多还原

【Abstract】 The tableau-based algorithm for consistency checking of Aboxes is simplified and improved.The proposed standard tableau-based algorithm not only deletes the redundant part after each rule,but also gives up the restriction on the order of transformation rules.So this is a simplification and an improvement of the algorithm,and the finite step halting theorem for checking consistency of ALCN Aboxes is obtained therefrom.更多还原