A general theorem prover for quantified modal logics. The main contribution of this work is twofold. It presents a modular tableau calculus, in the free-variable style, treating the main domain variants of quantified modal logic and dealing with languages where rigid and non-rigid designation can coexist. The calculus uses, to this end, light and simple semantical annotations. Such a general proof-system results from the fusion into a unified framework of two calculi previously defined by the second and third authors. Moreover, the work presents a theorem prover, called GQML-Prover, based on such a calculus, which is accessible in the Internet. The fair deterministic proof-search strategy used by the prover is described and illustrated via a meaningful example.