Sammendrag
This thesis presents a free-variable sequent calculi for the modal logics
K45, S5 and the logic of Only Knowing. Labels act as placeholders for
points in models, using label variables to postpone the choice of point until
more knowledge of a putative satisfying model is gathered, allowing a
least commitment search. The relation of contextually equivalents is used
to obtain variable-sharing derivations baring tight connections to matrix
systems and the goal directed Connection calculus. A system of indexed
formulae is employed to enforce reuse of label parameters, establishing an
upper bound for the search space. The calculus of the logic of Only Knowing
is defined by combining the calculi established for K45 and S5, and
utilizing an auxiliary derivation to test models for maximality.