A complete tableau system for basic hybrid logic with propositional quantification

In this paper we present a tableau proof system for basic hybrid logic extended with quantification over basic modal propositions, and prove its completeness with respect to general models. This paper is largely devoted to the technical details of the proof, but we also discuss the link with the philosophical work of Arthur Prior, which led us to this system in the first place.