  Game semantics and winning strategies offer a potential conceptual bridge
between semantics and proof systems of logics. We illustrate this link for
hybrid logic -- an extension of modal logic that allows for explicit reference
to worlds within the language. The main result is that the systematic search of
winning strategies over all models can be finitized and thus reformulated as a
proof system.
