Abstract : Hybrid EL-TBoxes combine general concept inclusions (GCIs), which are interpreted with descriptive semantics, with cyclic concept definitions, which are interpreted with greatest fixpoint (gfp) semantics. We introduce a proof-theoretic approach that yields a polynomial-time decision procedure for subsumption in EL w.r.t. hybrid TBoxes, and present preliminary experimental results regarding the performance of the reasoner Hyb that implements this decision procedure.
Franz Baader, Novak Novakovic, Boontawee Suntisrivaraporn. A Proof-Theoretic Subsumption Reasoner for Hybrid EL-TBoxes. 21st International Workshop on Description Logics - DL 2008, May 2008, Dresden, Germany. ⟨inria-00336702⟩