nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Axiomatising Logics with Separating Conjunction and Modalities

verfasst von : Stéphane Demri, Raul Fervari, Alessio Mansutti

Erschienen in: Logics in Artificial Intelligence

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics \(\text {MSL} ^{}(*,\langle \ne \rangle )\) and \(\text {MSL} ^{}(*,\Diamond )\), where \(*\) is the separating conjunction, \(\Diamond \) is the standard modal operator and \(\langle \ne \rangle \) is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

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 "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

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

Vorheriges Kapitel Interpolation and Beth Definability in Default Logics

Nächstes Kapitel Nested Sequents for the Logic of Conditional Belief

The class Tower [31] is the class of problems of time complexity bounded by a tower of exponentials, whose height is an elementary function of the input.

Areces, C., Fervari, R.: Hilbert-style axiomatization for hybrid XPath with data. In: Michael, L., Kakas, A. (eds.) JELIA 2016. LNCS (LNAI), vol. 10021, pp. 34–48. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48758-8_3CrossRef

Areces, C., Fervari, R., Hoffmann, G.: Tableaux for relation-changing modal logics. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 263–278. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_19CrossRef

Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Logic J. IGPL 23(4), 601–627 (2015)MathSciNetCrossRef

Aucher, G., van Benthem, J., Grossi, D.: Modal logics of sabotage revisited. JLC 28(2), 269–303 (2018)MathSciNetMATH

Balbiani, Ph., Tinchev,T.: Unification in modal logic Alt\(_1\). In: AiML 2016, pp. 117–134. College Publications (2016)

Berdine, Josh, Calcagno, Cristiano, O’Hearn, Peter W.: A Decidable Fragment of Separation Logic. In: Lodaya, Kamal, Mahajan, Meena (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30538-5_9CrossRefMATH

Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge University Press (2001)

Blackburn, P., van Benthem, J.F., Wolter, F. (eds.): Handbook of Modal Logic. Elsevier (2006)

Boudou, J.: Decidable logics with associative binary modalities. In: LIPIcs CSL 2017, vol. 82, pp. 1–15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

10.

Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. Ann. Pure Appl. Logic 161(3), 305–323 (2009)MathSciNetCrossRef

11.

Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL 2014, pp. 453–464. ACM (2014)

12.

Calvanese, D., Kotek, T., Šimkus, M., Veith, H., Zuleger, F.: Shape and content. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 3–17. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_1CrossRef

13.

Courtault, J.-R., Galmiche, D.: A modal separation logic for resource dynamics. JLC 28(4), 733–778 (2018)MathSciNetMATH

14.

Courtault, J.-R., van Ditmarsch, H., Galmiche, D.: A public announcement separation logic. Math. Struct. Comput. Sci. (2019, to appear)

15.

Courtault, J.-R., van Ditmarsch, H., Galmiche, D.: An epistemic separation logic. In: de Paiva, V., de Queiroz, R., Moss, L.S., Leivant, D., de Oliveira, A.G. (eds.) WoLLIC 2015. LNCS, vol. 9160, pp. 156–173. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47709-0_12CrossRefMATH

16.

Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. IC 205(3), 263–310 (2007)MathSciNetMATH

17.

Demri, S., Deters, M.: Two-variable separation logic and its inner circle. ToCL 2(16), 15:1–15:36 (2015)MATH

18.

Demri, S., Fervari, R.: On the complexity of modal separation logics. In: AiML 2018, pp. 179–198. College Publications (2018)

19.

Demri, S., Lozes, É., Mansutti, A.: The effects of adding reachability predicates in propositional separation logic. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 476–493. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_26CrossRefMATH

20.

Doumane, A.: Constructive completeness for the linear-time \(\mu \)-calculus. In: LICS 2017, pp. 1–12. IEEE Computer Society (2017)

21.

Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03182-7CrossRefMATH

22.

Echenim, M., Iosif, R., Peltier, N.: On the expressive completeness of Bernays-Schönfinkel-Ramsey separation logic. Technical report arXiv:1802.00195, arXiv:cs.LO, February 2018. To appear in FOSSACS 2019

23.

Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51803-7_36CrossRef

24.

Gierasimczuk, N., Kurzen, L., Velázquez-Quesada, F.R.: Learning and teaching as a game: a sabotage approach. In: He, X., Horty, J., Pacuit, E. (eds.) LORI 2009. LNCS (LNAI), vol. 5834, pp. 119–132. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04893-7_10CrossRefMATH

25.

Herzig, A.: A simple separation logic. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds.) WoLLIC 2013. LNCS, vol. 8071, pp. 168–178. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39992-3_16CrossRefMATH

26.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef

27.

Hou, Z., Clouston, R., Goré, R., Tiu, A.: Modular labelled sequent calculi for abstract separation logics. ToCL 19(2), 13:1–13:35 (2018)MathSciNetCrossRef

28.

Lu, X., Tian, C., Duan, Z.: Temporalising separation logic for planning with search control knowledge. In: IJCAI 2017, pp. 1167–1173 (2017)

29.

Pym, D., Spring, J., O’Hearn, P.W.: Why separation logic works. In: Philosophy and Technology, pp. 1–34 (2018). https://doi.org/10.1007/s13347-018-0312-8

30.

Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE (2002)

31.

Schmitz, S.: Complexity hierarchies beyond elementary. ACM Trans. Comput. Theor. 8(1), 3:1–3:36 (2016)MathSciNetCrossRef

32.

Segerberg, K.: A note on the logic of elsewhere. Theoria 47, 183–187 (1981)MathSciNet

33.

Shoham, Y., Leyton-Brown, K.: Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, New York (2008)CrossRef

34.

Benthem, J.: An essay on sabotage and obstruction. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 268–276. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32254-2_16CrossRef

35.

van Benthem, J.: Logical Dynamics of Information and Interaction. Cambridge University Press (2011)

36.

van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese Library Series, vol. 337. Springer, Dordrecht (2008). https://doi.org/10.1007/978-1-4020-5839-4CrossRefMATH

37.

Wang, Y., Cao, Q.: On axiomatizations of public announcement logic. Synthese 190(Supplement–1), 103–134 (2013)MathSciNetCrossRef

Titel: Axiomatising Logics with Separating Conjunction and Modalities
verfasst von: Stéphane Demri
Raul Fervari
Alessio Mansutti
Verlag: Springer International Publishing
Buch: Logics in Artificial Intelligence
Print ISBN: 978-3-030-19569-4

Electronic ISBN: 978-3-030-19570-0

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-19570-0_45

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 "Technik"

Springer Professional "Wirtschaft"