Reasoning for ALCQ extended with a flexible meta-modelling hierarchy
This work addresses a specific need in ontology engineering for real-world applications, but it is incremental as it builds on existing Description Logic frameworks.
The paper tackles the problem of integrating and relating existing ontologies through meta-modelling by introducing the Description Logic ALCQM, an extension of ALCQ that allows concepts to be individuals of other concepts in a hierarchical manner, and presents a tableau algorithm for checking ontology consistency with a proof of correctness.
This works is motivated by a real-world case study where it is necessary to integrate and relate existing ontologies through meta- modelling. For this, we introduce the Description Logic ALCQM which is obtained from ALCQ by adding statements that equate individuals to concepts in a knowledge base. In this new extension, a concept can be an individual of another concept (called meta-concept) which themselves can be individuals of yet another concept (called meta meta-concept) and so on. We define a tableau algorithm for checking consistency of an ontology in ALCQM and prove its correctness.