Provability Games for Non-classical Logics: Mezhirov Game for MPC, KD!, and KD

Game semantics provides an alternative view on basic logical concepts. Provability games, i.e., games for the validity of a formula provide a link between proof systems and semantics. We present a new type of provability games, namely the Mezhirov game, for minimal propositional logic and two modal systems: the logic of functional frames and the logic of serial frames, i.e., KD and prove their adequacy. The games are finite resulting in a finite search for winning strategies.