The Research On ABox Consistency Decision Algorithms For Description Logic SHIF And SHIQ

Description logics are a family of knowledge representation formalisms, and they have been widely applied in the field of knowledge representation, in that they are equipped with formal syntax and semantics and support inferences based on semantics. SHIF and SHIQ are two extensions to the basic description logic ALC, which are more expressive than ALC and are able to solve more complicated knowledge modeling problems. ABox consistency problem is one of the most important inference problems for Description logics, but has only received little attention in the study. In order to solve ABox consistency problems for SHIF and SHIQ, ABox consistency decision algorithms for these two description logics were studied in this thesis, and the following results were achieved.An ABox consistency decision algorithm for SHIF was presented and its correctness was proved. To decide whether a ABox Ain is consistent with regard to a TBox T, the algorithm first converts Ain into a standard ABox As by pre-disposal, and then continually applies specific Tableau rules in arbitrary order to As until it turns into a complete ABox. If the algorithm could yield a complete and clash-free ABox, it gives a positive answer, else give a negative answer. The "improved blocking" mechanism adopted by the algorithm can restrict the application of Tableau rules, which thereby ensures the algorithm could terminate in the case that the input objects only have infinite models. By proving termination, soundness and completeness of the algorithm, its correctness was confirmed.An ABox consistency decision algorithm for SHIQ was presented and its correctness was proved. To decide whether a ABox Ain is consistent with regard to a TBox T and a role hierarchy H, the algorithm first converts Ain into a standard ABox As by pre-disposal, and then continually applies specific Tableau rules in arbitrary order to As until it turns into a complete ABox. If the algorithm could yield a complete and clash-free ABox, it gives a positive answer, else give a negative answer. To ensure termination, the algorithm also adopts improved blocking. The proof of soundness and completeness of this algorithm is similar to that of the previous algorithm, while the proof of its termination adopts a new method, which makes use of a property of well-founded relations.The ABox consistency decision algorithm for SHIQ was implemented. The algorithm was first changed into a deterministic one, correctness of which was proved by means of a ABox tree, and then it was implemented as a program. Because SHIF is a sub-language of SHIQ, the program could also be used to decide ABox consistency for SHIF.