Scientific Annals of Computer Science

"Alexandru Ioan Cuza" University of Iaşi



Locality and Applications to Subsumption Testing in EL and Some of its Extensions

Published in, p. 251-284, doi: 10.7561/SACS.2013.2.251

Authors: V. Sofronie-Stokkermans

ABSTRACT

In this paper we show that subsumption problems in the description logics {{mathcal|EL}} and EL+ can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of e ficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for TBox and CBox subsumption in EL and EL+. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend EL and EL+ with n-ary roles and/or numerical domains.

Keywords: description logics, deduction, hierarchical reasoning

Full text (PDF) | BibTeX

References


[1] F. Baader. Restricted role-value-maps in a description logic with existential restrictions and terminological cycles. In Proc. of the 2003 International Workshop on Description Logics (DL2003), CEUR-WS, 2003.

[2] F. Baader. Terminological cycles in a description logic with existential restrictions. In: G. Gottlob and T. Walsh, editors, Proc. of the 18th International Joint Conference in Arti cial Intelligence, pages 325-330, Morgan Kaufmann, 2003.

[3] F. Baader, C. Lutz, E. Karabaev, and M. Theißen. A new n-ary existential quanti er in description logics. In Proc. 28th Annual German Conference on Arti cial Intelligence (KI 2005), LNAI 3698, pages 18-33, Springer, 2005.

[4] F. Baader, C. Lutz, B. Suntisrivaraporn. Is tractable reasoning in extensions of the description logic EL useful in practice? Journal of Logic, Language and Information (M4M special issue), 2007.

[5] F. Baader, S. Brandt, and C. Lutz. Pushing the EL Envelope. In Proceedings of the Nineteenth International Joint Conference on Arti cial Intelligence IJCAI-05, pages 364-369, Morgan-Kaufmann Publishers, 2005.

[6] F. Baader, C. Lutz, and B. Suntisrivaraporn, Ecient Reasoning in EL+, In Proceedings of the 2006 International Workshop on Description Logics (DL2006), CEUR-WS, 2006.

[7] S. Burris. Polynomial time uniform word problems. Mathematical Logic Quarterly, 41:173{182, 1995. http://dx.doi.org/10.1002/malq.19950410204

[8] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[9] W.F. Dowling and J.H. Gallier. Linear time algorithms for testing the satis ability of propositional Horn formulae. J. Logic Programming, 1(3(: 267-284, 1984.

[10] H. Ganzinger. Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In Proc. 16Th IEEE Symposium on Logic in Computer Science (LICS'01), pages 81-92. IEEE Computer Society Press, 2001. http://dx.doi.org/10.1109/LICS.2001.932485

[11] R. Givan and D. McAllester. New results on local inference relations. In Principles of Knowledge Representation and reasoning: Proceedings of the Third International Conference (KR'92), pages 403-412. Morgan Kaufmann Press, 1992.

[12] R. Givan and D.A. McAllester. Polynomial-time computation via local inference relations. ACM Transactions on Computational Logic, 3(4):521-541, 2002. http://dx.doi.org/10.1145/566385.566387

[13] C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in veri cation. In Proc. TACAS 2008, LNCS 4963, pages 265-281, Springer 2008. http://dx.doi.org/10.1007/978-3-540-78800-3_19

[14] C. Ihlemann, V. Sofronie-Stokkermans. On Hierarchical Reasoning in Combinations of Theories. In Proceedings of IJCAR-2010, LNCS 6173, pages 30-45, Springer 2010. http://dx.doi.org/10.1007/978-3-642-14203-1_4

[15] A. Kurucz, F. Wolter, M. Zakharyaschev. On P/NP Dichotomies for EL Subsumption under Relational Constraints. In Proc. of the 2011 International Workshop on Description Logics (DL 2011), CEUR Workshop Proceedings 745, 2011.

[16] D. Magka, Y. Kazakov, I. Horrocks. Tractable Extensions of the Description Logic EL with Numerical Datatypes. Journal of Automated Reasoning, 47(4): 427-450, 2011 http://dx.doi.org/10.1007/s10817-011-9235-0

[17] D. Magka, Y. Kazakov, I. Horrocks. Tractable Extensions of the Description Logic EL with Numerical Datatypes. Journal of Automated Reasoning, 47(4): 427-450, 2011 http://dx.doi.org/10.1007/s10817-011-9235-0

[18] T. Skolem. Logisch-kombinatorische Untersuchungen ü ber die Erfü llbarkeit und Beweisbarkeit mathematischer Sä tze nebst einem Theorem uber dichte Mengen. Skrifter utgit av Videnskabsselskapet i Kristiania, I. Matematisk-naturvidenskabelig klasse, 4, pages 1-36, 1920.

[19] V. Sofronie-Stokkermans. Automated theorem proving by resolution in non-classical logics. Annals of Mathematics and Arti cial Intelligence (Special issue "Knowledge Discovery and Discrete Mathematics: Dedicated to the Memory of Peter L. Hammer"), 49 (1-4): 221-252, 2007. http://dx.doi.org/10.1007/s10472-007-9051-8

[20] V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In R. Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20(, LNAI 3632, pages 219-234. Springer, 2005. http://dx.doi.org/10.1007/11532231_16

[21] V. Sofronie-Stokkermans. Interpolation in local theory extensions. In IJCAR'2006: Int. Joint Conf. on Automated Reasoning, LNCS 4130, pages 235-250. Springer, 2006. http://dx.doi.org/10.1007/11814771_21

[22] V. Sofronie-Stokkermans. Interpolation in local theory extensions. Logical Methods in Computer Science 4(4):Paper 1, 2008. http://dx.doi.org/10.2168/ LMCS-4(4:1)2008.

[23] V. Sofronie-Stokkermans. Locality and subsumption testing in EL and some of its extensions. In Proceedings of DL 2008, CEUR Workshop Proceedings 353, 2008.

[24] V. Sofronie-Stokkermans. Locality and subsumption testing in EL and some of its extensions. Advances in Modal Logic (Proceedings of AiML 2008), pages 315-339, College Publications, 2008.

[25] V. Sofronie-Stokkermans and C. Ihlemann. Automated reasoning in some local extensions of ordered structures. Journal of Multiple-Valued Logics and Soft Computing cSpecial issue dedicated to ISMVL'07), 13 (4-6), 397-414, 2007. http://dx.doi.org/10.1109/ISMVL.2007.10

[26] K.A. Spackman, K.E. Campbell, R.A. C^ote. SNOMED RT: A reference terminology for health care. Journal of the Americal Medical Informatics Association, pages 640-644, 1997. Fall Symposium Supplement.

[27] K.A. Spackman. Normal forms for description logic expression of clinical concepts in SNOMED RT. Journal of the Americal Medical Informatics Association, pages 627{631, 2001. Symposium Supplement.

[28] K.A. Spackman, R. Dionne, E. Mays and J. Weis. Role Grouping as an Extension to the Description Logic of Ontylog motivated by Concept Modelling in SNOMED. Proceedings of the AMIA Symposium (2002), pages 712-716, 2002.


© 2006-2017 FII | Contact: annals at info.uaic.ro