nach oben

Journal of Automated Reasoning

Erschienen in:

01.01.2019

ExpTime Tableaux with Global Caching for Hybrid PDL

verfasst von: Linh Anh Nguyen

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel A Conflict-Driven Solving Procedure for Poly-Power Constraints

Nächster Artikel Automating Free Logic in HOL, with an Experimental Application in Category Theory

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Let \(\varphi \) be a formula in HPDL\(_@\). Let \(a_1,\ldots ,a_h\) be all nominals, \(\sigma _1,\ldots ,\sigma _k\) all atomic programs and \(@_{a_{i_1}}\psi _1, \ldots , @_{a_{i_\ell }}\psi _\ell \) all satisfaction statements occurring in \(\varphi \). Let \(p_1,\ldots ,p_\ell \) be new propositions (i.e., atomic formulas) and \(\varphi '\), \(\psi '_1, \ldots , \psi '_\ell \) the formulas obtained from \(\varphi \), \(\psi _1, \ldots , \psi _\ell \), respectively, by replacing each satisfaction statement \(@_{a_{i_j}}\psi _j\) by \(p_j\), for \(1 \le j \le \ell \). Let \(\tau _0\) and \(\tau \) be new nominals and \(\varrho \) a new atomic program. Define \(\mathcal {A}\) to be the ABox consisting of the assertions \(\tau \!:\!\varphi '\), \(\varrho (\tau _0,\tau )\), \(\varrho (\tau _0,a_i)\) (for \(1 \le i \le h\)), \(\tau _0\!:\!(\langle \varrho \rangle (a_{i_j} \wedge \psi '_j) \rightarrow [(\varrho \cup \sigma _1 \cup \ldots \cup \sigma _h)^*]p_j)\) and \(\tau _0\!:\!(\langle \varrho \rangle (a_{i_j} \wedge \lnot \psi '_j) \rightarrow [(\varrho \cup \sigma _1 \cup \ldots \cup \sigma _h)^*]\lnot p_j)\) (for \(1 \le j \le \ell \)). Clearly, \(\mathcal {A}\) does not contain satisfaction statements. It can be shown that \(\varphi \) is satisfiable iff \(\mathcal {A}\) is satisfiable.

Note that \(\Sigma (\alpha )\) contains not only atomic programs but also expressions of the form \((\varphi ?)\), and a program \(\alpha \) is a regular expression over its alphabet \(\Sigma (\alpha )\).

That is, if \( Status (v) \notin \{ closed , closed\text {-}wrt (\ldots )\}\), then \( Status (v) := closed\text {-}wrt (\{u\})\), else if \( Status (v) = closed\text {-}wrt (U)\) then \( Status (v) := closed\text {-}wrt (U \cup \{u\})\).

As an optimization, if there exists \(\xi \in FullLabel (v)\) of the form \(o\!:\!\langle A,q\rangle \varphi \) or \(o\!:\!\langle \omega \rangle \langle A,q\rangle \varphi \) such that it is not \(\Diamond \)-realizable at v w.r.t. a complex state u that is an ancestor of v and checking \(\Diamond \)-realizability of \(\xi \) at v w.r.t. u does not go through any simple non-state whose label contains a nominal, then \(\Diamond \)-nonrealizability of \(\xi \) at v does not really depend on u, and \( Status (v)\) can be changed to \( closed \).

As an optimization, it makes sense to expand v only when there may exist a path from the root to v that does not contain any node with the status \( closed \).

This condition can be weakened, e.g., to that \(\mathcal {M}\) is finitely branching.

The steps 2a–2i of this loop correspond to the conditions 4a–4i of Definition 2, respectively.

If \(x_j \in V\), then \(o_i = null \), else either \(o_i = null \) or \(o_i = a_j\).

We require this due to the condition 4g of Definition 2. It may exclude transitions of the form \((q_i,\chi '_i?,q_i)\) of the automaton A but does not cause loss of generality when proving the property (2) at a later step.

Recall the remark in the caption of Fig. 1 on page 5.

There are evidences supporting the claim that global caching increases efficiency for reasoning in the DLs \(\mathcal {ALC}\) [20, 19, Section 8] and \(\mathcal {SHIQ}\) [30, Section 7]. We do not have evidences for the case of HPDL. In general, efficiency strongly depends also on optimizations and the applied search strategy.

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
verfasst von: Linh Anh Nguyen
Publikationsdatum: 01.01.2019
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-09506-8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2020

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

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

Priority Inheritance Protocol Proved Correct

Politeness and Combination Methods for Theories with Bridging Functions

A Conflict-Driven Solving Procedure for Poly-Power Constraints