Description Logics (DLs) are a family of knowledge representation languages, used to reason with information sets in a structured and well-understood way. They play a big role in any field using large amounts of data, e.g. artificial intelligence, databases, and they are of importance in providing a logical formalism for ontologies and the Semantic Web. A common battle in the world of DLs is the one between expressivity, where we add fixpoints, inverses, role restrictions, etc, to a standard DL, and decidability. That is why more expressive as well as light-weight DLs are considered, which both benefit from different derivation system. In this talk I will first give an introduction on the general area of Description Logic, and then focus on the different reasoning problems and how they are solved proof-theoretically. The main result will be on Martin Hofmann’s paper, presenting the sequent calculus for the light description logic EL with the fixpoint extension, and see how cyclic proofs are used in this context. This talk is based on the reading course I did together with Bahareh Afshari as a preparation for my Master thesis.