Description logics are a family of knowledge representation that have been widely investigated and used in knowledge-based systems. The strength of description logics is beyond their modeling assets, it’s their reasoning abilities. Reasoning takes the shape of mechanisms that make the implicit knowledge explicit. One of the most common mechanism is based on the subsumption relationship. This relationship is a hierarchical relationship between concepts which aims to state if a concept is more general than another. The associated reasoning tasks aims to determine the subsumption relationship between two concepts. Variables have been introduced to description logic to answer the needs of representing incomplete information. In this context, deciding subsumption evolved into two non-standard reasoning tasks known as matching and unification. Matching aims to decide the subsumption relationship between a concept and a pattern (i.e. a concept expressed with variables). Unification extends matching to the case where both entries are patterns. The semantics associated to variables can be qualified as non-refreshing semantics where assignment are fixed.

In this thesis, we investigate reasoning with variables augmented with refreshing semantics. Refreshing semantics enables variables to be released and then given a new assignment. We define recursive pattern queries as terminologies that may contain variables leading to investigation of problems to answer recursive pattern queries over description logic ontologies. More specifically, we focus on the description logic EL. Recursive pattern queries are expressed in the logic ELRV , an extension of the description logic EL with variables equipped with refreshing semantics. We study the complexity of query answering and query containment in ELRV , two reasoning mechanisms that can be viewed as a variant of matching and unification in presence of refreshing variables. Our main technical results are derived by establishing a correspondence between this logic and a variant of variable automata. While the upper bound is given by specific algorithms which are proven to be optimal, the lower bound is achieved by a reduction to halting problem of alternating turing machine. Thus leading to these problems being exptime-complete.

Le jury est composé de :

• François Goasdoué, Professeur des universités , Université de Rennes,  Rapporteur       
• Nabil Layaïda, Directeur de recherche CNRS, INRIA Grenoble, Rapporteur   
• Mirian Halfeld Ferrari Alves, Professeur des universités, Université d'Orléans, Examinatrice       
• Farouk Toumani, Professeur des universités, Université Clermont Auvergne, Directeur de thèse
• Marinette Bouet, Maitre de conférences, Université Clermont Auvergne, Directrice de thèse.