Referent: Małgorzata Kruszelnicka

Tytuł referatu: Bisimulation on finite Kripke models

Streszczenie: The notion of bisimulation has been introduced to test whether two processes behave the same. Originally discovered in Computer Science, bisimulation nowadays is employed in many fields. Today it is used in a number of areas of Computer Science such as functional languages, data types, databases, program analysis, to name but a few. Growing interests in this notion led to the discovery of bisimulation in Modal Logic and Set Theory. Finally, the notion was introduced into first-order logic, and found a straightforward game-theoretical interpretation. We present the notion of bisimulation for intuitionistic logic. Our discussion focuses on two cases: the propositional and the first-order case. In both cases we present the theorem which states that bisimulation implies logical equivalence, and consider possible variants of the inverse implication. Further, we present our contribution to the research of the inverse theorem.