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

Published in Volume XXIII, Issue 2, 2013, pages 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 EL and EL⁺ can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient 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.

Full Text (PDF)

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 Articial Intelligence, pages 325-330, Morgan Kaufmann, 2003.

[3] F. Baader, C. Lutz, E. Karabaev, and M. Theißen. A new n-ary existential quantier in description logics. In Proc. 28th Annual German Conference on Articial 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 Articial 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 satisability 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 verication. 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 Articial 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.

Bibtex

@article{sacscuza:sofronie-stokkermans2013laatstieasoie,
  title={Locality and Applications to Subsumption Testing in mathcal{EL} and Some of its Extensions},
  author={V. Sofronie-Stokkermans},
  journal={Scientific Annals of Computer Science},
  volume={23},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2013},
  pages={251--284},
  doi={10.7561/SACS.2013.2.251},
  publisher={``A.I. Cuza'' University Press}
}