Description logics (DLs) are an important family of formalisms for reasoning about ontologies. CEL is the first reasoner for the Description Logic EL+, supporting as its main reasoning task the computation of the subsumption hierarchy induced by EL+ ontologies. The Description Logic EL+ forms the core expressive features of OWL 2 EL Profile -- which is a tractable fragment of the new Web Ontology Language OWL 2. The most distinguishing feature of CEL is that, unlike other modern DL reasoners, it implements a polynomial-time algorithm. The supported Description Logic EL+ offers a selected set of expressive means that are tailored toward the formulation of medical and biological ontologies.

From version 1.0, CEL also supports supplemental reasoning features like incremental classification, modularization and axiom pinpointing. Moreover, the OWL API wrapper for CEL has eventually become available, so now you can use CEL as the backend reasoner from within Protege!