Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Dynamic Logic

DALI 2019: Dynamic Logic. New Trends and Applications pp 3–18Cite as

Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq

  • Conference paper
  • First Online:

  • 284 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12005))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. 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_11

    Chapter  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

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

    MathSciNet  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    Book  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

  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_26

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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_45

    Chapter  Google Scholar 

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

    Google Scholar 

  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_6

    Chapter  MATH  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Book  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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_26

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

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

    Book  MATH  Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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_16

    Chapter  Google Scholar 

  35. van Benthem, J., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Class. Log. 17(2), 157–182 (2007)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Book  MATH  Google Scholar 

  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)

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

Download references

Ackowledgements

This work was partially supported by ANPCyT-PICTs-2017-1130 and 2016-0215, MinCyT Córdoba, SeCyT-UNC, and the Laboratoire International Associé INFINIS.

Author information

Authors and Affiliations

  1. FaMAF, Universidad Nacional de Córdoba, Córdoba, Argentina

    Raul Fervari, Francisco Trucco & Beta Ziliani

  2. Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Buenos Aires, Argentina

    Raul Fervari & Beta Ziliani

Authors
  1. Raul Fervari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francisco Trucco
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Beta Ziliani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Raul Fervari .

Editor information

Editors and Affiliations

  1. University of Minho, Braga, Portugal

    Luís Soares Barbosa

  2. Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, Noord-Holland, The Netherlands

    Alexandru Baltag

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fervari, R., Trucco, F., Ziliani, B. (2020). Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. In: Soares Barbosa, L., Baltag, A. (eds) Dynamic Logic. New Trends and Applications. DALI 2019. Lecture Notes in Computer Science(), vol 12005. Springer, Cham. https://doi.org/10.1007/978-3-030-38808-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-38808-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-38807-2

  • Online ISBN: 978-3-030-38808-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation