Representation Theorems and Locality for Subsumption Testing and Interpolation in the Description Logics εL; εL+ and their Extensions with n-ary Roles and Numerical Domains

• Autorzy: Sofronie-Stokkermans V.

Identyfikatory

DOI

10.3233/FI-2017-1612

• Języki publikacji: EN

Abstrakty

EN

In this paper we show that subsumption problems in lightweight description logics (such as εL and εL⁺) 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 CBox subsumption in εL, εL⁺ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend εL and εL⁺ with n-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of εL and εL⁺ have ground interpolation and thus that εL, εL⁺, and their extensions studied in this paper have interpolation.

Słowa kluczowe

EN

assimilation theory; interpolation algorithms; description logics; word problem; monotone operators

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 156, nr 3/4
• Strony: 361--411
• Opis fizyczny: Bibliogr. 43 poz., tab.

Twórcy

autor

Sofronie-Stokkermans V.

• University Koblenz-Landau, Universitätsstraße 1, 56070 Koblenz, Germany

Bibliografia

• [1] Baader F. Terminological Cycles in a Description Logic with Existential Restrictions. In: Gottlob G, Walsh T (eds.), IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003. Morgan Kaufmann, 2003 pp. 325–330. URL http://ijcai.org/Proceedings/03/Papers/048.pdf.
• [2] Spackman KA, Campbell KE, Côté RA. SNOMED RT: A reference terminology for health care. In: AMIA 1997, American Medical Informatics Association Annual Symposium, Nashville, TN, USA, October 25-29, 1997. AMIA, 1997 URL http://knowledge.amia.org/amia-55142-a1997a-1.585351/t-001-1.587519/f-001-1.587520/a-127-1.587635/a-128-1.587632.
• [3] Spackman KA. Normal forms for description logic expressions of clinical concepts in SNOMED RT. In: AMIA 2001, American Medical Informatics Association Annual Symposium, Washington, DC, USA, November 3-7, 2001. AMIA, 2001 URL http://knowledge.amia.org/amia-55142-a2001a-1.597057/t-001-1.599654/f-001-1.599655/a-126-1.599761/a-127-1.599758.
• [4] Baader F, Lutz C, Suntisrivaraporn B. Is tractable reasoning in extensions of the description logic εL useful in practice? Journal of Logic, Language and Information, 2007. Special issue on Method for Modality (M4M), 2007.
• [5] Baader F, Lutz C, Suntisrivaraporn B. Efficient Reasoning in εL+. In: Parsia B, Sattler U, Toman D (eds.), Proceedings of the 2006 International Workshop on Description Logics (DL2006), Windermere, Lake District, UK, May 30-June 1, 2006, volume 189 of CEUR Workshop Proceedings. CEUR-WS.org, 2006 URL http://ceur-ws.org/Vol-189/submission_8.pdf.
• [6] Baader F, Brandt S, Lutz C. Pushing the EL Envelope. In: Kaelbling LP, Saffiotti A (eds.), IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30-August 5, 2005. Professional Book Center, 2005 pp. 364–369. URL http://ijcai.org/Proceedings/05/Papers/0372.pdf.
• [7] Baader F. Restricted Role-value-maps in a Description Logic with Existential Restrictions and Terminological Cycles. In: Calvanese D, Giacomo GD, Franconi E (eds.), Proceedings of the 2003 International Workshop on Description Logics (DL2003), Rome, Italy September 5-7, 2003, volume 81 of CEUR Workshop Proceedings. CEUR-WS.org, 2003 URL http://ceur-ws.org/Vol-81/baader.pdf.
• [8] Rasiowa H, Sikorski R. The Mathematics of Metamathematics. Państwowe Wydawnictwo Naukowe, 1963.
• [9] Rasiowa H. An Algebraic Approach to Non-Classical Logics. Elsevier Science, 1974.
• [10] Sofronie-Stokkermans V. Hierarchic Reasoning in Local Theory Extensions. In: Nieuwenhuis R (ed.), Automated Deduction-CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632 of Lecture Notes in Computer Science. Springer, 2005 pp. 219–234. doi:10.1007/11532231_16. URL https://doi.org/10.1007/11532231_16.
• [11] Sofronie-Stokkermans V. Interpolation in Local Theory Extensions. In: Furbach U, Shankar N (eds.), Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science. Springer, 2006 pp. 235–250. doi:10.1007/11814771_21. URL https://doi.org/10.1007/11814771_21.
• [12] Sofronie-Stokkermans V. Interpolation in Local Theory Extensions. Logical Methods in Computer Science, 2008. 4(4). doi:10.2168/LMCS-4(4:1)2008. URL https://doi.org/10.2168/LMCS-4(4:1) 2008.
• [13] Sofronie-Stokkermans V, Ihlemann C. Automated Reasoning in Some Local Extensions of Ordered Structures. Multiple-Valued Logic and Soft Computing, 2007. 13(4-6):397–414. URL http://www.oldcitypublishing.com/MVLSC/MVLSCabstracts/MVLSC13.4-6abstracts/MVLSCv13n4-6p397-413Sofronie.html.
• [14] Ihlemann C, Sofronie-Stokkermans V. On Hierarchical Reasoning in Combinations of Theories. In: Giesl J, Hähnle R (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science. Springer, 2010 pp. 30–45. doi:10.1007/978-3-642-14203-1_4. URL https://doi.org/10.1007/978-3-642-14203-1_4.
• [15] Jacobs S, Sofronie-Stokkermans V. Applications of Hierarchical Reasoning in the Verification of Complex Systems. Electr. Notes Theor. Comput. Sci., 2007. 174(8):39–54. doi:10.1016/j.entcs.2006.11.038. URL https://doi.org/10.1016/j.entcs.2006.11.038.
• [16] Ihlemann C, Jacobs S, Sofronie-Stokkermans V. On Local Reasoning in Verification. In: Ramakrishnan CR, Rehof J (eds.), Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science. Springer, 2008 pp. 265–281. doi:10.1007/978-3-540-78800-3_19. URL https://doi.org/10.1007/978-3-540-78800-3_19.
• [17] Sofronie-Stokkermans V. Efficient Hierarchical Reasoning about Functions over Numerical Domains. In: Dengel A, Berns K, Breuel TM, Bomarius F, Roth-Berghofer T (eds.), KI 2008: Advances in Artificial Intelligence, 31st Annual German Conference on AI, KI 2008, Kaiserslautern, Germany, September 23-26, 2008. Proceedings, volume 5243 of Lecture Notes in Computer Science. Springer, 2008 pp. 135–143. doi:10.1007/978-3-540-85845-4_17. URL https://doi.org/10.1007/978-3-540-85845-4_17.
• [18] Sofronie-Stokkermans V. Hierarchical Reasoning for the Verification of Parametric Systems. In: Giesl J, Hähnle R (eds.), Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science. Springer, 2010 pp. 171–187. doi:10.1007/978-3-642-14203-1_15. URL https://doi.org/10.1007/978-3-642-14203-1_15.
• [19] Sofronie-Stokkermans V. Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems. In: Bonacina MP (ed.), Automated Deduction-CADE-24-24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science. Springer, 2013 pp. 360–376. doi:10.1007/978-3-642-38574-2_25. URL https://doi.org/10.1007/978-3-642-38574-2_25.
• [20] Sofronie-Stokkermans V. Locality and Subsumption Testing in EL and Some of its Extensions. In: Baader F, Lutz C, Motik B (eds.), Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, volume 353 of CEUR Workshop Proceedings. CEURWS. org, 2008 URL http://ceur-ws.org/Vol-353/Sofronie-Stokkermans.pdf.
• [21] Sofronie-Stokkermans V. Locality and subsumption testing in EL and some of its extensions. In: Areces C, Goldblatt R (eds.), Advances in Modal Logic 7, papers from the seventh conference on ”Advances in Modal Logic,” held in Nancy, France, 9-12 September 2008. College Publications, 2008 pp. 315–339. URL http://www.aiml.net/volumes/volume7/Sofronie-Stokkermans.pdf.
• [22] Sofronie-Stokkermans V. Locality and Applications to Subsumption Testing in EL and Some of its Extensions. Sci. Ann. Comp. Sci., 2013. 23(2):251–284. doi:10.7561/SACS.2013.2.251. URL https://doi.org/10.7561/SACS.2013.2.251.
• [23] Lemmon EJ. Algebraic Semantics for Modal Logics I. J. Symb. Log., 1966. 31(1):46–65. doi:10.2307/2270619. URL https://doi.org/10.2307/2270619.
• [24] Lemmon EJ. Algebraic Semantics for Modal Logics II. J. Symb. Log., 1966. 31(2):191–218. doi:10.2307/2269810. URL https://doi.org/10.2307/2269810.
• [25] Jónsson B, Tarski A. Boolean algebras with operators, Part I. American Journal of Mathematics, 1951. 73:891–939.
• [26] Jónsson B, Tarski A. Boolean algebras with operators, Part II. American Journal of Mathematics, 1952. 74:127–162.
• [27] Goldblatt R. Varieties of Complex Algebras. Ann. Pure Appl. Logic, 1989. 44(3):173–242. doi:10.1016/0168-0072(89)90032-8. URL https://doi.org/10.1016/0168-0072(89)90032-8.
• [28] van Benthem J. Correspondence theory. In: Gabbay D, Guenthner F (eds.), Handbook of Philosophical Logic, volume 2, pp. 167–247. Reidel, 1984.
• [29] Skolem T. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischer Sätze nebst einem Theorem über dichte Mengen. Skrifter utgit av Videnskabsselskapet i Kristiania, I. Matematisk-naturvidenskabelig klasse, 4, 1920. pp. 1–36.
• [30] Burris S. Polynomial Time Uniform Word Problems. Math. Log. Q., 1995. 41:173–182. doi:10.1002/malq.19950410204. URL https://doi.org/10.1002/malq.19950410204.
• [31] Givan R, McAllester DA. New Results on Local Inference Relations. In: Nebel B, Rich C, Swartout WR (eds.), Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR’92). Cambridge, MA, October 25-29, 1992. Morgan Kaufmann, 1992 pp. 403–412.
• [32] Givan R, McAllester DA. Polynomial-time computation via local inference relations. ACM Trans. Comput. Log., 2002. 3(4):521–541. doi:10.1145/566385.566387. URL http://doi.acm.org/10.1145/566385.566387.
• [33] Ganzinger H. Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 2001 pp. 81–90. doi:10.1109/LICS.2001.932485. URL https://doi.org/10.1109/LICS.2001.932485.
• [34] Davey BA, Priestley HA. Introduction to Lattices and Order. Cambridge University Press, 1990.
• [35] Sofronie-Stokkermans V. Automated theorem proving by resolution in non-classical logics. Ann. Math. Artif. Intell., 2007. 49(1-4):221–252. doi:10.1007/s10472-007-9051-8. URL https://doi.org/10.1007/s10472-007-9051-8.
• [36] Baader F, Lutz C, Brandt S. Pushing the EL Envelope Further. In: Clark K, Patel-Schneider PF (eds.), Proceedings of the Fourth OWLED Workshop on OWL: Experiences and Directions, Washington, DC, USA, 1-2 April 2008., volume 496 of CEUR Workshop Proceedings. CEUR-WS.org, 2008 URL http://ceur-ws.org/Vol-496/owled2008dc_paper_3.pdf.
• [37] Baader F, Karabaev E, Lutz C, Theißen M. A New n-Ary Existential Quantifier in Description Logics. In: Furbach U (ed.), KI 2005: Advances in Artificial Intelligence, 28th Annual German Conference on AI, KI 2005, Koblenz, Germany, September 11-14, 2005, Proceedings, volume 3698 of Lecture Notes in Computer Science. Springer, 2005 pp. 18–33. doi:10.1007/11551263_4. URL https://doi.org/10.1007/11551263_4.
• [38] Dowling WF, Gallier JH. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. Log. Program., 1984. 1(3):267–284. doi:10.1016/0743-1066(84)90014-1. URL https://doi.org/10.1016/0743-1066(84)90014-1.
• [39] Nebel B, Bürckert H. Reasoning about Temporal Relations: A Maximal Tractable Subclass of Allen’s Interval Algebra. J. ACM, 1995. 42(1):43–66. doi:10.1145/200836.200848. URL http://doi.acm.org/10.1145/200836.200848.
• [40] Jónsson B. Extensions of relational structures. In: Addison J, Henkin L, Tarski A (eds.), The Theory of Models, Proc. of the 1963 Symposium at Berkeley. North-Holland, Amsterdam, 1965 pp. 146–157.
• [41] Bacsich PD. Amalgamation properties and interpolation theorem for equational theories. Algebra Universalis, 1975. 5:45–55.
• [42] Wroński A. On a form of equational interpolation property. In: Dorn G, Weingartner P (eds.), Foundations of Logic and Linguistics (Salzburg, 1983), pp. 23–29. Springer, New York, 1985.
• [43] Konev B, Walther D, Wolter F. The Logical Difference Problem for Description Logic Terminologies. In: Armando A, Baumgartner P, Dowek G (eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science. Springer, 2008 pp. 259–274. doi:10.1007/978-3-540-71070-7_21. URL https://doi.org/10.1007/978-3-540-71070-7_21.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).