The project belongs to a line of the ongoing research on the unification in the area of Description Logic. Description Logic (DL) is a formalism used for knowledge representation, where the knowledge is captured in complex concepts constructed from a set of primary terms with formal constructors. DL enables an application of automated inferences over a knowledge base such like answering queries in a smart way, computing concept hierarchies, detecting errors. The knowledge bases (sets of definitions of complex concepts), based on the constructors of DL, are called DL-knowledge bases or ontologies.
In this project we want to design an algorithm solving unification in a DL FLE. FLE avails of an expressive power sufficient to formalize all the knowledge contained in the targeted ontologies. The examples of such ontologies are
SNOMED CT, GALEN, FMA which represent medical, anatomical knowledge, and they are the intended area of the application of our research.
The unification problem is given in this context, as an input of a pair of complex concepts. The algorithm solving this problem should construct a set of definitions for hereto undefined primitive concepts occurring in the input such that, with these definitions the concepts in the input become unified, i.e. identical or equivalent. Subsequently, the set of
definitions obtained in this way has to be assessed by an expert, who can decide if they make sense. If the answer is
positive, the ontology can be repaired: the redundancy removed and the new definitions added. Thus, the unification algorithm may be of great help for the ontology engineers who work constantly on the extensions of the knowledge bases.
