Checking Consistency of an ABox w.r.t. Global Assumptions in PDL

• Autorzy: Nguyen L.A. L.A. , Szałas A.
• Języki publikacji: EN

Abstrakty

EN

We reformulate Pratt's tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first EXPTIME (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove a new result that the data complexity of the instance checking problem in PDL is coNP-complete.

Słowa kluczowe

EN

propositional dynamic logic; checking consistency

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 1
• Strony: 97--113
• Opis fizyczny: Bibliogr. 29 poz.

Twórcy

autor

Nguyen L.A. L.A.

autor

Szałas A.

• Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warsaw, Poland,

Bibliografia

• [1] Abate, P., Goré, R., Widmann, F.: An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability, Electr. Notes Theor. Comput. Sci., 231, 2009, 191-209.
• [2] Baader, F.: Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles, Proceedings of IJCAI'91, 1991.
• [3] Baader, F., Sattler, U.: An Overview of Tableau Algorithms for Description Logics, Studia Logica, 69, 2001, 5-40.
• [4] Calvanese, D., De Giacomo, G., Lenzerini, M.: Representing and Reasoning on XML Documents: A Description Logic Approach, Journal of Logic and Computation, 9(3), 1999, 295-318.
• [5] Calvanese, D., De Giacomo, G., Lenzerini, M., Nardi, D.: Reasoning in Expressive Description Logics, in: Handbook of Automated Reasoning, Elsevier, 2001, 1581-1634.
• [6] De Giacomo, G.: Decidability of Class-Based Knowledge Representation Formalisms, Ph.D. Thesis, Universita' di Roma "La Sapienza", 1995.
• [7] De Giacomo, G., Lenzerini, M.: TBox and ABox Reasoning in Expressive Description Logics, Proceedings of KR'1996, 1996.
• [8] De Giacomo, G., Massacci, F.: Combining deduction and model checking into tableaux and algorithms for Converse-PDL, Information and Computation, 117-137, 2000, 87-138.
• [9] Doherty, P., Dunin-Kęplicz, B., Szałas, A.: Dynamics of Approximate Information Fusion, Proc. RSEISP 2007 (M. Kryszkiewicz, J. Peters, H. Rybinski, A. Skowron, Eds.), number 4585 in LNAI, Springer-Verlag, 2007.
• [10] Donini, F., Massacci, F.: EXPTime tableaux for ALC, Art. Intelligence, 124, 2000, 87-138.
• [11] Fischer, M., Ladner, R.: Propositional Dynamic Logic of Regular Programs, J. Comput. Syst. Sci., 18(2), 1979, 194-211.
• [12] Goré, R., Nguyen, L.: EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies, Proc. of TABLEAUX 2007, LNAI 4548 (N. Olivetti, Ed.), Springer-Verlag, 2007.
• [13] Goré, R., Nguyen, L.: Sound Global Caching for Abstract Modal Tableaux, Proceedings of CS&P'2008 (H.-D. B. et al, Ed.), 2008.
• [14] Goré, R., Widmann, F.: An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability, Proceedings of CADE-22, LNAI 5663 (R. Schmidt, Ed.), Springer-Verlag, 2009.
• [15] Halpern, J., Moses, Y.: A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief, Artificial Intelligence, 54, 1992, 319-379.
• [16] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic, MIT Press, 2000.
• [17] Hustadt, U., Motik, B., Sattler, U.: Data Complexity of Reasoning in Very Expressive Description Logics., Proceedings of IJCAI-05, 2005.
• [18] http://www.irit.fr/Lotrec/.
• [19] Marx, M.: Conditional XPath, ACM Transactions on Database Systems, 30(4), 2005, 929-959.
• [20] Nguyen, L.: An Efficient Tableau Prover using Global Caching for the Description Logic ALC, Fundamenta Informaticae, 93(1-3), 2009, 273-288.
• [21] Nguyen, L., Szałas, A.: ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse, Manuscript, available at http://www.mimuw.edu.pl/~nguyen/creg-long.pdf, 2009.
• [22] Nguyen, L., Szałas, A.: An Optimal Tableau Decision Procedure for Converse-PDL, Proceedings of KSE'2009 (N.-T. Nguyen, T.-D. Bui, E. Szczerbicki, N.-B. Nguyen, Eds.), IEEE Computer Society, 2009.
• [23] Nguyen, L., Szałas, A.: Optimal Tableau Decision Procedures for PDL, http://arxiv.org/abs/0904.0721, 2009.
• [24] Nguyen, L., Szałas, A.: A Tableau Calculus for Regular Grammar Logics with Converse, Proceedings of CADE-22, LNAI 5663 (R. Schmidt, Ed.), Springer-Verlag, 2009.
• [25] Niwiński, D., Walukiewicz, I.: Games for the mu-Calculus, Theor. Comput. Sci., 163(1&2), 1996, 99-116.
• [26] Pratt, V.: A Near-Optimal Method for Reasoning about Action, J. Comput. Syst. Sci., 20(2), 1980, 231-254.
• [27] Schaerf, A.: Reasoning with Individuals in Concept Languages, Data Knowl. Eng., 13(2), 1994, 141-176.
• [28] Schild, K.: A Correspondence Theory for Terminological Logics: Preliminary Report, Proceedings of IJCAI'1991, 1991.
• [29] Schmidt, R.: http://www.cs.man.ac.uk/~schmidt/pdl-tableau/.