Reasoning in EL-Description Logic with Refreshing Variables

Description logics have been widely studied and used in several knowledge-based systems. They allow to model knowledge and more importantly to reason over it. Subsumption relationship, a hierarchical relationship between concepts, is one of the most common reasoning task. Matching and unification generalize subsumption to description involving variables. In this paper, we study the problem of reasoning in description logics with variables. More specifically, we consider refreshing semantics for variables in the context of the EL description logic. We investigate a particular reasoning mechanism, namely weak subsumption, which can be viewed as a generalization of matching and unification in presence of refreshing variables. We show that weak-subsumption is EXPTIME-complete. Our main technical results are derived by establishing a correspondence between this logic and variable automata.