This thesis presents a free-variable sequent calculi for the modal logicsK45, S5 and the logic of Only Knowing. Labels act as placeholders forpoints in models, using label variables to postpone the choice of point untilmore knowledge of a putative satisfying model is gathered, allowing aleast commitment search. The relation of contextually equivalents is usedto obtain variable-sharing derivations baring tight connections to matrixsystems and the goal directed Connection calculus. A system of indexedformulae is employed to enforce reuse of label parameters, establishing anupper bound for the search space. The calculus of the logic of Only Knowingis defined by combining the calculi established for K45 and S5, andutilizing an auxiliary derivation to test models for maximality.