CAJ | 학술논문

为判定描述逻辑SHIQ的ABox一致性，提出一种Tableau算法。给定TBox T、ABox A和角色层次H，通过预处理将A转换成标准的ABox A’，按照特定的完整策略将一套Tableau规则应用于A’，从而不断地对A’进行扩展，直到将其扩展成完整的ABox A’’为止。A、T和H一致，当且仅当算法能产生一个完整且无冲突的ABox A’’。该算法采用的阻塞机制能防止Tableau规则被无限次执行，避免多余的规则应用。通过证明Tableau规则的执行次数为有限次，确认算法的可终止性。通过证明由A’’能构造一个同时满足A、T和H的解释，确认算法的合理性。通过证明Tableau规则的执行不会破坏A’与H的一致关系，确认算法的完备性。
위판정묘술라집SHIQ적ABox일치성，제출일충Tableau산법。급정TBox T、ABox A화각색층차H，통과예처리장A전환성표준적ABox A’，안조특정적완정책략장일투Tableau규칙응용우A’，종이불단지대A’진행확전，직도장기확전성완정적ABox A’’위지。A、T화H일치，당차부당산법능산생일개완정차무충돌적ABox A’’。해산법채용적조새궤제능방지Tableau규칙피무한차집행，피면다여적규칙응용。통과증명Tableau규칙적집행차수위유한차，학인산법적가종지성。통과증명유A’’능구조일개동시만족A、T화H적해석，학인산법적합이성。통과증명Tableau규칙적집행불회파배A’여H적일치관계，학인산법적완비성。
In order to decide ABox consistency for Description Logic(DL) SHIQ, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm first converts A into a standard ABox A’ by pre-disposal, and then applies a set of Tableau rules to A’ according to specific completion strategies, thus A’ is extended continually, until it is extended to a complete ABox A’’. A is consistent with T and H, if and only if the algorithm can yield a complete and clash-free ABox A’’. The blocking mechanism adopted by the algorithm can prevent Tableau rules’ unlimited execution, and avoid redundant rule application. By proving Tableau rules’ execution times is limited, the algorithm’s termination is ensured. By proving Tableau rules’ excecution is unlikely to destroy the consistency between A’ and H, the algorithm’s soundness is ensured. By proving an explanation which satisfies A, T and H can be constructed in terms of A’’, the algorithm’s completeness is ensured.