Abstract
The Description Logic \(\mathcal{EL}\) has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, \(\mathcal{EL}\) is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in \(\mathcal{EL}\) is decidable. More precisely, \(\mathcal{EL}\)-unification is NP-complete, and thus has the same complexity as \(\mathcal{EL}\)-matching. We also show that, w.r.t. the unification type, \(\mathcal{EL}\) is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F.: Unification in commutative theories. J. of Symbolic Computation 8(5) (1989)
Baader, F.: Terminological cycles in KL-ONE-based knowledge representation languages. In: Proc. AAAI 1990 (1990)
Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proc. IJCAI 2003 (2003)
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\mathcal{EL}\) envelope. In: Proc. IJCAI 2005 (2005)
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Baader, F., Küsters, R.: Matching in description logics with existential restrictions. In: Proc. KR 2000 (2000)
Baader, F., Küsters, R.: Unification in a description logic with transitive closure of roles. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, p. 217. Springer, Heidelberg (2001)
Baader, F., Küsters, R., Borgida, A., McGuinness, D.L.: Matching in description logics. J. of Logic and Computation 9(3) (1999)
Baader, F., Narendran, P.: Unification of concepts terms in description logics. J. of Symbolic Computation 31(3) (2001)
Baader, F., Nutt, W.: Basic description logics. In: [5] (2003)
Baader, F., Sertkaya, B., Turhan, A.-Y.: Computing the least common subsumer w.r.t. a background terminology. J. of Applied Logic 5(3) (2007)
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol. I. Elsevier Science Publishers, Amsterdam (2001)
Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else. In: Proc. ECAI 2004 (2004)
Ghilardi, S.: Best solving modal equations. Ann. Pure Appl. Logic 102(3) (2000)
Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From SHIQ and RDF to OWL: The making of a web ontology language. Journal of Web Semantics 1(1) (2003)
Kazakov, Y., de Nivelle, H.: Subsumption of concepts in \(\mathcal{FL}_0\) for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete. In: Proc. DL 2003. CEUR Electronic Workshop Proceedings (2003), http://CEUR-WS.org/Vol-81/
Küsters, R.: Non-Standard Inferences in Description Logics. LNCS (LNAI), vol. 2100. Springer, Heidelberg (2001)
Rector, A., Horrocks, I.: Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions. In: Proc. AAAI 1997 (1997)
Sofronie-Stokkermans, V.: Locality and subsumption testing in \(\mathcal{EL}\) and some of its extensions. In: Proc. AiML 2008 (2008)
Wolter, F., Zakharyaschev, M.: Undecidability of the unification and admissibility problems for modal and description logics. ACM Trans. Comput. Log. 9(4) (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Morawska, B. (2009). Unification in the Description Logic \(\mathcal{EL}\) . In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-02348-4_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02347-7
Online ISBN: 978-3-642-02348-4
eBook Packages: Computer ScienceComputer Science (R0)