@inproceedings{e4027aba3b5a4be3bacc0ad3bc9f6bd8,
title = "Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge",
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).",
keywords = "Coalition Logic, common knowledge, completeness, Epistemic Logic, formal methods, Lean prover, Multi-agent systems",
author = "Kai Obendrauf and Anne Baanen and Patrick Koopmann and Vera Stebletsova",
note = "Publisher Copyright: {\textcopyright} 2024 Kai Obendrauf, Anne Baanen, Patrick Koopmann, and Vera Stebletsova.; 15th International Conference on Interactive Theorem Proving, ITP 2024 ; Conference date: 09-09-2024 Through 14-09-2024",
year = "2024",
month = sep,
doi = "10.4230/LIPIcs.ITP.2024.28",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "1--18",
editor = "Yves Bertot and Temur Kutsia and Michael Norrish",
booktitle = "15th International Conference on Interactive Theorem Proving (ITP 2024)",
}