Deciding the SHOQ(D)-Satisfiability with a Fully Tiered Clause Group

SHOQ(D) is one of the fundamental theories In Description Logics due to its support to concrete datatypes and named individuals. At present, deciding the satisfiability of SHOQ(D)-concepts is mainly completed by enhancing Tableau algorithm with blocking. However, there is still much to be desired in performance as there are tremendous description overlaps in completion forest, thus causing great spatial waste as a result. To tackle this problem, this paper presented a new approach to check the satisfiability of acyclic SHOQ(D)-concepts——FTC(Fully Tiered Clauses) algorithm. This calculus can make a direct judgement on the satisfiability of acyclic SHOQ(D)-concept by translating its description into a fully tiered clause group whose satisfiability is directly available, and reusing clauses to block unnecessary extensions. FTC algorithm eliminates description overlaps to the largest extent as it works on concept description directly. Therefore, FTC algorithm has notably better performance than Tableau by saving a lot of spatial costs.