Shakespearian modal logic: a labelled treatment of modal identity
Alberto Artosi, Paola Benassi, Guido Governatori, Antonino Rotolo · 1998
this paper we describe a modal proof system arising from the combination of a tableau-like classical system, which incorporates a restricted ("analytical") version of the cut rule, with a label formalism which allows for a speicialised, logic dependant unification algorithm. The system provides a uniform proof-theoretical treatment of first-order (normal) modal logics with identity, with and without Barcan formula and/or its converse 1