Game semantics for First-order Modal and Temporal Logics: State of the art and perspectives

Game semantics allows us to look at basic logical concepts from another side. This approach to logic has a long history, there are plenty of different types of games: provability games, semantic games, etc. And there is an interesting type of provability game called Mezhirov's game proposed by Iliya Mezhirov for intuitionistic logic of propositions and Grzegorczyk modal logic in 2006. Mezhirov's game semantics for intuitionistic logic is interesting because of its simplicity and strong connection with Kripke semantics and Kripke models. In this talk I will describe this game and present a possible generalization to intuitionistic logic of predicates QInt (to be more precise, to some extension of QInt).