计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2013年
20期
55-62
,共8页
支持补集%传递角色%角色层次%反向角色和数量约束的属性语言(SHIN)%ABox一致性判定%Tableau算法%阻塞机制%可终止性%合理性%完备性
支持補集%傳遞角色%角色層次%反嚮角色和數量約束的屬性語言(SHIN)%ABox一緻性判定%Tableau算法%阻塞機製%可終止性%閤理性%完備性
지지보집%전체각색%각색층차%반향각색화수량약속적속성어언(SHIN)%ABox일치성판정%Tableau산법%조새궤제%가종지성%합이성%완비성
attributive language with Complement,Transitive role,role Hierarchy,Inverse role,and Number restriction (SHIN)%ABox consistency decision%Tableau algorithm%blocking mechanism%termination%soundness%completeness
为了判定描述逻辑SHIN的ABox一致性，提出了一种Tableau算法。给定TBox T、ABox A和角色层次H，该算法通过预处理将A转换成标准的ABox A′，按照特定的完整策略将一套Tableau规则应用于 A′，直到将它扩展成完整的ABox A″为止。A与T和H一致，当且仅当算法能产生一个完整且无冲突的ABox A″。算法所采用的阻塞机制可以避免Tableau规则的无限次执行，该机制允许一个新个体被在其之前创建的任意新个体直接阻塞，而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明，算法的正确性得以确认。
為瞭判定描述邏輯SHIN的ABox一緻性，提齣瞭一種Tableau算法。給定TBox T、ABox A和角色層次H，該算法通過預處理將A轉換成標準的ABox A′，按照特定的完整策略將一套Tableau規則應用于 A′，直到將它擴展成完整的ABox A″為止。A與T和H一緻，噹且僅噹算法能產生一箇完整且無遲突的ABox A″。算法所採用的阻塞機製可以避免Tableau規則的無限次執行，該機製允許一箇新箇體被在其之前創建的任意新箇體直接阻塞，而不僅僅跼限于其祖先。通過對算法的可終止性、閤理性和完備性進行證明，算法的正確性得以確認。
위료판정묘술라집SHIN적ABox일치성，제출료일충Tableau산법。급정TBox T、ABox A화각색층차H，해산법통과예처리장A전환성표준적ABox A′，안조특정적완정책략장일투Tableau규칙응용우 A′，직도장타확전성완정적ABox A″위지。A여T화H일치，당차부당산법능산생일개완정차무충돌적ABox A″。산법소채용적조새궤제가이피면Tableau규칙적무한차집행，해궤제윤허일개신개체피재기지전창건적임의신개체직접조새，이불부부국한우기조선。통과대산법적가종지성、합이성화완비성진행증명，산법적정학성득이학인。
In order to decide ABox consistency for description logic SHIN, a Tableau algorithm is presented. Given a TBox T, an ABox A and a role hierarchy H, the algorithm 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 until A′ 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″. A blocking mechanism adopted by the algorithm can avoid infinite execution of Tableau rules. The mechanism allows a new individual to be directly blocked by any in-dividual created before it, which is not restricted to its ancestor. Through proving the termination, soundness and completeness of the algorithm, its correctness can be confirmed.
