A systematic presentation of quantified modal logics

this paper is an attempt at providing a systematic presentation of Quantified Modal Logics (with constant domains and rigid designators). We present a set of modular, uniform, normalizing, sound and complete labelled sequent calculi for all QMLs whose frame properties can be expressed as a finite set of first-order sentences with equality. We first present C-QK, a calculus for the logic QK, and then we extend it to any such logic QL. Each calculus, called C-QL, is modular (obtained by adding rules to C-QK), uniform (each added rule is clearly related to a property of the frame), normalizing (frame reasoning only happens at the top of the proof tree) and Kripke-sound and complete for QL. We improve on the existing literature on the subject (mainly, [21]) by extending the class of logics for which such a presentation is given, and by giving a new proof of soundness and completeness.