← All papers
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge
cs.LO
Jan 1, 2020 · v1
TL;DR
Formalizes the completeness proof for coalition logic with common knowledge in Lean.
Abstract
This paper presents a Lean formalization of the completeness proof for coalition logic with common knowledge (CL-CK). The formalization covers the syntax and semantics of the logic, the axiom system, canonical model construction, and the proof that every consistent formula is satisfiable in the canonical model.
Problem
Coalition logic with common knowledge (CL-CK) combines reasoning about coalitional ability with common knowledge among groups of agents, but its completeness proof had not been machine-checked.
Approach
The authors present a Lean formalization covering the syntax and semantics of CL-CK, its axiom system, canonical model construction, and the proof that every consistent formula is satisfiable in the canonical model.
Results
A complete Lean formalization of the completeness proof for coalition logic with common knowledge is achieved, mechanically verifying that the axiom system is adequate for the logic's semantics.