Document Open Access Logo

Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge

Authors Kai Obendrauf , Anne Baanen , Patrick Koopmann , Vera Stebletsova

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.28.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Kai Obendrauf
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
Anne Baanen
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
Patrick Koopmann
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
Vera Stebletsova
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands

Funding

  • Baanen, Anne: NWO Vidi grant No. 016.Vidi.189.037, Lean Forward.

Cite AsGet BibTex

Kai Obendrauf, Anne Baanen, Patrick Koopmann, and Vera Stebletsova. Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.28

Abstract

Coalition Logic (CL) is a well-known formalism for reasoning about the strategic abilities of groups of agents in multi-agent systems. Coalition Logic with Common Knowledge (CLC) extends CL with operators from epistic logics, and thus with the ability to model the individual and common knowledge of agents. We have formalized the syntax and semantics of both logics in the interactive theorem prover Lean 4, and used it to prove soundness and completeness of its axiomatization. Our formalization uses the type class system to generalize over different aspects of CLC, thus allowing us to reuse some of to prove properties in related logics such as CL and CLK (CL with individual knowledge).

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Mathematics of computing → Mathematical software
  • Computer systems organization → Dependable and fault-tolerant systems and networks
Keywords
  • Multi-agent systems
  • Coalition Logic
  • Epistemic Logic
  • common knowledge
  • completeness
  • formal methods
  • Lean prover

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Thomas Ågotnes and Natasha Alechina. Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation, 29(7):1041-1069, 2019. URL: https://doi.org/10.1093/logcom/exv085.
  2. Mussab Alaa, Aos Alaa Zaidan, Bilal Bahaa Zaidan, Mohammed Talal, and Miss Laiha Mat Kiah. A review of smart home applications based on internet of things. Journal of Network and Computer Applications, 97:48-65, 2017. URL: https://doi.org/10.1016/j.jnca.2017.08.017.
  3. Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Theorem proving in lean 4. Accessed 2024-01-18. URL: https://lean-lang.org/theorem_proving_in_lean4/.
  4. Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg. The Hitchhiker’s Guide to Logical Verification. Vrije Universiteit Amsterdam, 2021 edition, 2021. Google Scholar
  5. Colm Baston and Venanzio Capretta. Game forms for coalition effectivity functions. In TYPES 2019, pages 26-27, 2019. URL: https://nottingham-repository.worktribe.com/output/2681068.
  6. Bruno Bentzen. A Henkin-style completeness proof for the modal logic S5. In Lecture Notes in Computer Science, pages 459-467. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-89391-0_25.
  7. Lubor Budaj. Formalization of modal logic S5 in the Coq proof assistant, 2022. Bachelor’s Thesis, University of Groningen. URL: https://fse.studenttheses.ub.rug.nl/28482/1/BSc_Thesis_final.pdf.
  8. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), volume 9195, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  9. Asta Halkjær From. Formalized soundness and completeness of epistemic logic. In Alexandra Silva, Renata Wassermann, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation, pages 1-15, Cham, 2021. Springer International Publishing. Google Scholar
  10. Herman Geuvers. Proof assistants: History, ideas and future. Sadhana, 34:3-25, 2009. Google Scholar
  11. Balaji Parasumanna Gokulan and Dipti Srinivasan. An introduction to multi-agent systems. In Dipti Srinivasan and Lakhmi C. Jain, editors, Innovations in Multi-Agent Systems and Applications, pages 1-27. Springer, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-14435-6_1.
  12. Valentin Goranko, Wojciech Jamroga, and Paolo Turrini. Strategic games and truly playable effectivity functions. Autonomous Agents and Multi-Agent Systems, 26(2):288-314, March 2013. URL: https://doi.org/10.1007/s10458-012-9192-y.
  13. Frans C. A. Groen, Matthijs T. J. Spaan, Jelle R. Kok, and Gregor Pavlin. Real world multi-agent systems: Information sharing, coordination and planning. In TbiLLC '05, volume 4363 of LNCS, pages 154-165, Cham, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-75144-1_12.
  14. Joni Helin. Combining deep and shallow embeddings. Electronic Notes in Theoretical Computer Science, 164(2):61-79, 2006. URL: https://doi.org/10.1016/j.entcs.2006.10.005.
  15. Thierry Lecomte, Thierry Servat, and Guilhem Pouzancre. Formal methods in safety-critical railway systems. In 10th Brasilian symposium on formal methods, pages 29-31, August 2007. Google Scholar
  16. Pierre Lescanne and Jérôme Puisségur. Dynamic logic of common knowledge in a proof assistant. (preprint), 2007. URL: https://doi.org/10.48550/arXiv.0712.3146.
  17. Jiatu Li. Formalization of pal⋅s5 in proof assistant. (preprint), 2020. URL: https://doi.org/10.48550/arXiv.2012.09388.
  18. Cláudia Nalon, Lan Zhang, Clare Dixon, and Ullrich Hustadt. A resolution prover for coalition logic. In Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146 of EPTCS, pages 65-73, 2014. URL: https://doi.org/10.4204/EPTCS.146.9.
  19. Paula Neeley. A formalization of dynamic epistemic logic. Master’s thesis, Carnegie Mellon University, 2021. Google Scholar
  20. Kai Obendrauf. CL-Lean Formalization. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:5679444e6dc3b26cd7f1c54786bff9be89541c19;origin=https://github.com/kaiobendrauf/cl-lean;visit=swh:1:snp:1f23793a440680675cf5720ee67fd69fe95b4a5b;anchor=swh:1:rev:bd4fba27cb459f14f0ec77b738de9cd02232671e (visited on 2024-07-08). URL: https://github.com/kaiobendrauf/cl-lean.
  21. Kai Obendrauf. Formalizing completeness proofs for coalition logic with and without common knowledge in Lean. Master’s thesis, Vrije Universiteit Amsterdam, 2023. URL: https://doi.org/10.5281/zenodo.12582708.
  22. Marc Pauly. A modal logic for coalitional power in games. Journal of Logic and Computation, 12(1):149-166, 2002. URL: https://doi.org/10.1093/logcom/12.1.149.
  23. Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. Tabled typeclass resolution. CoRR, abs/2001.04301, 2020. URL: https://arxiv.org/abs/2001.04301.
  24. Alfred Tarski. Über einige fundamentale Begriffe der Metamathematik. Sprawozdania z Posiedzeń Towarzystwa Naukowego Warszawskiego. Wydział III, 23:22-29, 1930. Google Scholar
  25. The mathlib Community. The Lean mathematical library. In CPP 2020, pages 367-381, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3372885.3373824.
  26. Johan Van Benthem. Games in dynamic-epistemic logic. Bulletin of Economic Research, 53(4):219-248, 2001. URL: https://doi.org/10.1111/1467-8586.00133.
  27. Wiebe van der Hoek and Michael J. Wooldridge. Logics for multiagent systems. AI Mag., 33(3):92-105, 2012. URL: https://doi.org/10.1609/aimag.v33i3.2427.
  28. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In POPL '89, Principles of Programming Languages, pages 60-76. ACM, 1989. URL: https://doi.org/10.1145/75277.75283.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact