CEL (Classifier for EL) is a reasoner for the small description logic EL+ which can be used to compute the subsumption hierarchy induced by EL+ ontologies. The most distinguishing feature of CEL is that, unlike all other modern DL reasoners, it is based on a polynomial-time subsumption algorithm, which allows it to process very large ontologies in reasonable time. In spite of its restricted expressive power, EL+ is well-suited for formulating life science ontologies. The Description Logic underlying CEL The system CEL1 is a first step towards realizing the dream of a description logic system that offers both sound and complete polynomial-time algorithms and expressive means that allow its use in real-world applications. It is based on recent theoretical advances that have shown that the description logic (DL) EL, which allows for conjunction and existential restrictions, and some of its extensions have a polynomial-time subsumption problem even in the presence of concept definitions an...