Abstract
Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL \(\mathcal{EL}\), which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for \(\mathcal{EL}\) developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and descriptive semantics. We show that hybrid unification in \(\mathcal{EL}\) is NP-complete and introduce a goal-oriented algorithm for computing hybrid unifiers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), pp. 325–330. Morgan Kaufmann, Los Altos (2003)
Baader, F., Borgwardt, S., Morawska, B.: Unification in the description logic \(\mathcal{EL}\) w.r.t. cycle-restricted TBoxes. LTCS-Report 11-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany (2011), http://lat.inf.tu-dresden.de/research/reports.html
Baader, F., Borgwardt, S., Morawska, B.: Extending unification in \(\mathcal{EL}\) towards general TBoxes. In: Proc. of the 13th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2012), pp. 568–572. AAAI/MIT Press (2012)
Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in \(\mathcal{ELH}_{R+}\) w.r.t. Cycle-restricted ontologies. In: Thielscher, M., Zhang, D. (eds.) AI 2012. LNCS, vol. 7691, pp. 493–504. Springer, Heidelberg (2012)
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003)
Baader, F., Fernández Gil, O., Morawska, B.: Hybrid unification in the description logic \(\mathcal{EL}\). LTCS-Report 13-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany (2013), http://lat.inf.tu-dresden.de/research/reports.html
Baader, F., Morawska, B.: Unification in the description logic \(\mathcal{EL}\). In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350–364. Springer, Heidelberg (2009)
Baader, F., Morawska, B.: Unification in the description logic \(\mathcal{EL}\). Logical Methods in Computer Science 6(3) (2010)
Baader, F., Narendran, P.: Unification of concept terms in description logics. J. of Symbolic Computation 31(3), 277–305 (2001)
Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else? In: de Mántaras, R.L., Saitta, L. (eds.) Proc. of the 16th Eur. Conf. on Artificial Intelligence (ECAI 2004), pp. 298–302 (2004)
Brandt, S., Model, J.: Subsumption in \(\cal EL\) w.r.t. hybrid tboxes. In: Furbach, U. (ed.) KI 2005. LNCS (LNAI), vol. 3698, pp. 34–48. Springer, Heidelberg (2005)
Küsters, R.: Non-Standard Inferences in Description Logics. LNCS (LNAI), vol. 2100. Springer, Heidelberg (2001)
Novaković, N.: Proof-theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in EL w.r.t. Hybrid TBoxes. Master’s thesis, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Germany (2007), http://lat.inf.tu-dresden.de/research/mas/#Nov-Mas-07
Novaković, N.: A proof-theoretic approach to deciding subsumption and computing least common subsumer in \(\cal EL\) w.r.t. hybrid TBoxes. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 311–323. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Fernández Gil, O., Morawska, B. (2013). Hybrid Unification in the Description Logic \(\mathcal{EL}\) . In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-40885-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40884-7
Online ISBN: 978-3-642-40885-4
eBook Packages: Computer ScienceComputer Science (R0)