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. A goal-oriented NP unification algorithm for \(\mathcal{EL}\) that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this paper, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (\(\mathcal{H}\)) and transitive roles (R + ). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.
Supported by DFG under grant BA 1122/14-1.
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., Borgwardt, S., Mendez, J., Morawska, B.: UEL: Unification solver for \(\mathcal{EL}\). In: Proc. DL 2012. CEUR Workshop Proceedings, vol. 846 (2012)
Baader, F., Borgwardt, S., Morawska, B.: Extending unification in \(\mathcal{EL}\) towards general TBoxes. In: Proc. KR 2012, pp. 568–572. AAAI Press (2012) (short paper)
Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in \(\mathcal{ELH}_{R+}\) w.r.t. cycle-restricted ontologies. LTCS-Report 12-05, TU Dresden, Germany (2012), http://lat.inf.tu-dresden.de/research/reports.html
Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in \(\mathcal{EL}\) w.r.t. cycle-restricted TBoxes. In: Proc. DL 2012. CEUR Workshop Proceedings, vol. 846 (2012)
Baader, F., Borgwardt, S., Morawska, B.: SAT Encoding of Unification in \(\mathcal{ELH}_{{R}^+}\) w.r.t. Cycle-Restricted Ontologies. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 30–44. Springer, Heidelberg (2012)
Baader, F., Borgwardt, S., Morawska, B.: SAT encoding of unification in \(\mathcal{ELH}_{R^+}\) w.r.t. cycle-restricted ontologies. LTCS-Report 12-02, TU Dresden, Germany (2012), http://lat.inf.tu-dresden.de/research/reports.html
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\mathcal{EL}\) envelope. In: Proc. IJCAI 2005, pp. 364–369. Morgan Kaufmann (2005)
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.: SAT Encoding of Unification in \(\mathcal{EL}\). In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 97–111. Springer, Heidelberg (2010)
Baader, F., Morawska, B.: Unification in the description logic \(\mathcal{EL}\). Log. Meth. Comput. Sci. 6(3) (2010)
Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31(3), 277–305 (2001)
Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else? In: Proc. 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)
Gomes, C.P., Kautz, H., Sabharwal, A., Selman, B.: Satisfiability solvers. In: Handbook of Knowledge Representation, pp. 89–134. Elsevier (2008)
Hofmann, M.: Proof-theoretic approach to description-logic. In: Proc. LICS 2005. pp. 229–237. IEEE Press (2005)
Morawska, B.: General E-unification with eager variable elimination and a nice cycle rule. J. Autom. Reasoning 39(1), 77–106 (2007)
Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. IJCAI 1991, pp. 466–471 (1991)
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
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Borgwardt, S., Morawska, B. (2012). A Goal-Oriented Algorithm for Unification in \(\mathcal{ELH}_{R+}\) w.r.t. Cycle-Restricted Ontologies. In: Thielscher, M., Zhang, D. (eds) AI 2012: Advances in Artificial Intelligence. AI 2012. Lecture Notes in Computer Science(), vol 7691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35101-3_42
Download citation
DOI: https://doi.org/10.1007/978-3-642-35101-3_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35100-6
Online ISBN: 978-3-642-35101-3
eBook Packages: Computer ScienceComputer Science (R0)