Query containment is a well-studied problem spanning over several decades of research. Generally, it is defined as the problem of determining if the result of one query is included in the result of another query for any given dataset. It has major applications in query optimization and knowledge base verification. The main objective of this thesis is to provide sound and complete procedures to determine containment of SPARQL queries under expressive description logic axioms. Further, to support theoretical results by experimentation. To date query containment has been done using different techniques: containment mapping, canonical databases, automata theory techniques and through a reduction to the validity problem in logic. In this thesis, we use the later technique to address containment using an expressive logic called mu-calculus. In doing so, RDF graphs are encoded as transitions systems, and queries and schema axioms are encoded as mu-calculus formulae. Thereby, query containment can be reduced to validity test in the logic. The focus of this thesis is to identify various fragments of SPARQL (and PSPARQL) and description logic schema languages for which containment is decidable. Additionally, to provide theoretically and experimentally proven procedures to check containment of those decidable fragments. Last not but least, this thesis proposes a benchmark for containment solvers. This benchmark is used to test and compare the current state-of-the-art containment solvers.
