查看文章

A Description Logic (DL) system is characterized by four fundamental aspects: the set of constructs used in concept and role expressions, the kind of assertions allowed in the TBox (assertions on concepts) and the ABox (assertions on individuals), and the inference mechanisms for reasoning on both the TBox and the ABox. Most of the research done in the last decade made several simplifying assumptions on the above aspects. However, the recent interest in DLs exhibited in many application areas (databases, software engineering, intelligent access to the network, planning, etc.) calls for investigating DL systems with full capabilities. The work presented in this paper represents a step in this direction. We present a sound, complete, and terminating (in worst-case EXPTIME) inference procedure that solves the problem of reasoning in a DL system with the following characteristics: it comes equipped with a very expressive language, it allows the most general form of TBox assertions, and it takes into account instance assertions on both concepts and roles in the ABox.