ExpTime Tableaux with Global Caching for Graded Propositional Dynamic Logic

• Autorzy: Nguyen L. A.

Identyfikatory

DOI

10.3233/FI-2016-1408

• Konferencja: International Workshop on CONCURRENCY, SPECIFICATION, and PROGRAMMING (CS&P 2015), (24; 28-30.09.2015, Rzeszów, Poland).
• Języki publikacji: EN

Abstrakty

EN

We present the first direct tableau decision procedure for graded PDL, which uses global caching and has ExpTime (optimal) complexity when numbers are encoded in unary. It shows how to combine checking fulfillment of existential star modalities with integer linear feasibility checking for tableaux with global caching. As graded PDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.

Słowa kluczowe

EN

description logics; knowledge representation; computational complexity; reasoning; mathematical terminology

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 147, nr 2/3
• Strony: 261--288
• Opis fizyczny: Bibliogr. 16 poz., tab.

Twórcy

autor

Nguyen L. A.

• Division of Knowledge and System Engineering for ICT, Faculty of Information Technology, Ton Duc Thang University, Ho Chi Minh City, Vietnam
• Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland

Bibliografia

• [1] Fischer MJ, Ladner RE. Propositional Dynamic Logic of Regular Programs. J Comput Syst Sci. 1979; 18(2):194–211. doi:10.1016/0022-0000(79)90046-1.
• [2] Harel D, Kozen D, Tiuryn J. Dynamic Logic. MIT Press; 2000. ISBN:0262082896.
• [3] Dunin-Kęplicz B, Nguyen LA, Szałas A. Converse-PDL with regular inclusion axioms: a framework for MAS logics. Journal of Applied Non-Classical Logics. 2011;21(1):61–91. Available from: http://dx.doi.org/10.3166/jancl.21.61-91.
• [4] Giacomo GD, Lenzerini M. TBox and ABox Reasoning in Expressive Description Logics. In: Proceedings of KR’1996; 1996. p. 316–327.
• [5] Pratt VR. A Near-Optimal Method for Reasoning about Action. J Comput Syst Sci. 1980;20(2):231–254. doi:10.1016/0022-0000(80)90061-6.
• [6] Nguyen LA, Szałas A. Checking Consistency of an ABox w.r.t. Global Assumptions in PDL. Fundamenta Informaticae. 2010;102(1):97–113. Available from: http://dl.acm.org/citation.cfm?id=1883623.1883631.
• [7] Abate P, Goré R, Widmann F. An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability. Electronic Notes in Theoretical Computer Science. 2009;231:191–209. doi:10.1016/j.entcs.2009.02.036.
• [8] Nguyen LA, Szałas A. An Optimal Tableau Decision Procedure for Converse-PDL. In: Nguyen NT, Bui TD, Szczerbicki E, Nguyen NB, editors. Proceedings of KSE’2009. IEEE Computer Society; 2009. p. 207–214. Available from: http://dx.doi.org/10.1109/KSE.2009.12, doi: 10.1109/KSE.2009.12.
• [9] Goré R, Widmann F. Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse. In: Proceedings of IJCAR 2010. vol. 6173 of LNCS. Springer; 2010. p. 225–239. ISBN:978-3-642-14202-4. doi:10.1007/978-3-642-14203-1_20.
• [10] De Giacomo G, Lenzerini M. What’s in an Aggregate: Foundations for Description Logics with Tuples and Sets. In: Proceedings of IJCAI 95. Morgan Kaufmann; 1995. p. 801–807. Available from: http://dl.acm.org/citation.cfm?id=1625855.1625959.
• [11] Tobies S. Complexity results and practical algorithms for logics in knowledge representation. RWTH-Aachen; 2001. Available from: http://publications.rwth-aachen.de/record/52234/files/Tobies_Stephan.pdf.
• [12] Nguyen LA. ExpTime Tableaux with Global Caching for Graded Propositional Dynamic Logic. In: Proceedings of CS&P’2015. vol. 1492 of CEUR Workshop Proceedings. CEUR-WS.org; 2015. p. 44–56. Available from: http://ceur-ws.org/Vol-1492/Paper_29.pdf.
• [13] Nguyen LA. ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking; 2013. arXiv:1205.5838v4.
• [14] De Giacomo G, Lenzerini M. Boosting the Correspondence between Description Logics and Propositional Dynamic Logics. In: Proceedings of AAAI 1994. AAAI Press / The MIT Press; 1994. p. 205–212.
• [15] Nguyen LA. Designing a Tableau Reasoner for Description Logics. In: Proc. of ICCSAMA’2015. vol. 358 of Advances in Intelligent Systems and Computing. Springer; 2015. p. 321–333. ISBN: 978-3-319-17995-7, doi:10.1007/978-3-319-17996-4_29.
• [16] Nguyen LA, Golińska-Pilarek J. An ExpTime Tableau Method for Dealing with Nominals and Qualified Number Restrictions in Deciding the Description Logic SHOQ. Fundam Inform. 2014;135(4):433–449. Available from: http://dx.doi.org/10.3233/FI-2014-1133, doi:10.3233/FI-2014-1133.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).