A Proof-Theoretic Subsumption Reasoner for Hybrid EL-TBoxes

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.

• Type: Conference
• Year: 2008
• Where: DLOG
• Authors: Franz Baader, Novak Novakovik, Boontawee Suntisrivaraporn
• Keywords: Automated Reasoning, Cyclic Concept Definitions, Decision Procedure, DLOG 2008, Polynomial-time Decision Procedure