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).
| Original language | English |
|---|---|
| Title of host publication | 15th International Conference on Interactive Theorem Proving (ITP 2024) |
| Subtitle of host publication | [Proceedings] |
| Editors | Yves Bertot, Temur Kutsia, Michael Norrish |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 1-18 |
| Number of pages | 18 |
| ISBN (Electronic) | 9783959773379 |
| DOIs | |
| Publication status | Published - Sept 2024 |
| Event | 15th International Conference on Interactive Theorem Proving, ITP 2024 - Tbilisi, Georgia Duration: 9 Sept 2024 → 14 Sept 2024 |
Publication series
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 309 |
| ISSN (Print) | 1868-8969 |
Conference
| Conference | 15th International Conference on Interactive Theorem Proving, ITP 2024 |
|---|---|
| Country/Territory | Georgia |
| City | Tbilisi |
| Period | 9/09/24 → 14/09/24 |
Bibliographical note
Publisher Copyright:© 2024 Kai Obendrauf, Anne Baanen, Patrick Koopmann, and Vera Stebletsova.
Keywords
- Coalition Logic
- common knowledge
- completeness
- Epistemic Logic
- formal methods
- Lean prover
- Multi-agent systems