Top

Published in:

2020 | OriginalPaper | Chapter

Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq

Authors : Raul Fervari, Francisco Trucco, Beta Ziliani

Published in: Dynamic Logic. New Trends and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Over the last years, the study of logics that can modify a model while evaluating a formula has gained in interest. Motivated by many examples in practice such as hybrid logics, separation logics and dynamic epistemic logics, the ability of updating a model has been investigated from a more general point of view. In this work, we formalize and verify in the proof assistant Coq, the bisimulation theorems for a particular family of dynamic logics that can change the accessibility relation of a model. The benefits of this formalization are twofold. First, our results apply for a wide variety of dynamic logics. Second, we argue that this is the first step towards the development of a modal logic library in Coq, which allows us to mechanize many relevant results in modal logics.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

next chapter Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions

Areces, C., Fervari, R., Hoffmann, G.: Moving arrows and four model checking results. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 142–153. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32621-9_11CrossRefMATH

Areces, C., Fervari, R., Hoffmann, G.: Swap logic. Log. J. IGPL 22(2), 309–332 (2014)MathSciNetCrossRef

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

Areces, C., Fervari, R., Hoffmann, G., Martel, M.: Satisfiability for relation-changing logics. J. Log. Comput. 28(7), 1443–1470 (2018)MathSciNetCrossRef

Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory logics. Rev. Symb. Log. 4(2), 290–318 (2011)MathSciNetCrossRef

Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)CrossRef

Aucher, G., Balbiani, P., Fariñas del Cerro, L., Herzig, A.: Global and local graph modifiers. ENTCS 231, 293–307 (2009)MathSciNet

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

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)MATH

10.

Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)CrossRef

11.

Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1–84. Elsevier (2007)

12.

Bohrer, B., Platzer, A.: Toward structured proofs for dynamic logics. CoRR, abs/1908.05535 (2019)

13.

D’Abrera, C., Goré, R.: Verified synthesis of (very simple) Sahlqvist correspondents via Coq. In: AiML 2018, Short Presentations, pp. 26–30. College Publications (2018)

14.

de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26CrossRef

15.

de Wind, P.: Modal Logic in Coq. Vrije Universiteit, Amsterdam (2001)

16.

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

17.

Demri, S., Fervari, R., Mansutti, A.: Axiomatising logics with separating conjunction and modalities. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 692–708. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19570-0_45CrossRef

18.

Fervari, R.: Relation-Changing Modal Logics. Ph.D. thesis, Universidad Nacional de Córdoba, Argentina (2014)

19.

Fervari, R., Velázquez-Quesada, F.R.: Dynamic epistemic logics of introspection. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 82–97. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73579-5_6CrossRefMATH

20.

Fervari, R., Velázquez-Quesada, F.R.: Introspection as an action in relational models. JLAMP 108, 1–23 (2019)MathSciNetMATH

21.

Girard, P., Seligman, J., Liu, F.: General dynamic dynamic logic. In: AiML 2012, pp. 239–260. College Publications (2012)

22.

Gonthier, G.: Formal proof – the four-color theorem (2008)

23.

Hales, T.C., et al.: A formal proof of the kepler conjecture. Forum Math. Pi 5, e2 (2017)MathSciNetCrossRef

24.

Harel, D.: Dynamic Logic. Foundations of Computing. The MIT Press, Cambridge (2000)CrossRef

25.

Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: Essays Combin. Log. Lambda Calc. Formalism 44, 479–490 (1980)

26.

Kripke, S.: Semantical analysis of modal logic I. Normal propositional calculi. Z. fur Math. Log. Grundlagen der Math. 9, 67–96 (1963)MathSciNetCrossRef

27.

Löding, C., Rohde, P.: Model checking and satisfiability for sabotage modal logic. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 302–313. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24597-1_26CrossRef

28.

Mitsch, S., Platzer, A.: The keymaera X proof IDE - concepts on usability in hybrid systems theorem proving. In: F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016)CrossRef

29.

Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover, vol. 828. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0030541CrossRefMATH

30.

Pym, D., Spring, J., O’Hearn, P.W.: Why separation logic works. Philos. Technol. 32(3), 483–516 (2019)CrossRef

31.

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

32.

Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis, RWTH Aachen (2006)

33.

Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6 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., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Class. Log. 17(2), 157–182 (2007)MathSciNetCrossRef

36.

van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic epistemic logic with assignment. In: AAMAS 2005, pp. 141–148. ACM (2005)

37.

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

38.

Wu, M., Goré, R.: Verified decision procedures for modal logics. In: ITP 2019. LIPIcs, vol. 141, pp. 31:1–31:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

39.

Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in Coq. ENTCS 338, 219–236 (2018)MathSciNetMATH

Title: Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq
Authors: Raul Fervari
Francisco Trucco
Beta Ziliani
Publisher: Springer International Publishing
Book: Dynamic Logic. New Trends and Applications
Print ISBN: 978-3-030-38807-2

Electronic ISBN: 978-3-030-38808-9

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-38808-9_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner