nach oben

vorheriger Artikel A Conflict-Driven Solving Procedure for Poly-Po...

nächster Artikel Automating Free Logic in HOL, with an Experimen...

Tipp

ExpTime Tableaux with Global Caching for Hybrid PDL

Zeitschrift:: Journal of Automated Reasoning > Ausgabe 1/2020

Autor:: Linh Anh Nguyen

» Jetzt Zugang zum Volltext erhalten

Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

We present the first direct tableau decision procedure with the ExpTime complexity for HPDL (Hybrid Propositional Dynamic Logic). It checks whether a given ABox (a finite set of assertions) in HPDL is satisfiable. Technically, it combines global caching with checking fulfillment of eventualities and dealing with nominals. Our procedure contains enough details for direct implementation and has been implemented for the TGC2 (Tableaux with Global Caching) system. As HPDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Benthem, J.V., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, pp. 821–868. Elsevier, New York (2007)

Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69, 5–40 (2001) MathSciNetCrossRef

Blackburn, P.: Internalizing labelled deduction. J. Log. Comput. 10(1), 137–168 (2000) MathSciNetCrossRef

Blackburn, P., ten Cate, B.: Pure extensions, proof rules, and hybrid axiomatics. Studia Logica 84(2), 277–322 (2006) MathSciNetCrossRef

Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput. 17(3), 517–554 (2007) MathSciNetCrossRef

Bolander, T., Blackburn, P.: Terminating tableau calculi for hybrid logics extending K. Electr. Notes Theor. Comput. Sci. 231, 21–39 (2009) MathSciNetCrossRef

Bolander, T., Braüner, T.: Tableau-based decision procedures for hybrid logic. J. Log. Comput. 16(6), 737–763 (2006) MathSciNetCrossRef

Braüner, T.: Why does the proof-theory of hybrid logic work so well? J. Appl. Non-Class. Log. 17(4), 521–543 (2007) MathSciNetCrossRef

Braüner, T.: Hybrid logic. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, summer, 2017th edn. Stanford University, Metaphysics Research Lab (2017)

10.

Calvanese, D., De Giacomo, G., Lenzerini, M., Nardi, D.: Reasoning in expressive description logics. In: Robinson, J.A., Voronkov, A. (eds) Handbook of Automated Reasoning, vol. 2, pp. 1581–1634. Elsevier and MIT Press (2001)

11.

Cerrito, S., Mayer, M.C.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L.D., Goranko, V., Shehtman, V.B. (eds) Advances in Modal Logic 8, Papers from the Eighth Conference on Advances in Modal Logic held in Moscow, Russia, 24–27 August 2010, pp. 59–76. College Publications (2010)

12.

Divroodi, A., Nguyen, L.: On bisimulations for description logics. Inf. Sci. 295, 465–493 (2015) MathSciNetCrossRef

13.

Donini, F., Massacci, F.: ExpTime tableaux for \(\cal{ALC}\). Art. Intell. 124, 87–138 (2000) CrossRef

14.

Dunin-Kȩplicz, B., Nguyen, L., Szałas, A.: Converse-PDL with regular inclusion axioms: a framework for MAS logics. J. Appl. Non-Class. Log. 21(1), 61–91 (2011) MathSciNetCrossRef

15.

Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979) MathSciNetCrossRef

16.

Giacomo, G.D., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Proceedings of KR’1996, pp. 316–327 (1996)

17.

Goré, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Proceedings of IJCAR 2014, LNCS, vol. 8562, pp. 26–45. Springer (2014)

18.

Goré, R., Nguyen, L.: Analytic cut-free tableaux for regular modal logics of agent beliefs. In: Proceedings of CLIMA VIII, LNCS, vol. 5056, pp. 274–289. Springer (2007)

19.

Goré, R., Nguyen, L.: ExpTime tableaux for \(\cal{ALC}\) using sound global caching. J. Autom. Reason. 50(4), 355–381 (2013) MathSciNetCrossRef

20.

Goré, R., Postniece, L.: An experimental evaluation of global caching for \(\cal{ALC}\) (system description). In: Proceedings of IJCAR 2008, LNCS, vol. 5195, pp. 299–305. Springer (2008)

21.

Goré, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: R. Schmidt (ed.) Proceedings of CADE-22, LNAI 5663, pp. 437–452. Springer (2009)

22.

Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Proceedings of IJCAR 2010, LNCS, vol. 6173, pp. 225–239. Springer (2010)

23.

Hansen, J.: Terminating tableaux for dynamic epistemic logics. Electr. Notes Theor. Comput. Sci. 262, 141–156 (2010) MathSciNetCrossRef

24.

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, New York (2000) CrossRef

25.

Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason. 39(3), 249–276 (2007) MathSciNetCrossRef

26.

Kaminski, M., Smolka, G.: A goal-directed decision procedure for Hybrid PDL. J. Autom. Reason. 52(4), 407–450 (2014) MathSciNetCrossRef

27.

Kritsimallis, A.: Tableaux with partial caching for Hybrid PDL with satisfaction statements. In: Proceedings of ICTAC 2017, LNCS, vol. 10580, pp. 229–247. Springer (2017)

28.

Nguyen, L.: Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion axioms. In: Proc. of KES-AMSTA’2013, Frontiers in Artificial Intelligence and Applications, vol. 252, pp. 235–244. IOS Press (2013)

29.

Nguyen, L.: ExpTime tableaux with global state caching for the description logic \(\cal{SHIO}\). Neurocomputing 146, 249–263 (2014) CrossRef

30.

Nguyen, L.: Design of the tableau reasoner TGC2 for description logics. Int. J. Softw. Eng. Knowl. Eng. 26(8), 1315–1333 (2016) CrossRef

31.

Nguyen, L.: ExpTime tableaux with global caching for graded propositional dynamic logic. Fundam. Inf. 147(2–3), 261–288 (2016) MathSciNetCrossRef

32.

Nguyen, L., Golińska-Pilarek, J.: An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic \(\cal{SHOQ}\). Fundam. Inf. 135(4), 433–449 (2014) MathSciNetCrossRef

33.

Nguyen, L., Szałas, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL. Fundam. Inf. 102(1), 97–113 (2010) MathSciNetCrossRef

34.

Pratt, V.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2), 231–254 (1980) MathSciNetCrossRef

35.

Sattler, U., Vardi, M.: The hybrid \(\mu \)-calculus. In: Proceedings of IJCAR 2001, LNCS, vol. 2083, pp. 76–91. Springer (2001)

36.

Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of IJCAI’1991, pp. 466–471 (1991)

37.

Seligman, J.: Internalization: The case of hybrid logics. J. Log. Comput. 11(5), 671–689 (2001) MathSciNetCrossRef

38.

Tzakova, M.: Tableau calculi for hybrid logics. In: Proceedings of TABLEAUX’99, LNCS, vol. 1617, pp. 278–292. Springer (1999)

Titel: ExpTime Tableaux with Global Caching for Hybrid PDL
Autor:: Linh Anh Nguyen
Publikationsdatum: 01.01.2019
DOI: https://doi.org/10.1007/s10817-018-09506-8
Verlag: Springer Netherlands
Zeitschrift: Journal of Automated Reasoning
Ausgabe 1/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670

Premium Partner

Bildnachweise

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Publisher's Note

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2020

Priority Inheritance Protocol Proved Correct

Politeness and Combination Methods for Theories with Bridging Functions

Automating Free Logic in HOL, with an Experimental Application in Category Theory

A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

A Conflict-Driven Solving Procedure for Poly-Power Constraints

Premium Partner