Free-Variable Calculi for the Modal Logics K45 and S5 --- Extended to the Logic of Only Knowing. Skjæveland, M. G. Master's thesis, University of Oslo, 2006.
Free-Variable Calculi for the Modal Logics K45 and S5 --- Extended to the Logic of Only Knowing [link]Paper  abstract   bibtex   
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.
@mastersthesis{ Sk-UIO2006,
  author = {Martin G. Skj{æ}veland},
  title = {{Free-Variable Calculi for the Modal Logics K45 and
                  S5 --- Extended to the Logic of Only Knowing}},
  school = {University of Oslo},
  year = {2006},
  url = {http://hdl.handle.net/10852/9526},
  abstract = { 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.}
}

Downloads: 0